Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Assume H0:
In x2 (lam x0 (λ x3 . x1 x3)).
Apply unknownprop_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with
setsum (proj0 x2) (proj1 x2) = x2,
In (proj0 x2) x0,
In (proj1 x2) (x1 (proj0 x2)),
setsum (proj0 x2) (proj1 x2) = x2 leaving 2 subgoals.
Apply unknownprop_632d5604ed3c6300a4762cec49c7927befabcc480df4aa1142cf8872f14519d7 with
x0,
x1,
x2.
The subproof is completed by applying H0.
The subproof is completed by applying H1.