Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
setsum x0 x1,
setsum x2 x3.
Let x4 of type ι be given.
Apply unknownprop_976b9ed71c1ec1f277c9c37a01879b51c2de3497fe82149802bec54f853970e6 with
x0,
x1,
x4,
λ x5 . In x5 (setsum x2 x3) leaving 3 subgoals.
The subproof is completed by applying H2.
Let x5 of type ι be given.
Apply unknownprop_a381a34f160abaf2788d778fb7e511fe432033da3c71a8dc7ca4fe2a805729af with
x2,
x3,
x5.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x0,
x2,
x5 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Let x5 of type ι be given.
Apply unknownprop_ba4ceb4cfc28d9d20da4c7556dd8a911f49892fbf59d2c31799f1fb1cd51e58b with
x2,
x3,
x5.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x1,
x3,
x5 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.