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: combinator x0.

Assume H1: combinator x1.

Assume H2: combinator x2.

Assume H3: combinator x3.

Apply unknownprop_6d861aa069d3c6b52ea4a1626e236a28ccef38ff01ec7a48d612e144c66b13b6 with λ x4 x5 : ι → ι → ο . x5 x0 x2 ⟶ x5 x1 x3 ⟶ x5 ((λ x6 x7 . Inj1 (setsum x6 x7)) x0 x1) ((λ x6 x7 . Inj1 (setsum x6 x7)) x2 x3).

Assume H4: (λ x4 x5 . ∀ x6 : ι → ι → ο . per_i x6 ⟶ (∀ x7 . combinator x7 ⟶ x6 x7 x7) ⟶ (∀ x7 x8 x9 x10 . combinator x7 ⟶ combinator x8 ⟶ combinator x9 ⟶ combinator x10 ⟶ x6 x7 x9 ⟶ x6 x8 x10 ⟶ x6 (Inj1 (setsum x7 x8)) (Inj1 (setsum x9 x10))) ⟶ (∀ x7 x8 . x6 (Inj1 (setsum (Inj1 (setsum (Inj0 0) x7)) x8)) x7) ⟶ (∀ x7 x8 x9 . x6 (Inj1 (setsum (Inj1 (setsum (Inj1 (setsum (Inj0 (Power 0)) x7)) x8)) x9)) (Inj1 (setsum (Inj1 (setsum x7 x9)) (Inj1 (setsum x8 x9))))) ⟶ x6 x4 x5) x0 x2.

Assume H5: (λ x4 x5 . ∀ x6 : ι → ι → ο . per_i x6 ⟶ (∀ x7 . combinator x7 ⟶ x6 x7 x7) ⟶ (∀ x7 x8 x9 x10 . combinator x7 ⟶ combinator x8 ⟶ combinator x9 ⟶ combinator x10 ⟶ x6 x7 x9 ⟶ x6 x8 x10 ⟶ x6 (Inj1 (setsum x7 x8)) (Inj1 (setsum x9 x10))) ⟶ (∀ x7 x8 . x6 (Inj1 (setsum (Inj1 (setsum (Inj0 0) x7)) x8)) x7) ⟶ (∀ x7 x8 x9 . x6 (Inj1 (setsum (Inj1 (setsum (Inj1 (setsum (Inj0 (Power 0)) x7)) x8)) x9)) (Inj1 (setsum (Inj1 (setsum x7 x9)) (Inj1 (setsum x8 x9))))) ⟶ x6 x4 x5) x1 x3.

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

Assume H6: per_i x4.

Assume H7: ∀ x5 . combinator x5 ⟶ x4 x5 x5.

Assume H8: ∀ x5 x6 x7 x8 . combinator x5 ⟶ combinator x6 ⟶ combinator x7 ⟶ combinator x8 ⟶ x4 x5 x7 ⟶ x4 x6 x8 ⟶ x4 (Inj1 (setsum x5 x6)) (Inj1 (setsum x7 x8)).

Assume H9: ∀ x5 x6 . x4 (Inj1 (setsum (Inj1 (setsum (Inj0 0) x5)) x6)) x5.

Assume H10: ∀ x5 x6 x7 . x4 (Inj1 (setsum (Inj1 (setsum (Inj1 (setsum (Inj0 (Power 0)) x5)) x6)) x7)) (Inj1 (setsum (Inj1 (setsum x5 x7)) (Inj1 (setsum ... ...)))).

...

■

Proofgold Proof