An exact proof term for the current goal is (infinite_setminus_finite X {y} HinfX (Sing_finite y)).