fact: Record iso (F G: graph): Type@{S} := Iso { iso_v:> bij F G; iso_e: bij (edge F) (edge G); iso_d: edge F -> bool; iso_ihom: is_ihom iso_v iso_e iso_d }.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)