proposition: Fact minor_of_map (G H : sgraph) (phi : G -> option H): minor_map phi -> minor G H.
proof: Proof. case => *. by exists phi. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)