Let X and F be given.

Assume HinfX: infinite X.

Assume HfinF: finite F.

We prove the intermediate claim HinfXF: infinite (X ∖ F).

An exact proof term for the current goal is (infinite_setminus_finite X F HinfX HfinF).

An exact proof term for the current goal is (infinite_nonempty (X ∖ F) HinfXF).

∎