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_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a 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_1fbfebc9584f3b35fe974f93c7762fab1d5a4f649af5608ad307cbbc36ce4d37 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_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 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.