Let X be given.

Apply set_ext to the current goal.

An exact proof term for the current goal is setminus_Subq X Empty.

Let u be given.

Assume Hu: u ∈ X.

Apply setminusI to the current goal.

An exact proof term for the current goal is Hu.

An exact proof term for the current goal is EmptyE u.

∎