proposition: Lemma is_guarded_inj_rev_aux {A B: Type} (P: A -> Prop) (f: A -> B) (g: B -> option A) (a: A): P a -> is_rev_fun P f g -> g (f a) = Some a.
proof: Proof. intros. specialize (H0 (f a)). destruct (g (f a)). + destruct H0. specialize (H1 a H). rewrite (proj1 H1) by auto. auto. + specialize (H0 a H). congruence. 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