proposition: Lemma filter_spec : forall (s : t) (x : elt) (f : elt -> bool), Proper (X.eq==>eq) f -> (In x (filter f s) <-> In x s /\ f x = true).
proof: Proof. induction s; simpl. - intuition; inv. - intros. destruct (f a) eqn:E; rewrite ?InA_cons, IHs; intuition. + setoid_replace x with a; auto. + setoid_replace a with x in E; auto. congruence. Qed.
imports: MSetInterface