Let X and x be given.

Assume H: x ∈ X.

rewrite the current goal using (Inj1_eq X) (from left to right).

We will prove Inj1 x ∈ {0} ∪ {Inj1 x|x ∈ X}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is (ReplI X Inj1 x H).

∎