proposition: Lemma image_Disjoint_rev: forall {A B: Type} (X Y: Ensemble A) (f: A -> B), Disjoint _ (image_set X f) (image_set Y f) -> Disjoint _ X Y.
proof: Proof. intros. rewrite Disjoint_spec in *. intros x ? ?. apply (H (f x)); constructor; auto. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Equivalence Coq.Sets.Ensembles Coq.Sets.Constructive_sets CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext