proposition: Lemma minor_map_rmap (G H : sgraph) (phi : H -> {set G}) : minor_rmap phi -> minor_map (fun x : G => [pick x0 : H | x \in phi x0]).
proof: Proof. set phi' := (fun x => _). case => P1 P2 P3 P4. have phiP x x0 : x0 \in phi x = (phi' x0 == Some x). { rewrite /phi'. case: pickP => [x' Hx'|]; last by move->. rewrite Some_eqE. apply/idP/eqP => [|<-//]. apply: contraTeq => /P3 D. by rewrite (disjointFr D Hx'). } split. - move => y. case/set0Pn : (P1 y) => y0. rewrite phiP => /eqP <-. by exists y0. - move => y x0 y0. rewrite !inE -!phiP => H1 H2. move: (P2 y _ _ H1 H2). apply: connect_mono => u v. by rewrite /= -!mem_preim !phiP. - move => x y /P4/neighborP [x0] [y0] [*]. exists x0;exists y0. by rewrite -!mem_preim -!phiP. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)