Let X be given.

Assume H1: ∀x, x ∉ X.

Apply Empty_Subq_eq to the current goal.

Let x be given.

Assume H2: x ∈ X.

We will prove False.

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

∎