proposition: Lemma induced_rmap_sub u : induced_rmap u \subset S.
proof: Proof. by rewrite /induced_rmap sub1set; apply: (valP u). Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)