proposition: Lemma is_guarded_inj_empty {A B: Type} (f: A -> B): is_guarded_inj (Empty_set _) f.
proof: Proof. intros. exists (fun v => None). intro b. intros. inv H. 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