Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_4bfbb4dec5e67ad21ca2193ea2b4908e823372bc7bdc402dd93e056c69cdf1ed with
setsum x0 x1,
x0,
x1 = 0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply andE with
Subq x2 x0,
equip (setsum x0 x1) x2,
x1 = 0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_2930a4208854e6b6adcdb51a7c34faf7a8789ce5177dbf41617428ceaf9b3c6b with
x2,
setsum (setminus x0 x2) x1.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
setsum x2 (setsum (setminus x0 x2) x1),
setsum (setsum x2 (setminus x0 x2)) x1,
x2 leaving 2 subgoals.
Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with
setsum (setsum x2 (setminus x0 x2)) x1,
setsum x2 (setsum (setminus x0 x2) x1).
The subproof is completed by applying unknownprop_766395d00d5702634c7092b386cd74ca5b8819cfa7c5b44f21fdf51440a1519d with
x2,
setminus x0 x2,
x1.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
setsum (setsum x2 (setminus x0 x2)) x1,
setsum x0 x1,
x2 leaving 2 subgoals.
Apply unknownprop_092a01ae1d0b9a6545cd8d7970276c4297444af2ad61da23593151943992d677 with
setsum x2 (setminus x0 x2),
x1,
x0,
x1 leaving 2 subgoals.
Apply unknownprop_90a352f74f9892bfc39c1ccdaecae19d23018050a6f899381839d73f3a3293bc with
x0,
x2.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_779bad135e02b130c4f2c6fb2f6a4cc60941e04327d78e3212c24d54199ba5e5 with x1.
The subproof is completed by applying H3.
Apply unknownprop_fe7ff313be3d0b9f2334c12982636aff94f7603137e8053506a95c79965309c2 with
x1.
Let x3 of type ι be given.
Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with
x3,
x1.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
Inj1 x3.
Apply L4 with
λ x4 x5 . In (Inj1 x3) x4.
Apply unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 with
setminus x0 x2,
x1,
x3.
The subproof is completed by applying H5.