proposition: Lemma filter_iff : compat_bool E.eq f -> (In x (filter f s) <-> In x s /\ f x = true).
proof: Proof. split; [split; [apply filter_1 with f | apply filter_2 with s] | destruct 1; apply filter_3]; auto. Qed.
imports: DecidableTypeEx FSetInterface