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