proposition: Theorem filter_app : forall (A : Set)(ls1 ls2 : list A)(f : A -> bool), filter f (ls1 ++ ls2) = filter f ls1 ++ filter f ls2.
proof: Proof. induction ls1; intuition; simpl in *. case_eq (f a); intuition. rewrite <- app_comm_cons. f_equal. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation