proposition: Lemma topological_property_T0_sep : topological_property T0_sep.
proof: Proof. intros X Y f [g Hcont_f Hcont_g Hgf Hfg] Hsep x y neq. destruct (Hsep (g x) (g y)) as [[U [Hopen [Hin H']]] | [U [Hopen [H' Hin]]]]; [ shelve | left | right ]; exists (inverse_image g U); repeat split; try apply Hcont_g; assumption + (intros [?]; contradiction). Unshelve. intro contra. eapply f_equal in contra. rewrite Hfg, Hfg in contra. contradiction. Qed.
imports: Coq(Program.Subset) Topology(Homeomorphisms SubspaceTopology)