proposition: Lemma filter_ext : forall f f', Proper (E.eq==>Logic.eq) f -> (forall x, f x = f' x) -> forall s s', s[=]s' -> filter f s [=] filter f' s'.
proof: Proof. intros f f' Hf Hff' s s' Hss' x. rewrite 2 filter_iff; auto. - rewrite Hff', Hss'; intuition. - red; red; intros; rewrite <- 2 Hff'; auto. Qed.
imports: DecidableTypeEx MSetInterface