proposition: Lemma induced_separates (V : {set G}) (S : {set induced V}) (x y : induced V) : separates x y S -> separates (val x) (val y) (val @: S :|: ~:V).
proof: Proof. case => xS yS sepS. split => [||p]; rewrite ?inE ?negb_or ?negbK ?mem_imset ?xS ?yS ?(valP x) ?(valP y) //=. case: (boolP (p \subset V)) => [/subsetP subA|/subsetPn [z Z1 Z2]]; last first. by exists z; rewrite ?inE ?Z1 ?Z2. have [q nodes_q] := Path_to_induced subA. have [z Z1 Z2] := sepS q. exists (val z); by [rewrite mem_path -nodes_q map_f|rewrite !inE mem_imset ?Z2]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)