Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι → ι . (∃ x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . ∃ x5 x6 : ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p 8b17e.. 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 8b17e.. 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 8b17e.. 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 8b17e.. 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 8b17e.. 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 8b17e.. 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 8b17e.. 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 8b17e.. 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 . 8b17e.. x7 ⟶ 8b17e.. x8 ⟶ MetaCat_exp_p 8b17e.. 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_019eb3b7cc5b1d8119b16df5b31478f2fc6984523484e01d24620556dcd20e19.

Let x7 of type ι be given.

Let x8 of type ι be given.

Assume H7: 8b17e.. x7.

Assume H8: 8b17e.. x8.

Claim L9: ...

...

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

...

■

Proofgold Proof