proposition: Lemma induced_vseparator (G : sgraph) (A : {set G}) (S : {set induced A}) : vseparator S -> vseparator (val @: S :|: ~: A).
proof: Proof. by move => [x] [y] /induced_separates ?; exists (val x); exists (val y). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)