fact: Record pre_graph := { vset : {fset VT}; eset : {fset ET}; endpt : bool -> ET -> VT; lv : VT -> Lv; le : ET -> Le; p_in : VT; p_out : VT }.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)