fact: Definition strong_evalid (pg: PreGraph) (e: Edge) : Prop := evalid pg e /\ vvalid pg (src pg e) /\ vvalid pg (dst pg e).
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext