fact: Definition minor_rmap (G H : sgraph) (phi : H -> {set G}) := [/\ (forall x : H, phi x != set0), (forall x : H, connected (phi x)), (forall x y : H, x != y -> [disjoint phi x & phi y]) & (forall x y : H, x -- y -> neighbor (phi x) (phi y))].
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)