Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

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

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

Assume H0: per_i x3.

Assume H1: ∀ x4 . combinator x4 ⟶ x3 x4 x4.

Assume H2: ∀ x4 x5 x6 x7 . combinator x4 ⟶ combinator x5 ⟶ combinator x6 ⟶ combinator x7 ⟶ x3 x4 x6 ⟶ x3 x5 x7 ⟶ x3 (Inj1 (setsum x4 x5)) (Inj1 (setsum x6 x7)).

Assume H3: ∀ x4 x5 . x3 (Inj1 (setsum (Inj1 (setsum (Inj0 0) x4)) x5)) x4.

Assume H4: ∀ x4 x5 x6 . x3 (Inj1 (setsum (Inj1 (setsum (Inj1 (setsum (Inj0 (Power 0)) x4)) x5)) x6)) (Inj1 (setsum (Inj1 (setsum x4 x6)) (Inj1 (setsum x5 x6)))).

The subproof is completed by applying H4 with x0, x1, x2.

■

Proofgold Proof