Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_17fe3de18bc1fbdc28d994143167b7a573f559855ba378d2014a681d31fa93ad with
λ x3 x4 : ι → (ι → ι) → ι . In x2 (x4 x0 (λ x5 . x1 x5)) ⟶ and (and (setsum (proj0 x2) (proj1 x2) = x2) (In (proj0 x2) x0)) (In (proj1 x2) (x1 (proj0 x2))).
Apply unknownprop_a7f2dda18b84bce65b5de34328a937fef2c23812675d88bde1e7e2463ed59bbe with
x0,
λ x3 . Repl (x1 x3) (λ x4 . setsum x3 x4),
x2,
and (and (setsum (proj0 x2) (proj1 x2) = x2) (In (proj0 x2) x0)) (In (proj1 x2) (x1 (proj0 x2))) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
x1 x3,
setsum x3,
x2,
and (and (setsum (proj0 x2) (proj1 x2) = x2) (In (proj0 x2) x0)) (In (proj1 x2) (x1 (proj0 x2))) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x4 of type ι be given.
Assume H3:
In x4 (x1 x3).
Apply H4 with
λ x5 x6 . and (and (setsum (proj0 x6) (proj1 x6) = x6) (In (proj0 x6) x0)) (In (proj1 x6) (x1 (proj0 x6))).
Apply unknownprop_e2d9dae0ea3a0bd6555cf6ae3b66e91e8730bfc402bf8dbafcc7b19c9adfb426 with
x3,
x4,
λ x5 x6 . and (and (setsum x6 (proj1 (setsum x3 x4)) = setsum x3 x4) (In x6 x0)) (In (proj1 (setsum x3 x4)) (x1 x6)).
Apply unknownprop_d4bb68cbfba730ad1b1ee2c6901fadf3c573cb615fac3296f9bb52128e37668a with
x3,
x4,
λ x5 x6 . and (and (setsum x3 x6 = setsum x3 x4) (In x3 x0)) (In x6 (x1 x3)).
Apply unknownprop_c7bf67064987d41cefc55afb6af6ecbbb6b830405f2005e0def6e504b3ca3bf3 with
setsum x3 x4 = setsum x3 x4,
In x3 x0,
In x4 (x1 x3) leaving 3 subgoals.
Let x5 of type ι → ι → ο be given.
The subproof is completed by applying H5.
The subproof is completed by applying H1.
The subproof is completed by applying H3.