Let X and A be given.

Assume HcountX: countable X.

We will prove countable (X ∖ A).

Apply (Subq_countable (X ∖ A) X HcountX) to the current goal.

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

∎