Let x0 of type ι → ο be given.

Assume H0: ∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setsum x1 x2).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 x4 : ι → ι → ι . ∃ x5 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p x0 HomSet (λ x6 . lam x6 (λ x7 . x7)) (λ x6 x7 x8 x9 x10 . lam x6 (λ x11 . ap x9 (ap x10 x11))) x2 x3 x4 x5) ⟶ x1.

Apply H1 with setsum.

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι → ι . (∃ x4 : ι → ι → ι . ∃ x5 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p x0 HomSet (λ x6 . lam x6 (λ x7 . x7)) (λ x6 x7 x8 x9 x10 . lam x6 (λ x11 . ap x9 (ap x10 x11))) setsum x3 x4 x5) ⟶ x2.

Apply H2 with λ x3 x4 . lam x3 (λ x5 . Inj0 x5).

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι → ι . (∃ x5 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p x0 HomSet (λ x6 . lam x6 (λ x7 . x7)) (λ x6 x7 x8 x9 x10 . lam x6 (λ x11 . ap x9 (ap x10 x11))) setsum (λ x6 x7 . lam x6 (λ x8 . Inj0 x8)) x4 x5) ⟶ x3.

Apply H3 with λ x4 x5 . lam x5 (λ x6 . Inj1 x6).

Let x4 of type ο be given.

Assume H4: ∀ x5 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p x0 HomSet (λ x6 . lam x6 (λ x7 . x7)) (λ x6 x7 x8 x9 x10 . lam x6 (λ x11 . ap x9 (ap x10 x11))) setsum (λ x6 x7 . lam x6 (λ x8 . Inj0 x8)) (λ x6 x7 . lam x7 (λ x8 . Inj1 x8)) x5 ⟶ x4.

Apply H4 with λ x5 x6 x7 x8 x9 . lam (setsum x5 x6) (λ x10 . combine_funcs x5 x6 (λ x11 . ap x8 x11) (λ x11 . ap x9 x11) x10).

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H5: x0 x5.

Assume H6: x0 x6.

Apply and6I with x0 x5, x0 x6, x0 (setsum x5 x6), HomSet x5 (setsum x5 x6) (lam x5 (λ x7 . Inj0 x7)), HomSet x6 (setsum x5 x6) (lam x6 (λ x7 . Inj1 x7)), ∀ x7 . ... ⟶ ∀ x8 x9 . ... ⟶ ... ⟶ and (and (and (HomSet (setsum x5 x6) x7 ((λ x10 x11 x12 . lam (setsum x5 x6) (λ x13 . combine_funcs x5 x6 (λ x14 . ap x11 x14) (λ x14 . ap x12 x14) x13)) x7 x8 x9)) (lam x5 (λ x10 . ap ((λ x11 x12 x13 . lam (setsum x5 x6) (λ x14 . combine_funcs x5 x6 (λ x15 . ap x12 x15) (λ x15 . ap x13 x15) x14)) x7 x8 x9) (ap (lam x5 (λ x11 . Inj0 x11)) ...)) = ...)) ...) ... leaving 6 subgoals.

...

■

Proofgold Proof