fact: Definition is_rev_fun {A B: Type} (P: A -> Prop) (f: A -> B) (g: B -> option A) := forall b, match g b with | Some a0 => P a0 /\ forall a, P a -> (f a = b <-> a = a0) | None => forall a, P a -> f a <> b end.
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