proposition: Lemma filter_subset : forall f, compat_bool E.eq f -> forall s s', s[<=]s' -> filter f s [<=] filter f s'.
proof: Proof. unfold Subset; intros; rewrite filter_iff in *; intuition. Qed.
imports: DecidableTypeEx FSetInterface