proposition: Lemma bagP (U : {set G}) x z : reflect (forall y, y \in CP U -> x \in cp z y) (z \in bag U x).
proof: Proof. rewrite /bag -lock inE. exact: (iffP forall_inP). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)