proposition: Lemma map_of_total (G H : sgraph) (phi : G -> H) : total_minor_map phi -> minor_map (Some \o phi).
proof: Proof. case => A B C. split => // y. case: (A y) => x <-. by exists x. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)