Let x0 of type ο be given.

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

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

Let x1 of type ο be given.

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

Apply H1 with λ x2 x3 . 0.

Let x2 of type ο be given.

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

Apply H2 with λ x3 x4 . 0.

Let x3 of type ο be given.

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

Apply H3 with λ x4 x5 x6 x7 x8 . 0.

Let x4 of type ο be given.

Assume H4: ∀ x5 : ι → ι → ι . (∃ x6 : ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p 90aea.. BinRelnHom struct_id struct_comp (λ x8 x9 . pack_r 0 (λ x10 x11 . False)) (λ x8 x9 . 0) (λ x8 x9 . 0) (λ x8 x9 x10 x11 x12 . 0) x5 x6 x7) ⟶ x4.

Apply H4 with λ x5 x6 . pack_r 0 (λ x7 x8 . False).

Let x5 of type ο be given.

Assume H5: ∀ x6 : ι → ι → ι . (∃ x7 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p 90aea.. BinRelnHom struct_id struct_comp (λ x8 x9 . pack_r 0 (λ x10 x11 . False)) (λ x8 x9 . 0) (λ x8 x9 . 0) (λ x8 x9 x10 x11 x12 . 0) (λ x8 x9 . pack_r 0 (λ x10 x11 . False)) x6 x7) ⟶ x5.

Apply H5 with λ x6 x7 . 0.

Let x6 of type ο be given.

Assume H6: ∀ x7 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p 90aea.. BinRelnHom struct_id struct_comp (λ x8 x9 . pack_r 0 (λ x10 x11 . False)) (λ x8 x9 . 0) (λ x8 x9 . 0) (λ x8 x9 x10 x11 x12 . 0) (λ x8 x9 . pack_r 0 (λ x10 x11 . False)) (λ x8 x9 . 0) x7 ⟶ x6.

Apply H6 with λ x7 x8 x9 x10 . 0.

Apply andI with MetaCat_product_constr_p 90aea.. BinRelnHom struct_id struct_comp (λ x7 x8 . pack_r 0 (λ x9 x10 . False)) (λ x7 x8 . 0) (λ x7 x8 . 0) (λ x7 x8 x9 x10 x11 . 0), ∀ x7 x8 . 90aea.. x7 ⟶ 90aea.. x8 ⟶ MetaCat_exp_p 90aea.. BinRelnHom struct_id struct_comp (λ x9 x10 . pack_r 0 (λ x11 x12 . False)) (λ x9 x10 . 0) (λ x9 x10 . 0) (λ x9 x10 x11 x12 x13 . 0) x7 x8 (pack_r 0 (λ x9 x10 . False)) 0 (λ x9 x10 . 0) leaving 2 subgoals.

The subproof is completed by applying unknownprop_bab06722b95d9bfeb5f47bd12c980207aa4ecb908298635ec81d8f167d979164.

Let x7 of type ι be given.

Let x8 of type ι be given.

Assume H7: 90aea.. x7.

Assume H8: 90aea.. x8.

Claim L9: ...

...

Apply and5I with 90aea.. x7, 90aea.. x8, 90aea.. (pack_r 0 (λ x9 x10 . False)), BinRelnHom (pack_r 0 (λ x9 x10 . False)) ... 0, ... leaving 5 subgoals.

...

■

Proofgold Proof