Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
setsum 0 x0,
Inj0 x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with
0,
x0,
x1,
λ x2 . In x2 (Inj0 x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply FalseE with
(λ x3 . In x3 (Inj0 x0)) (Inj0 x2).
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x2.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply unknownprop_4f49d21f24dabb41b3016d1a1948efcd60aa6c40669844fde2f790559a3ee8dc with
x0,
x2.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply unknownprop_993af6114ae86d533b92ae8c379a80f32d0d6d215834c9194ed09e506217bf3f with
x0,
x1,
λ x2 . In x2 (setsum 0 x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 with
0,
x0,
x2.
The subproof is completed by applying H1.