proposition: Lemma separator_cap A B S : separator A B S -> A :&: B \subset S.
proof: Proof. move => sepS. apply/subsetP => x /setIP [xA xB]. case: (sepS _ _ (idp x)) => // s in_S. by rewrite mem_idp => /eqP <-. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)