Let x0 of type ι be given.
Apply unknownprop_18f2d370dfd49e4814f0679ca190367baf02242d69c073c3acc36d9d0ad55409 with
x0,
(λ x1 x2 . Inj1 (setsum x1 x2)) ((λ x1 x2 . Inj1 (setsum x1 x2)) (Inj0 0) x0) x0,
x0 leaving 2 subgoals.
Apply unknownprop_59dc2ada135e75255841f62c62f419a2d1e6131d02495074154917da7a240d45 with
Inj1 (setsum (Inj1 (setsum (Inj0 0) x0)) x0),
x0.
The subproof is completed by applying unknownprop_0c6fbfed11077b2a213848b5161614fab651df3e326c4cdaaf5b72693971ae12 with x0, x0.
The subproof is completed by applying unknownprop_0c6fbfed11077b2a213848b5161614fab651df3e326c4cdaaf5b72693971ae12 with x0, x0.