Let x0 of type ι → ο be given.

Assume H0: ∀ x1 . x0 x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x0 x2.

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι → ι → ι . (∃ x3 : ι → ι → ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p x0 HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) x2 x3 x4) ⟶ x1.

Apply H1 with λ x2 x3 x4 x5 . {x6 ∈ x3|quotient (3897e.. x2 x4 x5) x6}.

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι → ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p x0 HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) (λ x5 x6 x7 x8 . {x9 ∈ x6|quotient (3897e.. x5 x7 x8) x9}) x3 x4) ⟶ x2.

Apply H2 with λ x3 x4 x5 x6 . lam x4 (λ x7 . canonical_elt (3897e.. x3 x5 x6) x7).

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p x0 HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) (λ x5 x6 x7 x8 . {x9 ∈ x6|quotient (3897e.. x5 x7 x8) x9}) (λ x5 x6 x7 x8 . lam x6 (λ x9 . canonical_elt (3897e.. x5 x7 x8) x9)) x4 ⟶ x3.

Apply H3 with λ x4 x5 x6 x7 x8 x9 . lam {x10 ∈ x5|quotient (3897e.. x4 x6 x7) x10} (λ x10 . ap x9 x10).

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H4: x0 x4.

Assume H5: x0 x5.

Let x6 of type ι be given.

Let x7 of type ι be given.

Assume H6: HomSet x4 x5 x6.

Assume H7: HomSet x4 x5 x7.

Claim L8: ...

...

Apply unknownprop_9981628fee84bcf70587ffb7933bd9c35042a1a594a2ae21c28e38ea11e09d6a with x0 x4, x0 x5, HomSet x4 x5 x6, HomSet x4 x5 x7, x0 {x8 ∈ x5|quotient (3897e.. x4 x6 x7) x8}, HomSet x5 {x8 ∈ x5|quotient (3897e.. x4 x6 x7) x8} (lam x5 (λ x8 . canonical_elt (3897e.. x4 x6 x7) x8)), (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) x4 x5 {x8 ∈ x5|quotient (3897e.. x4 x6 x7) x8} (lam x5 (λ x8 . canonical_elt (3897e.. x4 x6 x7) x8)) x6 = (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) x4 x5 {x8 ∈ x5|quotient (3897e.. x4 x6 x7) x8} (lam x5 (λ x8 . canonical_elt (3897e.. x4 x6 x7) x8)) x7, ∀ x8 . ... ⟶ ∀ x9 . ... ⟶ ... ⟶ and (and (HomSet {x10 ∈ x5|quotient (3897e.. x4 x6 x7) x10} x8 ((λ x10 x11 x12 x13 x14 x15 . lam {x16 ∈ x11|quotient (3897e.. x10 x12 x13) x16} (λ x16 . ap x15 x16)) x4 x5 x6 ... ... ...)) ...) ... leaving 8 subgoals.

...

■

Proofgold Proof