proposition: Lemma filter_equal : forall f, compat_bool E.eq f -> forall s s', s[=]s' -> filter f s [=] filter f s'.
proof: Proof. unfold Equal; intros; repeat rewrite filter_iff; auto; rewrite H0; tauto. Qed.
imports: DecidableTypeEx FSetInterface