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