Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
proj1 (setsum x0 x1),
x1 leaving 2 subgoals.
Let x2 of type ι be given.
Apply unknownprop_be49f58ae512303b2e2368079518d123ccac20768e32f8ffad0cf1d3d6946239 with
x0,
x1,
x2.
Apply unknownprop_ddee32b485fe3b18e7ed6649c430b0ba07fbbe95c6ca01a1512260320292f5d6 with
setsum x0 x1,
x2.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply unknownprop_83b1431ffbe4fafc920badacc16dca6e556c4f5636fd99bcf3d43ceb7144eaab with
setsum x0 x1,
x2.
Apply unknownprop_ba4ceb4cfc28d9d20da4c7556dd8a911f49892fbf59d2c31799f1fb1cd51e58b with
x0,
x1,
x2.
The subproof is completed by applying H0.