proposition: Lemma for_all_mem_3: forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.
proof: Proof. intros. apply (bool_eq_ind (for_all f s));intros;auto. rewrite for_all_filter in H1; auto. rewrite is_empty_equal_empty in H1. generalize (equal_mem_2 _ _ H1 x). rewrite filter_b; auto. rewrite empty_mem. rewrite H. rewrite H0. simpl;auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx