Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_dd1328b865aa819c364e1e9b4190389a20a5d1546b8b0b6028c8c78f394e7e5f with
x0,
x1 = 0.
Let x2 of type ι be given.
Apply andE with
nat_p x2,
equip x0 x2,
x1 = 0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_dd1328b865aa819c364e1e9b4190389a20a5d1546b8b0b6028c8c78f394e7e5f with
x1,
x1 = 0.
Let x3 of type ι be given.
Apply andE with
nat_p x3,
equip x1 x3,
x1 = 0 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_bad5adbbba30ab6e9c584ed350d824b3c3bff74e61c0a5380ac75f32855c37ee with
x2,
λ x4 x5 . add_nat x2 x3 = x5.
Apply unknownprop_1802716335fee6416d44bac0fcaaa43dc51d1b0983c43b49030fee94e3ccb659 with
add_nat x2 x3,
x2 leaving 3 subgoals.
Apply unknownprop_3336121954edce0fefb5edee2ad1b426a9827aac09625122db0ff807b493dc73 with
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
The subproof is completed by applying H2.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
add_nat x2 x3,
x0,
x2 leaving 2 subgoals.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
add_nat x2 x3,
setsum x0 x1,
x0 leaving 2 subgoals.
Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with
setsum x0 x1,
add_nat x2 x3.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
setsum x0 x1,
setsum x2 x3,
add_nat x2 x3 leaving 2 subgoals.
Apply unknownprop_092a01ae1d0b9a6545cd8d7970276c4297444af2ad61da23593151943992d677 with
x0,
x1,
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Apply unknownprop_fdfb3bc0b63e07822df027346a439c33cc340718a5ebbc484b4889f8644512aa with
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Claim L8: x3 = 0
Apply unknownprop_a50abc442758e144802e3adbefc02fb417bda6091771111332b2d10a54290944 with
x2,
x3,
0 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
The subproof is completed by applying L7.
Apply unknownprop_583d89fd1ad8d69ba9f546e19a854760a1fb18a1f5be71aa71ee27b6e6082be7 with
x1.
Apply L8 with
λ x4 x5 . equip x1 x4.
The subproof is completed by applying H6.