Let x0 of type ο be given.

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

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

Let x1 of type ο be given.

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

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

Claim L2: (λ x2 . λ x3 : ι → ι . ∀ x4 . x4 ∈ x2 ⟶ x3 (x3 x4) = x3 x4) 1 (λ x2 . 0)

Let x2 of type ι be given.

Assume H2: x2 ∈ 1.

Let x3 of type ι → ι → ο be given.

Assume H3: x3 0 0.

The subproof is completed by applying H3.

Apply unknownprop_b86feca7d75a8a9395700bbe8d4f0209442e24ec0112262c4575714731c978c8 with λ x2 . λ x3 : ι → ι . ∀ x4 . x4 ∈ x2 ⟶ x3 (x3 x4) = x3 x4 leaving 2 subgoals.

The subproof is completed by applying unknownprop_170570cd9c8bbfca7e90abaab69c5d65b36e383209d6e68011d09548573ef745.

The subproof is completed by applying L2.

■

Proofgold Proof