Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_3030666c70e3b0a40e79c3dea18074452b4f067cae53efb13b5a85e3938a9613 with
setsum x0 x1,
λ x2 x3 . x2 = x1.
The subproof is completed by applying unknownprop_d4bb68cbfba730ad1b1ee2c6901fadf3c573cb615fac3296f9bb52128e37668a with x0, x1.