Let X and y be given.

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

Assume H1: y ∈ {0} ∪ {Inj1 x|x ∈ X}.

We will prove y = 0 ∨ ∃x ∈ X, y = Inj1 x.

Apply (binunionE {0} {Inj1 x|x ∈ X} y H1) to the current goal.

Assume H2: y ∈ {0}.

Apply orIL to the current goal.

An exact proof term for the current goal is (SingE 0 y H2).

Assume H2: y ∈ {Inj1 x|x ∈ X}.

Apply orIR to the current goal.

We will prove ∃x ∈ X, y = Inj1 x.

An exact proof term for the current goal is (ReplE X Inj1 y H2).

∎