proposition: Lemma for_all_mem_1: forall s, (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.
proof: Proof. intros. rewrite for_all_filter; auto. rewrite is_empty_equal_empty. apply equal_mem_1;intros. rewrite filter_b; auto. rewrite empty_mem. generalize (H a); case (mem a s);intros;auto. rewrite H0;auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx