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