proposition: Lemma minorRE G H : minor G H -> exists phi : H -> {set G}, minor_rmap phi.
proof: Proof. case => phi /minor_rmap_map D. eexists. exact: D. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)