Let x0 of type ι be given.

Let x1 of type ι be given.

Apply unknownprop_6d861aa069d3c6b52ea4a1626e236a28ccef38ff01ec7a48d612e144c66b13b6 with λ x2 x3 : ι → ι → ο . x3 x0 x1 ⟶ x3 x1 x0.

Assume H0: (λ x2 x3 . ∀ x4 : ι → ι → ο . per_i x4 ⟶ (∀ x5 . combinator x5 ⟶ x4 x5 x5) ⟶ (∀ 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))) ⟶ (∀ x5 x6 . x4 (Inj1 (setsum (Inj1 (setsum (Inj0 0) x5)) x6)) x5) ⟶ (∀ x5 x6 x7 . x4 (Inj1 (setsum (Inj1 (setsum (Inj1 (setsum (Inj0 (Power 0)) x5)) x6)) x7)) (Inj1 (setsum (Inj1 (setsum x5 x7)) (Inj1 (setsum x6 x7))))) ⟶ x4 x2 x3) x0 x1.

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

Assume H1: per_i x2.

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

Assume H3: ∀ 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 H4: ∀ x3 x4 . x2 (Inj1 (setsum (Inj1 (setsum (Inj0 0) x3)) x4)) x3.

Assume H5: ∀ 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)))).

Apply unknownprop_5574bdb5e5df6f14031f4de95b01de091bd6680b3f0f837fce12fa18146d5760 with x2, x2 x1 x0 leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H6: symmetric_i x2.

Assume H7: transitive_i x2.

Apply unknownprop_674ed6c4effec187d63542edb45f0f44eee57482deede26631bfc32a17ae2e6f with x2, x0, x1 leaving 2 subgoals.

The subproof is completed by applying H6.

Apply H0 with x2 leaving 5 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

■

Proofgold Proof