proposition: Lemma image_Intersection: forall {A B: Type} (X Y: Ensemble A) (f: A -> B), Included (image_set (Intersection _ X Y) f) (Intersection _ (image_set X f) (image_set Y f)).
proof: Proof. intros. unfold Included, In; intros y. rewrite !Intersection_spec, !image_set_spec. intros [x [? ?]]. rewrite Intersection_spec in H. split; exists x; tauto. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Equivalence Coq.Sets.Ensembles Coq.Sets.Constructive_sets CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext