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)),
∃ x3 . and (In x3 x0) (∃ x4 . and (In x4 (x1 x3)) (x2 = setsum x3 x4)) leaving 2 subgoals.
Apply unknownprop_632d5604ed3c6300a4762cec49c7927befabcc480df4aa1142cf8872f14519d7 with
x0,
x1,
x2.
The subproof is completed by applying H0.
Let x3 of type ο be given.
Assume H4:
∀ x4 . and (In x4 x0) (∃ x5 . and (In x5 (x1 x4)) (x2 = setsum x4 x5)) ⟶ x3.
Apply H4 with
proj0 x2.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In (proj0 x2) x0,
∃ x4 . and (In x4 (x1 (proj0 x2))) (x2 = setsum (proj0 x2) x4) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x4 of type ο be given.
Apply H5 with
proj1 x2.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In (proj1 x2) (x1 (proj0 x2)),
x2 = setsum (proj0 x2) (proj1 x2) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x5 of type ι → ι → ο be given.
The subproof is completed by applying H1 with λ x6 x7 . x5 x7 x6.