Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
setsum 1 x0,
Inj1 x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with
1,
x0,
x1,
λ x2 . In x2 (Inj1 x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Claim L2: x2 = 0
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
0,
x2.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
1,
Sing 0,
x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e8598561026ee5bf15479322ab1713bd41b786cd16638ceaff374ea0aee3dd94.
The subproof is completed by applying H1.
Apply L2 with
λ x3 x4 . In (Inj0 x4) (Inj1 x0).
Apply unknownprop_25dcd37854379c500286034919edde76e517fd33657eb811d3ea3caad4445b57 with
λ x3 x4 . In x4 (Inj1 x0).
The subproof is completed by applying unknownprop_9998e40d8c081bcb0998eee5b18bc644807c64b4a7795024462a6db641b5bcc2 with x0.
Let x2 of type ι be given.
Apply unknownprop_20467f36510c7b6830c7e44d6955dc079b6e83b8bbc05b0500ccb9075a391641 with
x0,
x2.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply unknownprop_0b120035bc22426ea02988561990499be78ef89e658ec0c0b4bcff54639930cb with
x0,
x1,
λ x2 . In x2 (setsum 1 x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_25dcd37854379c500286034919edde76e517fd33657eb811d3ea3caad4445b57 with
λ x2 x3 . In x2 (setsum 1 x0).
Apply unknownprop_1fbfebc9584f3b35fe974f93c7762fab1d5a4f649af5608ad307cbbc36ce4d37 with
1,
x0,
0.
The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.
Let x2 of type ι be given.
Apply unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 with
1,
x0,
x2.
The subproof is completed by applying H1.