proposition: Lemma filter_ext : forall f f', compat_bool E.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. do 2 (rewrite filter_iff; auto). - rewrite Hff', Hss'; intuition. - repeat red; intros; rewrite <- 2 Hff'; auto. Qed.
imports: DecidableTypeEx FSetInterface