Let x0 of type ο be given.

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

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

Let x1 of type ο be given.

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

Apply H1 with λ x2 x3 x4 x5 . 0.

Let x2 of type ο be given.

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

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

Let x3 of type ι be given.

Let x4 of type ι be given.

Assume H3: 90aea.. x3.

Assume H4: 90aea.. x4.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H5: BinRelnHom x3 x4 x5.

Assume H6: BinRelnHom x3 x4 x6.

Claim L7: ...

...

Apply unknownprop_9981628fee84bcf70587ffb7933bd9c35042a1a594a2ae21c28e38ea11e09d6a with 90aea.. x3, 90aea.. x4, BinRelnHom x3 x4 x5, BinRelnHom x3 x4 x6, 90aea.. (pack_r 0 (λ x7 x8 . False)), BinRelnHom (pack_r 0 (λ x7 x8 . False)) x3 0, struct_comp (pack_r 0 (λ x7 x8 . False)) x3 x4 x5 0 = struct_comp (pack_r 0 (λ x7 x8 . False)) x3 x4 x6 0, ∀ x7 . 90aea.. x7 ⟶ ∀ x8 . BinRelnHom x7 x3 x8 ⟶ struct_comp x7 x3 x4 x5 x8 = struct_comp x7 x3 x4 x6 x8 ⟶ and (and (BinRelnHom x7 (pack_r 0 (λ x9 x10 . False)) 0) (struct_comp x7 (pack_r 0 (λ x9 x10 . False)) x3 0 0 = x8)) (∀ x9 . BinRelnHom x7 (pack_r 0 (λ x10 x11 . False)) x9 ⟶ struct_comp x7 (pack_r 0 (λ x10 x11 . False)) x3 0 x9 = x8 ⟶ x9 = 0) leaving 8 subgoals.

The subproof is completed by applying H3.

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 L7.

Apply unknownprop_db29be70f626d907819defaaafb0849de7b3b2be132ffdec2cf3d6bf6e7f756a with pack_r 0 (λ x7 x8 . False), x3 leaving 2 subgoals.

The subproof is completed by applying L7.

The subproof is completed by applying H3.

Apply unknownprop_765d413c5d1a8be896fb2d38fda75f9803185335550bf0cbde813c254ddda463 with pack_r 0 (λ x7 x8 . False), x3, x4, x6, 0, λ x7 x8 . struct_comp (pack_r 0 (λ x9 x10 . False)) x3 x4 x5 0 = x8 leaving 2 subgoals.

The subproof is completed by applying L7.

Apply unknownprop_765d413c5d1a8be896fb2d38fda75f9803185335550bf0cbde813c254ddda463 with pack_r 0 (λ x7 x8 . False), x3, x4, x5, 0.

The subproof is completed by applying L7.

Let x7 of type ι be given.

Assume H8: 90aea.. x7.

Let x8 of type ι be given.

Assume H9: BinRelnHom x7 x3 x8.

Assume H10: struct_comp x7 x3 x4 x5 x8 = struct_comp x7 x3 x4 x6 x8.

Claim L11: ...

...

Apply and3I with BinRelnHom x7 (pack_r 0 (λ x9 x10 . False)) 0, struct_comp x7 (pack_r 0 (λ x9 x10 . False)) x3 0 0 = x8, ∀ x9 . ... ⟶ struct_comp x7 (pack_r 0 (λ x10 x11 . False)) x3 0 ... = ... ⟶ x9 = 0 leaving 3 subgoals.

...

■

Proofgold Proof