proposition: Lemma filter_3 : forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s).
proof: Proof. intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition. generalize (Hiff (compat_P_aux H)); firstorder. Qed.
imports: FSetInterface