proposition: Lemma filter_2 : forall s x f, @compat_bool elt E.eq f -> In x (filter f s) -> f x = true.
proof: Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface