proposition: Lemma sepatates_cp (G : sgraph) (x y z : G) : separates x y [set z] -> z \in cp x y :\: [set x; y].
proof: Proof. case. rewrite !inE ![z == _]eq_sym => /negbTE-> /negbTE-> /= H. apply/cpP => p. by case: (H p) => z' Hz /set1P <-. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph minor) GraphTheory(checkpoint connectivity excluded set_tac)