proposition: Lemma filter_filter: forall A (f g: A->bool) l, filter f (filter g l) = filter (fun x => (andb (f x) (g x))) l.
proof: Proof. intros. induction l. reflexivity. unfold filter at 2 3. destruct (g a); simpl; destruct (f a); simpl; try apply f_equal; unfold filter in IHl at 2 3; rewrite IHl; reflexivity. Qed.
imports: Coq(Bool Arith Arith.Peano_dec Arith.Compare_dec List)