Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply binunionE with
{Inj0 x3|x3 ∈ x0},
{Inj1 x3|x3 ∈ x1},
x2,
or (∃ x3 . and (x3 ∈ x0) (x2 = Inj0 x3)) (∃ x3 . and (x3 ∈ x1) (x2 = Inj1 x3)) leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1:
x2 ∈ {Inj0 x3|x3 ∈ x0}.
Apply orIL with
∃ x3 . and (x3 ∈ x0) (x2 = Inj0 x3),
∃ x3 . and (x3 ∈ x1) (x2 = Inj1 x3).
Apply ReplE with
x0,
Inj0,
x2.
The subproof is completed by applying H1.
Assume H1:
x2 ∈ {Inj1 x3|x3 ∈ x1}.
Apply orIR with
∃ x3 . and (x3 ∈ x0) (x2 = Inj0 x3),
∃ x3 . and (x3 ∈ x1) (x2 = Inj1 x3).
Apply ReplE with
x1,
Inj1,
x2.
The subproof is completed by applying H1.