proposition: Fact minor_of_rmap (G H : sgraph) (phi : H -> {set G}): minor_rmap phi -> minor G H.
proof: Proof. move/minor_map_rmap. exact: minor_of_map. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)