proposition: Lemma image_single: forall {A B: Type} (a: A) (f: A -> B), Same_set (image_set (eq a) f) (eq (f a)).
proof: Proof. intros. rewrite Same_set_spec. intro x. rewrite image_set_spec. split; intros; eauto. destruct H as [? [? ?]]; subst; auto. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Equivalence Coq.Sets.Ensembles Coq.Sets.Constructive_sets CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext