Let x0 of type ο be given.

Assume H0: ∀ x1 . (∃ x2 : ι → ι . MetaCat_terminal_p struct_b MagmaHom struct_id struct_comp x1 x2) ⟶ x0.

Apply H0 with pack_b 1 (λ x1 x2 . x1).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . MetaCat_terminal_p struct_b MagmaHom struct_id struct_comp (pack_b 1 (λ x3 x4 . x3)) x2 ⟶ x1.

Apply H1 with λ x2 . lam (ap x2 0) (λ x3 . 0).

Apply unknownprop_b85684d5d13773c983896044d4d43e914e6f740191b490f214049d237f32dd7c with struct_b leaving 2 subgoals.

Let x2 of type ι be given.

Assume H2: struct_b x2.

The subproof is completed by applying H2.

Apply pack_struct_b_I with 1, λ x2 x3 . x2.

Let x2 of type ι be given.

Assume H2: x2 ∈ 1.

Let x3 of type ι be given.

Assume H3: x3 ∈ 1.

The subproof is completed by applying H2.

■

Proofgold Proof