An exact proof term for the current goal is (andER (topology_on X Tx) (¬ (∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V)) H).