proposition: Lemma privateP v w : reflect (v -*- w /\ {in D, forall u, u -*- w -> u = v}) (w \in private_set v).
proof: Proof. apply: (iffP setDP); rewrite !in_cln => -[v_dom_w H]; split => //. - move => u inD u_dom_w; apply: contraNeq H => uDv. apply/bigcupP; exists u; by [exact/setD1P|rewrite in_cln]. - apply/negP => /bigcupP [u /setD1P [uDv /H]]. rewrite in_cln => X {}/X. exact/eqP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)