proposition: Lemma strict_is_minor (G H : sgraph) : strict_minor G H -> minor G H.
proof: Proof. move => [phi A]. exists (Some \o phi). exact: map_of_total. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)