Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_a818f53272de918398012791887b763f90bf043f961a4f625d98076ca0b8b392 with
In x2 (ap x0 x1),
In (setsum x1 x2) x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_762358d061bd2484ba81471a0b72cf827e125ecce5f1471d9abb4ee5039695f2 with x0, x1, x2.
The subproof is completed by applying unknownprop_5790343a8368d4f3aa514e68a19a3e4824006be2aed8a0a7a707f542e4c79154 with x0, x1, x2.