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_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
setsum x2 x3,
setsum x0 x1,
add_nat x0 x1 leaving 2 subgoals.
Apply unknownprop_092a01ae1d0b9a6545cd8d7970276c4297444af2ad61da23593151943992d677 with
x2,
x3,
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_fdfb3bc0b63e07822df027346a439c33cc340718a5ebbc484b4889f8644512aa with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.