proposition: Lemma is_guarded_inj_single {A B: Type} {EqB: EqDec B eq} (f: A -> B) (a: A): is_guarded_inj (eq a) f.
proof: Proof. intros. exists (fun b => if equiv_dec (f a) b then Some a else None). intro b. destruct_eq_dec (f a) b. + split; auto. intros; subst. tauto. + intros; subst. auto. Qed.
imports: Coq.Relations.Relation_Definitions Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.Relation_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext