Let x0 of type ι → ο be given.

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

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 x4 : ι → ι → ι . ∃ x5 : ι → ι → ι → ι → ι → ι . MetaCat_product_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 setprod.

Let x2 of type ο be given.

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

Apply H2 with λ x3 x4 . lam (setprod x3 x4) (λ x5 . ap x5 0).

Let x3 of type ο be given.

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

Apply H3 with λ x4 x5 . lam (setprod x4 x5) (λ x6 . ap x6 1).

Let x4 of type ο be given.

Assume H4: ∀ x5 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 HomSet (λ x6 . lam x6 (λ x7 . x7)) (λ x6 x7 x8 x9 x10 . lam x6 (λ x11 . ap x9 (ap x10 x11))) setprod (λ x6 x7 . lam (setprod x6 x7) (λ x8 . ap x8 0)) (λ x6 x7 . lam (setprod x6 x7) (λ x8 . ap x8 1)) x5 ⟶ x4.

Apply H4 with λ x5 x6 x7 x8 x9 . lam x7 (λ x10 . lam 2 (λ x11 . If_i (x11 = 0) (ap x8 x10) (ap x9 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 (setprod x5 x6), HomSet (setprod x5 x6) x5 (lam (setprod x5 x6) (λ x7 . ap x7 0)), HomSet (setprod x5 x6) x6 (lam (setprod x5 x6) (λ x7 . ap x7 1)), ∀ x7 . ... ⟶ ∀ x8 x9 . ... ⟶ ... ⟶ and (and (and (HomSet x7 (setprod x5 x6) ((λ x10 x11 x12 . lam x10 (λ x13 . lam 2 (λ x14 . If_i (x14 = 0) (ap x11 x13) (ap x12 x13)))) x7 x8 x9)) (lam x7 (λ x10 . ap (lam (setprod x5 x6) (λ x11 . ap x11 0)) ...) = ...)) ...) ... leaving 6 subgoals.

...

■

Proofgold Proof