proposition: Lemma add_filter_2 : forall s s' x, f x=false -> (Add x s s') -> filter f s [=] filter f s'.
proof: Proof. unfold Add, MP.Add, Equal; intros. repeat rewrite filter_iff; auto. rewrite H0; clear H0. intuition. setoid_replace x with a in H; auto. congruence. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx