Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι → ι . (∃ x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . ∃ x5 x6 : ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p PER BinRelnHom struct_id struct_comp x1 x2 x3 x4 x5 x6 x7) ⟶ x0.

Apply H0 with BinReln_product.

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . ∃ x5 x6 : ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p PER BinRelnHom struct_id struct_comp BinReln_product x2 x3 x4 x5 x6 x7) ⟶ x1.

Apply H1 with λ x2 x3 . lam (setprod (ap x2 0) (ap x3 0)) (λ x4 . ap x4 0).

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι . ∃ x5 x6 : ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p PER BinRelnHom struct_id struct_comp BinReln_product (λ x8 x9 . lam (setprod (ap x8 0) (ap x9 0)) (λ x10 . ap x10 0)) x3 x4 x5 x6 x7) ⟶ x2.

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

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι → ι → ι → ι → ι . (∃ x5 x6 : ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p PER BinRelnHom struct_id struct_comp BinReln_product (λ x8 x9 . lam (setprod (ap x8 0) (ap x9 0)) (λ x10 . ap x10 0)) (λ x8 x9 . lam (setprod (ap x8 0) (ap x9 0)) (λ x10 . ap x10 1)) x4 x5 x6 x7) ⟶ x3.

Apply H3 with λ x4 x5 x6 x7 x8 . lam (ap x6 0) (λ x9 . lam 2 (λ x10 . If_i (x10 = 0) (ap x7 x9) (ap x8 x9))).

Let x4 of type ο be given.

Assume H4: ∀ x5 : ι → ι → ι . (∃ x6 : ι → ι → ι . ∃ x7 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p PER BinRelnHom struct_id struct_comp BinReln_product (λ x8 x9 . lam (setprod (ap x8 0) (ap x9 0)) (λ x10 . ap x10 0)) (λ x8 x9 . lam (setprod (ap x8 0) (ap x9 0)) (λ x10 . ap x10 1)) (λ x8 x9 x10 x11 x12 . lam (ap x10 0) (λ x13 . lam 2 (λ x14 . If_i (x14 = 0) (ap x11 x13) (ap x12 x13)))) x5 x6 x7) ⟶ x4.

Apply H4 with BinReln_exp.

Let x5 of type ο be given.

Assume H5: ∀ x6 : ι → ι → ι . (∃ x7 : ι → ι → ι → ι → ι . MetaCat_exp_constr_p PER BinRelnHom struct_id struct_comp BinReln_product (λ x8 x9 . lam (setprod (ap x8 0) (ap x9 0)) (λ x10 . ap x10 0)) (λ x8 x9 . lam (setprod (ap x8 0) (ap x9 0)) (λ x10 . ap x10 1)) (λ x8 x9 x10 x11 x12 . lam ... ...) ... ... ...) ⟶ x5.

...

■

Proofgold Proof