proposition: Lemma minor_rmap_map (G H : sgraph) (phi : G -> option H) : minor_map phi -> minor_rmap (fun x => [set y | phi y == Some x]).
proof: Proof. set phi' := fun _ => _. case => P1 P2 P3. split. - move => x. apply/set0Pn. case: (P1 x) => x0 H0. exists x0. by rewrite !inE H0. - move => x u v Hu Hv. move: (P2 x _ _ Hu Hv). apply: connect_mono => a b. by rewrite /= !inE. - move => x y. apply: contraNT => /pred0Pn [x0 /= /andP[]]. by rewrite -Some_eqE !inE => /eqP<-/eqP<-. - move => x y /P3 [x0] [y0] [*]. apply/neighborP. exists x0;exists y0. by rewrite !inE !mem_preim. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)