proposition: Lemma exists_mem_3: forall s x, mem x s=true -> f x=true -> exists_ f s=true.
proof: Proof. intros. rewrite for_all_exists; auto. rewrite negb_true_iff. apply for_all_mem_3 with x;auto. rewrite negb_false_iff; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx