proposition: Lemma separatorP (A B S : {set G}) : reflect (separator A B S) (separatorb A B S).
proof: Proof. rewrite /separatorb. apply: (iffP forall_inP) => [H|H a aA]. - apply: separatorI => a b p Ip aA bB. move/(_ _ aA) : H => /forall_inP /(_ _ bB) /forallP /(_ (Sub p Ip)) /exists_inP [s sS in_p]. by exists s. - apply/forall_inP => b bB. apply/forallP => [[p ?]]. apply/exists_inP. case: (H a b p) => // s S1 S2. by exists s. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)