Let x0 of type ο be given.

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

Apply H0 with pack_r 0 (λ x1 x2 . False).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . MetaCat_initial_p struct_r BinRelnHom struct_id struct_comp (pack_r 0 (λ x3 x4 . False)) x2 ⟶ x1.

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

Apply andI with struct_r (pack_r 0 (λ x2 x3 . False)), ∀ x2 . struct_r x2 ⟶ and (BinRelnHom (pack_r 0 (λ x3 x4 . False)) x2 ((λ x3 . lam 0 (λ x4 . 0)) x2)) (∀ x3 . BinRelnHom (pack_r 0 (λ x4 x5 . False)) x2 x3 ⟶ x3 = (λ x4 . lam 0 (λ x5 . 0)) x2) leaving 2 subgoals.

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

Let x2 of type ι be given.

Assume H2: struct_r x2.

Apply H2 with λ x3 . and (BinRelnHom (pack_r 0 (λ x4 x5 . False)) x3 ((λ x4 . lam 0 (λ x5 . 0)) x3)) (∀ x4 . BinRelnHom (pack_r 0 (λ x5 x6 . 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 BinRelnHom (pack_r 0 (λ x5 x6 . False)) (pack_r x3 x4) ((λ x5 . lam 0 (λ x6 . 0)) (pack_r x3 x4)), ∀ x5 . BinRelnHom (pack_r 0 (λ x6 x7 . False)) (pack_r x3 x4) x5 ⟶ x5 = (λ x6 . lam 0 (λ x7 . 0)) (pack_r x3 x4) leaving 2 subgoals.

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

Apply andI with lam 0 (λ x5 . 0) ∈ setexp x3 0, ∀ x5 . x5 ∈ 0 ⟶ ∀ x6 . x6 ∈ 0 ⟶ (λ x7 x8 . False) x5 x6 ⟶ x4 (ap (lam 0 (λ x7 . 0)) x5) (ap (lam 0 (λ x7 . 0)) x6) 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 . x6 ∈ 0 ⟶ (λ x7 x8 . False) x5 x6 ⟶ x4 (ap (lam 0 (λ x7 . 0)) x5) (ap (lam 0 (λ x7 . 0)) x6).

Apply EmptyE with x5.

The subproof is completed by applying H3.

Let x5 of type ι be given.

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

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

...

■

Proofgold Proof