Let x0 of type ι → ο be given.

Assume H0: ∀ x1 . x0 x1 ⟶ struct_u x1.

Assume H1: ∀ x1 x2 x3 x4 . x0 x1 ⟶ x0 x2 ⟶ UnaryFuncHom x1 x2 x3 ⟶ UnaryFuncHom x1 x2 x4 ⟶ x0 (9fd7a.. x1 x2 x3 x4).

Let x1 of type ο be given.

Assume H2: ∀ x2 : ι → ι → ι → ι → ι . (∃ x3 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 UnaryFuncHom struct_id struct_comp x2 x3 x4) ⟶ x1.

Apply H2 with 9fd7a...

Let x2 of type ο be given.

Assume H3: ∀ x3 : ι → ι → ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 UnaryFuncHom struct_id struct_comp 9fd7a.. x3 x4) ⟶ x2.

Apply H3 with λ x3 x4 x5 x6 . lam {x7 ∈ ap x3 0|ap x5 x7 = ap x6 x7} (λ x7 . x7).

Let x3 of type ο be given.

Assume H4: ∀ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 UnaryFuncHom struct_id struct_comp 9fd7a.. (λ x5 x6 x7 x8 . lam {x9 ∈ ap x5 0|ap x7 x9 = ap x8 x9} (λ x9 . x9)) x4 ⟶ x3.

Apply H4 with λ x4 x5 x6 x7 x8 x9 . lam (ap x8 0) (λ x10 . ap x9 x10).

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H5: x0 x4.

Assume H6: x0 x5.

Let x6 of type ι be given.

Let x7 of type ι be given.

Assume H7: UnaryFuncHom x4 x5 x6.

Assume H8: UnaryFuncHom x4 x5 x7.

Apply H0 with x4, λ x8 . ... ⟶ ... ⟶ ∀ x9 : ο . (... ⟶ ... ⟶ (∀ x10 . ... ⟶ ∀ x11 . ... ⟶ struct_comp x10 x8 x5 x6 x11 = struct_comp x10 x8 x5 ... ... ⟶ and (and (UnaryFuncHom x10 (9fd7a.. x8 x5 x6 x7) ((λ x12 x13 x14 x15 x16 x17 . lam (ap x16 0) (λ x18 . ap x17 x18)) x8 x5 x6 x7 x10 x11)) (struct_comp x10 (9fd7a.. x8 x5 x6 x7) x8 ((λ x12 x13 x14 x15 . lam {x16 ∈ ap x12 0|ap x14 x16 = ap x15 x16} (λ x16 . x16)) x8 x5 x6 x7) ((λ x12 x13 x14 x15 x16 x17 . lam (ap x16 0) (λ x18 . ap x17 x18)) x8 x5 x6 x7 x10 x11) = x11)) (∀ x12 . UnaryFuncHom x10 (9fd7a.. x8 x5 x6 x7) x12 ⟶ struct_comp x10 (9fd7a.. x8 x5 x6 x7) x8 ((λ x13 x14 x15 x16 . lam {x17 ∈ ap x13 0|ap x15 x17 = ap x16 x17} (λ x17 . x17)) x8 x5 x6 x7) x12 = x11 ⟶ x12 = (λ x13 x14 x15 x16 x17 x18 . lam (ap x17 0) (λ x19 . ap x18 x19)) x8 x5 x6 x7 x10 x11)) ⟶ x9) ⟶ x9, ... leaving 5 subgoals.

...

■

Proofgold Proof