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; intros. - split; intuition; inv. - destruct (f a) eqn:F; rewrite !InA_cons, ?IHs; intuition. + setoid_replace x with a; auto. + setoid_replace a with x in F; auto; congruence. Qed.
imports: MSetInterface OrdersFacts OrdersLists