Let x0 of type ο be given.

Assume H0: ∀ x1 . (∃ x2 : ι → ι . MetaCat_initial_p struct_p UnaryPredHom struct_id struct_comp x1 x2) ⟶ x0.

Apply H0 with pack_p 0 (λ x1 . False).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . MetaCat_initial_p struct_p UnaryPredHom struct_id struct_comp (pack_p 0 (λ x3 . False)) x2 ⟶ x1.

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

Apply andI with struct_p (pack_p 0 (λ x2 . False)), ∀ x2 . struct_p x2 ⟶ and (UnaryPredHom (pack_p 0 (λ x3 . False)) x2 ((λ x3 . lam 0 (λ x4 . 0)) x2)) (∀ x3 . UnaryPredHom (pack_p 0 (λ x4 . False)) x2 x3 ⟶ x3 = (λ x4 . lam 0 (λ x5 . 0)) x2) leaving 2 subgoals.

The subproof is completed by applying pack_struct_p_I with 0, λ x2 . False.

Let x2 of type ι be given.

Assume H2: struct_p x2.

Apply H2 with λ x3 . and (UnaryPredHom (pack_p 0 (λ x4 . False)) x3 ((λ x4 . lam 0 (λ x5 . 0)) x3)) (∀ x4 . UnaryPredHom (pack_p 0 (λ x5 . False)) x3 x4 ⟶ x4 = (λ x5 . lam 0 (λ x6 . 0)) x3).

Let x3 of type ι be given.

Let x4 of type ι → ο be given.

Apply andI with UnaryPredHom (pack_p 0 (λ x5 . False)) (pack_p x3 x4) ((λ x5 . lam 0 (λ x6 . 0)) (pack_p x3 x4)), ∀ x5 . UnaryPredHom (pack_p 0 (λ x6 . False)) (pack_p x3 x4) x5 ⟶ x5 = (λ x6 . lam 0 (λ x7 . 0)) (pack_p x3 x4) leaving 2 subgoals.

Apply unknownprop_63c01b8f599732ba7bc3b48c28c0f10755230e5cc9f0717c7895602d2eaf01d3 with 0, x3, λ x5 . False, x4, lam 0 (λ x5 . 0), λ x5 x6 : ο . x6.

Apply andI with lam 0 (λ x5 . 0) ∈ setexp x3 0, ∀ x5 . x5 ∈ 0 ⟶ (λ x6 . False) x5 ⟶ x4 (ap (lam 0 (λ x6 . 0)) x5) leaving 2 subgoals.

Apply lam_Pi with 0, λ x5 . x3, λ x5 . 0.

Let x5 of type ι be given.

Assume H3: x5 ∈ 0.

Apply FalseE with (λ x6 . 0) x5 ∈ (λ x6 . x3) x5.

Apply EmptyE with x5.

The subproof is completed by applying H3.

Let x5 of type ι be given.

Assume H3: x5 ∈ 0.

Apply FalseE with (λ x6 . False) x5 ⟶ x4 (ap (lam 0 (λ x6 . 0)) x5).

Apply EmptyE with x5.

The subproof is completed by applying H3.

Let x5 of type ι be given.

Apply unknownprop_63c01b8f599732ba7bc3b48c28c0f10755230e5cc9f0717c7895602d2eaf01d3 with 0, x3, λ x6 . False, x4, x5, λ x6 x7 : ο . x7 ⟶ x5 = (λ x8 . lam 0 (λ x9 . 0)) (pack_p x3 x4).

Assume H3: and (x5 ∈ setexp x3 0) (∀ x6 . x6 ∈ 0 ⟶ (λ x7 . False) x6 ⟶ x4 (ap x5 x6)).

Apply H3 with x5 = (λ x6 . lam 0 (λ x7 . 0)) (pack_p x3 x4).

Assume H4: x5 ∈ setexp x3 0.

Assume H5: ∀ x6 . ... ⟶ ... ⟶ x4 ....

...

■

Proofgold Proof