proposition: Lemma In_filter : forall (A : Type) (x:A) f l, In x (filter f l) <-> In x l /\ f x = true.
proof: Proof. induction l; intros; simpl. - split; auto; intros. destruct H; auto. - destruct (f a) eqn:?. * simpl; split; intros; intuition (subst; eauto). * split; intros; intuition eauto; congruence. Qed.
imports: Coq(List Permutation)