proposition: Lemma smerge2_separator (G : sgraph) (x y : G) (S : {set smerge2 G x y}) : vseparator S -> vseparator (y |: val @: S).
proof: Proof. move => [u[v [uNS vNS sep_uv]]]. exists (val u),(val v); split => [||p]. - rewrite !inE (negbTE (valP u)) /= mem_imset //; exact: val_inj. - rewrite !inE (negbTE (valP v)) /= mem_imset //; exact: val_inj. - have [|yNp] := boolP (y \in p); first by exists y => //; rewrite !inE eqxx. have [|//||q eq_q _] := lift_Path (p' := p). + exact: smerge2_edge. + move => z z_p. have zDy : z != y by apply: contraTneq z_p => ->. by apply/mapP; exists (Sub z zDy) => //; rewrite mem_enum. + have [z z_q z_S] := sep_uv q; exists (val z); last by rewrite !inE mem_imset ?z_S. by rewrite mem_path -eq_q mem_map. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)