Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
proj0 (setsum x0 x1),
x0 leaving 2 subgoals.
Let x2 of type ι be given.
Apply unknownprop_ba4bb65adf54ad53c05d3eefc02d565182a8e5e71305460b987698b4f5a40e27 with
x0,
x1,
x2.
Apply unknownprop_5992b8b7bec7fb836d55125523d586d30ffbc11c7b85cf6cd43502369de91721 with
setsum x0 x1,
x2.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply unknownprop_ceb85c7fe43781527455d6fbd821c5b30186b44a5471ea98652de6fa2b7064d9 with
setsum x0 x1,
x2.
Apply unknownprop_a381a34f160abaf2788d778fb7e511fe432033da3c71a8dc7ca4fe2a805729af with
x0,
x1,
x2.
The subproof is completed by applying H0.