Let x0 of type ι be given.
Apply set_ext with
setsum 0 x0,
Inj0 x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply setsum_Inj_inv with
0,
x0,
x1,
x1 ∈ Inj0 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1:
∃ x2 . and (x2 ∈ 0) (x1 = Inj0 x2).
Apply exandE_i with
λ x2 . x2 ∈ 0,
λ x2 . x1 = Inj0 x2,
x1 ∈ Inj0 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x2 ∈ 0.
Apply FalseE with
x1 = Inj0 x2 ⟶ x1 ∈ Inj0 x0.
Apply EmptyE with
x2.
The subproof is completed by applying H2.
Assume H1:
∃ x2 . and (x2 ∈ x0) (x1 = Inj1 x2).
Apply exandE_i with
λ x2 . x2 ∈ x0,
λ x2 . x1 = Inj1 x2,
x1 ∈ Inj0 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x2 ∈ x0.
Apply H3 with
λ x3 x4 . x4 ∈ Inj0 x0.
Apply Inj0I with
x0,
x2.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Apply exandE_i with
λ x2 . x2 ∈ x0,
λ x2 . x1 = Inj1 x2,
x1 ∈ setsum 0 x0 leaving 2 subgoals.
Apply Inj0E with
x0,
x1.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H1: x2 ∈ x0.
Apply H2 with
λ x3 x4 . x4 ∈ setsum 0 x0.
Apply Inj1_setsum with
0,
x0,
x2.
The subproof is completed by applying H1.