Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι → ι → ι → ι → ι . (∃ x2 x3 : ι → ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p 90aea.. BinRelnHom struct_id struct_comp x1 x2 x3 x4) ⟶ x0.

Apply H0 with λ x1 x2 x3 x4 x5 . pack_r 0 (λ x6 x7 . False).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι . (∃ x3 : ι → ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p 90aea.. BinRelnHom struct_id struct_comp (λ x5 x6 x7 x8 x9 . pack_r 0 (λ x10 x11 . False)) x2 x3 x4) ⟶ x1.

Apply H1 with λ x2 x3 x4 x5 x6 . 0.

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι → ι → ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p 90aea.. BinRelnHom struct_id struct_comp (λ x5 x6 x7 x8 x9 . pack_r 0 (λ x10 x11 . False)) (λ x5 x6 x7 x8 x9 . 0) x3 x4) ⟶ x2.

Apply H2 with λ x3 x4 x5 x6 x7 . 0.

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p 90aea.. BinRelnHom struct_id struct_comp (λ x5 x6 x7 x8 x9 . pack_r 0 (λ x10 x11 . False)) (λ x5 x6 x7 x8 x9 . 0) (λ x5 x6 x7 x8 x9 . 0) x4 ⟶ x3.

Apply H3 with λ x4 x5 x6 x7 x8 x9 x10 x11 . 0.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H4: 90aea.. x4.

Assume H5: 90aea.. x5.

Assume H6: 90aea.. x6.

Let x7 of type ι be given.

Let x8 of type ι be given.

Assume H7: BinRelnHom x6 x4 x7.

Assume H8: BinRelnHom x6 x5 x8.

Claim L9: ...

...

Apply unknownprop_d818050ba2f8af7e5df3c2818d15e1b858ad10296faac92a7847146e94c87036 with 90aea.. x4, 90aea.. x5, 90aea.. x6, BinRelnHom x6 x4 x7, BinRelnHom x6 x5 x8, 90aea.. (pack_r 0 (λ x9 x10 . False)), BinRelnHom x4 (pack_r 0 (λ x9 x10 . False)) 0, BinRelnHom x5 (pack_r 0 (λ x9 x10 . False)) 0, struct_comp x6 x4 (pack_r 0 (λ x9 x10 . False)) 0 x7 = struct_comp x6 x5 (pack_r 0 (λ x9 x10 . False)) 0 x8, ∀ x9 . 90aea.. x9 ⟶ ∀ x10 . BinRelnHom x4 x9 x10 ⟶ ∀ x11 . BinRelnHom x5 x9 x11 ⟶ struct_comp x6 x4 x9 x10 x7 = struct_comp x6 x5 x9 x11 x8 ⟶ and (and (and (BinRelnHom (pack_r 0 (λ x12 x13 . False)) x9 0) (struct_comp x4 (pack_r 0 (λ x12 x13 . False)) x9 0 0 = x10)) (struct_comp x5 (pack_r 0 (λ x12 x13 . False)) x9 0 0 = x11)) (∀ x12 . BinRelnHom (pack_r 0 (λ x13 x14 . False)) x9 x12 ⟶ struct_comp x4 (pack_r 0 (λ x13 x14 . False)) x9 x12 0 = x10 ⟶ struct_comp x5 (pack_r 0 (λ x13 x14 . False)) x9 x12 0 = x11 ⟶ x12 = 0) leaving 10 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

The subproof is completed by applying H8.

The subproof is completed by applying L9.

Apply unknownprop_db29be70f626d907819defaaafb0849de7b3b2be132ffdec2cf3d6bf6e7f756a with x4, pack_r 0 (λ x9 x10 . False) leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying L9.

Apply unknownprop_db29be70f626d907819defaaafb0849de7b3b2be132ffdec2cf3d6bf6e7f756a with x5, pack_r 0 (λ x9 x10 . False) leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying L9.

Apply unknownprop_765d413c5d1a8be896fb2d38fda75f9803185335550bf0cbde813c254ddda463 with x6, x5, pack_r 0 ..., 0, ..., ... leaving 2 subgoals.

...

■

Proofgold Proof