Quantifier negation rules
~ foreach(x) ℙ(x) === exists(x)  ~ ℙ(x)
~ exists(x)  ℙ(x) === foreach(x) ~ ℙ(x)