Let x0 of type ι → ο be given.

Let x1 of type ι → ι → ι → ο be given.

Let x2 of type ι → ι be given.

Let x3 of type ι → ι → ι → ι → ι → ι be given.

Assume H0: MetaCat x0 x1 x2 x3.

Assume H1: ∃ x4 x5 : ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p x0 x1 x2 x3 x4 x5 x6.

Assume H2: ∃ x4 x5 x6 : ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p x0 x1 x2 x3 x4 x5 x6 x7.

Claim L3: MetaCat x0 (λ x4 x5 . x1 x5 x4) x2 (λ x4 x5 x6 x7 x8 . x3 x6 x5 x4 x8 x7)

Apply unknownprop_e74d2abe5a1e30f6a719b289885351f18b3a36d32b938dab696ee27d1cef86e5 with x0, x1, x2, x3.

The subproof is completed by applying H0.

Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with x0, λ x4 x5 . x1 x5 x4, x2, λ x4 x5 x6 x7 x8 . x3 x6 x5 x4 x8 x7 leaving 3 subgoals.

The subproof is completed by applying L3.

Apply H1 with ∃ x4 x5 : ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 (λ x7 x8 . x1 x8 x7) x2 (λ x7 x8 x9 x10 x11 . x3 x9 x8 x7 x11 x10) x4 x5 x6.

Let x4 of type ι → ι → ι → ι → ι be given.

Assume H4: (λ x5 : ι → ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p x0 x1 x2 x3 x5 x6 x7) x4.

Apply H4 with ∃ x5 x6 : ι → ι → ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 (λ x8 x9 . x1 x9 x8) x2 (λ x8 x9 x10 x11 x12 . x3 x10 x9 x8 x12 x11) x5 x6 x7.

Let x5 of type ι → ι → ι → ι → ι be given.

Assume H5: (λ x6 : ι → ι → ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p x0 x1 x2 x3 x4 x6 x7) x5.

Apply H5 with ∃ x6 x7 : ι → ι → ι → ι → ι . ∃ x8 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 (λ x9 x10 . x1 x10 x9) x2 (λ x9 x10 x11 x12 x13 . x3 x11 x10 x9 x13 x12) x6 x7 x8.

Let x6 of type ι → ι → ι → ι → ι → ι → ι be given.

Assume H6: MetaCat_coequalizer_struct_p x0 x1 x2 x3 x4 x5 x6.

Let x7 of type ο be given.

Assume H7: ∀ x8 : ι → ι → ι → ι → ι . (∃ x9 : ι → ι → ι → ι → ι . ∃ x10 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 (λ x11 x12 . x1 x12 x11) x2 (λ x11 x12 x13 x14 x15 . x3 x13 x12 x11 x15 x14) x8 x9 x10) ⟶ x7.

Apply H7 with λ x8 x9 . x4 x9 x8.

Let x8 of type ο be given.

Assume H8: ∀ x9 : ι → ι → ι → ι → ι . (∃ x10 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 (λ x11 x12 . x1 x12 x11) x2 (λ x11 x12 x13 x14 x15 . x3 x13 x12 x11 x15 x14) (λ x11 x12 . x4 x12 x11) x9 x10) ⟶ x8.

Apply H8 with λ x9 x10 . x5 x10 x9.

Let x9 of type ο be given.

Assume H9: ∀ x10 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 (λ x11 x12 . x1 x12 x11) x2 (λ x11 x12 x13 x14 x15 . x3 x13 x12 x11 x15 x14) (λ x11 x12 . x4 x12 x11) (λ x11 x12 . x5 x12 x11) x10 ⟶ x9.

Apply H9 with λ x10 x11 . x6 x11 x10.

Apply unknownprop_20c1347ac12b8a76491a5d9969246271fef46ed47a599bce83dd091c6cf3b962 with x0, x1, x2, x3, x4, x5, x6.

The subproof is completed by applying H6.

The subproof is completed by applying H2.

■

Proofgold Proof