proposition: Proposition irredundantP: reflect {in D, forall v, (private_set v != set0)} irredundant.
proof: Proof. rewrite /irredundant ; apply: (iffP forallP). - move=> H1 v vinD. by move/implyP: (H1 v) => /(_ vinD). - move=> H2 v. apply/implyP=> vinD. by move: (H2 v vinD). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)