proposition: Lemma induced_rmapP : minor_rmap induced_rmap.
proof: Proof. split. - move=> ?; exact: set10. - move=> ?; exact: connected1. - by move=> ? ?; rewrite disjoints1 inE val_eqE. - by move=> ? ?; rewrite neighbor11. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)