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