Let X be given.

Let T be given.

Let U be given.

Assume Htop HU.

We will prove closed_in X T (X ∖ U).

Apply (closed_inI X T (X ∖ U)) to the current goal.

An exact proof term for the current goal is Htop.

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

We use U to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HU.

Use reflexivity.

∎