Let X be given.

Assume H1: X ⊆ Empty.

Apply set_ext to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is (Subq_Empty X).

∎