Let X, a and b be given.

Assume HinfX: infinite X.

An exact proof term for the current goal is (infinite_setminus_finite X (UPair a b) HinfX (finite_UPair a b)).

∎