Let x0 of type ι be given.

Claim L0: combinator_equiv ((λ x1 x2 . Inj1 (setsum x1 x2)) ((λ x1 x2 . Inj1 (setsum x1 x2)) ((λ x1 x2 . Inj1 (setsum x1 x2)) (Inj0 (Power 0)) (Inj0 0)) (Inj0 0)) x0) ((λ x1 x2 . Inj1 (setsum x1 x2)) ((λ x1 x2 . Inj1 (setsum x1 x2)) (Inj0 0) x0) ((λ x1 x2 . Inj1 (setsum x1 x2)) (Inj0 0) x0))

The subproof is completed by applying unknownprop_f902b7913114db5fa2d85e0971b159bc572f88b2a32ac77e9c7729d1b3e65b62 with Inj0 0, Inj0 0, x0.

Claim L1: combinator_equiv ((λ x1 x2 . Inj1 (setsum x1 x2)) ((λ x1 x2 . Inj1 (setsum x1 x2)) (Inj0 0) x0) ((λ x1 x2 . Inj1 (setsum x1 x2)) (Inj0 0) x0)) x0

The subproof is completed by applying unknownprop_0c6fbfed11077b2a213848b5161614fab651df3e326c4cdaaf5b72693971ae12 with x0, (λ x1 x2 . Inj1 (setsum x1 x2)) (Inj0 0) x0.

Apply unknownprop_18f2d370dfd49e4814f0679ca190367baf02242d69c073c3acc36d9d0ad55409 with (λ x1 x2 . Inj1 (setsum x1 x2)) ((λ x1 x2 . Inj1 (setsum x1 x2)) ((λ x1 x2 . Inj1 (setsum x1 x2)) (Inj0 (Power 0)) (Inj0 0)) (Inj0 0)) x0, (λ x1 x2 . Inj1 (setsum x1 x2)) ((λ x1 x2 . Inj1 (setsum x1 x2)) (Inj0 0) x0) ((λ x1 x2 . Inj1 (setsum x1 x2)) (Inj0 0) x0), x0 leaving 2 subgoals.

The subproof is completed by applying L0.

The subproof is completed by applying L1.

■

Proofgold Proof