proposition: Lemma add_filter_1 : forall s s' x, f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
proof: Proof. unfold Add, MP.Add; intros. repeat rewrite filter_iff; auto. rewrite H0; clear H0. intuition. setoid_replace y with x; auto with relations. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx