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