fact: Definition app_sig {A B: Type} (P: A -> Prop) (f: A -> B): sig P -> B := fun a => f (proj1_sig a).
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