fact: Record LabeledGraph {DV DE DG: Type} := { pg_lg: PreGraph; vlabel: Vertex -> DV; elabel: Edge -> DE; glabel: DG }.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext