Let X be given.

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

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

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

∎