Let x0 of type ι be given.

Let x1 of type ι be given.

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

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

Assume H0: per_i x2.

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

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

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

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

The subproof is completed by applying H3 with x0, x1.

■

Proofgold Proof