proposition: Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true.
proof: Proof. intros x l; induction l as [|a ? ?]; simpl. - tauto. - intros. case_eq (f a); intros; simpl; intuition congruence. Qed.
imports: PeanoNat