Let x0 of type ι → ο be given.
Assume H0:
∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setprod x1 x2).
Assume H1:
∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setexp x2 x1).
Let x1 of type ο be given.
Assume H2:
∀ x2 : ι → ι → ι . (∃ x3 x4 : ι → ι → ι . ∃ x5 : ι → ι → ι → ι → ι → ι . ∃ x6 x7 : ι → ι → ι . ∃ x8 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p x0 HomSet (λ x9 . lam_id x9) (λ x9 x10 x11 x12 x13 . lam_comp x9 x12 x13) x2 x3 x4 x5 x6 x7 x8) ⟶ x1.
Apply H2 with
setprod.
Let x2 of type ο be given.
Assume H3:
∀ x3 : ι → ι → ι . (∃ x4 : ι → ι → ι . ∃ x5 : ι → ι → ι → ι → ι → ι . ∃ x6 x7 : ι → ι → ι . ∃ x8 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p x0 HomSet (λ x9 . lam_id x9) (λ x9 x10 x11 x12 x13 . lam_comp x9 x12 x13) setprod x3 x4 x5 x6 x7 x8) ⟶ x2.
Apply H3 with
λ x3 x4 . lam (setprod x3 x4) (λ x5 . ap x5 0).
Let x3 of type ο be given.
Apply H4 with
λ x4 x5 . lam (setprod x4 x5) (λ x6 . ap x6 1).
Let x4 of type ο be given.
Apply H5 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.
Apply H6 with
λ x6 x7 . setexp x7 x6.
Let x6 of type ο be given.