fact: Record graph (Lv Le : Type) : Type := Graph { vertex:> finType; edge: finType; endpoint: bool -> edge -> vertex; vlabel: vertex -> Lv; elabel: edge -> Le }.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)