Let X, Y and x be given.
Assume H: x ∈ X.
We will prove Inj0 x ∈ {Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y}.
Apply binunionI1 to the current goal.
We will prove Inj0 x ∈ {Inj0 x|x ∈ X}.
Apply ReplI to the current goal.
An exact proof term for the current goal is H.
∎