proposition: Lemma not_set_Exists_Forall P `{dec : ∀ x, Decision (P x)} X : ¬set_Exists P X → set_Forall (not ∘ P) X.
proof: Proof. by destruct (set_Forall_Exists_dec (not ∘ P) P (λ x, swap_if (decide (P x))) X). Qed.
imports: stdpp(relations) stdpp(options)