proposition: Lemma filter_b : Proper (E.eq==>Logic.eq) f -> mem x (filter f s) = mem x s && f x.
proof: Proof. intros. generalize (mem_iff (filter f s) x)(mem_iff s x)(filter_iff s x H). destruct (mem x s); destruct (mem x (filter f s)); destruct (f x); simpl; intuition. Qed.
imports: DecidableTypeEx MSetInterface