fact: Definition labeled_graph_equiv (g1 g2: Graph) := g1 ~=~ g2 /\ (forall v, vvalid g1 v -> vvalid g2 v -> vlabel g1 v = vlabel g2 v) /\ (forall e, evalid g1 e -> evalid g2 e -> elabel g1 e = elabel g2 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