Let X be given.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ X ∖ Empty.

An exact proof term for the current goal is (setminusE1 X Empty x Hx).

Let x be given.

Assume HxX: x ∈ X.

An exact proof term for the current goal is (setminusI X Empty x HxX (EmptyE x)).

∎