Let x and y be given.

Assume H1: y ∈ x ∪ {x}.

Apply (binunionE x {x} y H1) to the current goal.

Assume H2: y ∈ x.

Apply orIL to the current goal.

An exact proof term for the current goal is H2.

Assume H2: y ∈ {x}.

Apply orIR to the current goal.

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

∎