Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι → ι . (∃ x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p 8b17e.. BinRelnHom struct_id struct_comp x1 x2 x3 x4) ⟶ x0.

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

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p 8b17e.. BinRelnHom struct_id struct_comp (λ x5 x6 . pack_r 0 (λ x7 x8 . False)) x2 x3 x4) ⟶ x1.

Apply H1 with λ x2 x3 . 0.

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p 8b17e.. BinRelnHom struct_id struct_comp (λ x5 x6 . pack_r 0 (λ x7 x8 . False)) (λ x5 x6 . 0) x3 x4) ⟶ x2.

Apply H2 with λ x3 x4 . 0.

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p 8b17e.. BinRelnHom struct_id struct_comp (λ x5 x6 . pack_r 0 (λ x7 x8 . False)) (λ x5 x6 . 0) (λ x5 x6 . 0) x4 ⟶ x3.

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

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H4: 8b17e.. x4.

Assume H5: 8b17e.. x5.

Claim L6: ...

...

Apply and6I with 8b17e.. x4, 8b17e.. x5, 8b17e.. (pack_r 0 (λ x6 x7 . False)), BinRelnHom x4 (pack_r 0 (λ x6 x7 . False)) 0, BinRelnHom x5 (pack_r 0 (λ x6 x7 . False)) 0, ∀ x6 . 8b17e.. x6 ⟶ ∀ x7 x8 . BinRelnHom x4 x6 x7 ⟶ BinRelnHom x5 x6 x8 ⟶ and (and (and (BinRelnHom (pack_r 0 (λ x9 x10 . False)) x6 0) (struct_comp x4 (pack_r 0 (λ x9 x10 . False)) x6 0 0 = x7)) (struct_comp x5 (pack_r 0 (λ x9 x10 . False)) x6 0 0 = x8)) (∀ x9 . BinRelnHom (pack_r 0 (λ x10 x11 . False)) x6 x9 ⟶ struct_comp x4 (pack_r 0 (λ x10 x11 . False)) x6 x9 0 = x7 ⟶ struct_comp x5 (pack_r 0 (λ x10 x11 . False)) x6 x9 0 = x8 ⟶ x9 = 0) leaving 6 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

The subproof is completed by applying L6.

Apply unknownprop_5d29dee76dbe631c3e61c3da6506dfaf505efc5a4aa6bec582f8fe5c402e18fa with x4, pack_r 0 (λ x6 x7 . False) leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying L6.

Apply unknownprop_5d29dee76dbe631c3e61c3da6506dfaf505efc5a4aa6bec582f8fe5c402e18fa with x5, pack_r 0 (λ x6 x7 . False) leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying L6.

Let x6 of type ι be given.

Assume H7: 8b17e.. x6.

Let x7 of type ι be given.

Let x8 of type ι be given.

Assume H8: BinRelnHom x4 x6 x7.

Assume H9: BinRelnHom x5 x6 x8.

Claim L10: ...

...

Claim L11: ...

...

Apply and4I with BinRelnHom (pack_r 0 (λ x9 x10 . False)) x6 0, struct_comp x4 (pack_r 0 (λ x9 x10 . False)) x6 0 0 = x7, struct_comp x5 (pack_r 0 (λ x9 x10 . False)) x6 0 0 = x8, ∀ x9 . ... ⟶ struct_comp x4 (pack_r 0 ...) ... ... 0 = ... ⟶ struct_comp x5 (pack_r 0 (λ x10 x11 . False)) x6 x9 0 = x8 ⟶ x9 = 0 leaving 4 subgoals.

...

■

Proofgold Proof