fact: Definition NodePred := {P : Vertex -> Prop & forall x, {P x} + {~ P x}}.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext