proposition: Lemma rmap_disjE (G H : sgraph) (phi : H -> {set G}) x i j : minor_rmap phi -> x \in phi i -> x \in phi j -> i=j.
proof: Proof. move => [_ _ map _] xi. apply contraTeq => iNj. by erewrite (disjointFr (map _ _ iNj)). Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)