Let x0 of type ι be given.
Let x1 of type ι be given.
Apply pairE with
proj0 x0,
proj1 x0,
x1,
x1 ∈ x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply exandE_i with
λ x2 . x2 ∈ proj0 x0,
λ x2 . x1 = setsum 0 x2,
x1 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2:
x2 ∈ proj0 x0.
Apply H3 with
λ x3 x4 . x4 ∈ x0.
Apply proj0E with
x0,
x2.
The subproof is completed by applying H2.
Apply exandE_i with
λ x2 . x2 ∈ proj1 x0,
λ x2 . x1 = setsum 1 x2,
x1 ∈ x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2:
x2 ∈ proj1 x0.
Apply H3 with
λ x3 x4 . x4 ∈ x0.
Apply proj1E with
x0,
x2.
The subproof is completed by applying H2.