Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 ∈ x0.
Apply Inj1_eq with
x0,
λ x2 x3 . Inj1 x1 ∈ x3.
Apply binunionI2 with
Sing 0,
{Inj1 x2|x2 ∈ x0},
Inj1 x1.
Apply ReplI with
x0,
Inj1,
x1.
The subproof is completed by applying H0.