fact: Definition subgraph_for := {| vertex := sub_vertex; edge := sub_edge; endpoint b e := Sub (endpoint b (val e)) (in_V b (valP e)); vlabel x := vlabel (val x); elabel e := elabel (val e); |}.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)