fact: Definition minor_map (G H : sgraph) (phi : G -> option H) := [/\ (forall y : H, exists x : G, phi x = Some y), (forall y : H, connected (phi @^-1 Some y)) & (forall x y : H, x -- y -> exists x0 y0 : G, [/\ x0 \in phi @^-1 Some x, y0 \in phi @^-1 Some y & x0 -- y0])].
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)