fact: Record diso (F G: diGraph): Type := Diso { diso_v:> bij F G; diso_hom: is_dhom diso_v; diso_hom': is_dhom diso_v^-1 }.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)