Let x0 of type ο be given.

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

Apply H0 with pack_u 1 (λ x1 . x1).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . MetaCat_terminal_p struct_u UnaryFuncHom struct_id struct_comp (pack_u 1 (λ x3 . x3)) x2 ⟶ x1.

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

Apply unknownprop_4c2c2f02b7bba52d2c2d534bff462776dfb77dde8f7d02ce4d576ba29cf94915 with struct_u leaving 2 subgoals.

Let x2 of type ι be given.

Assume H2: struct_u x2.

The subproof is completed by applying H2.

Apply pack_struct_u_I with 1, λ x2 . x2.

Let x2 of type ι be given.

Assume H2: x2 ∈ 1.

The subproof is completed by applying H2.

■

Proofgold Proof