proposition: Lemma filter_cons : forall (A : Set)(P : A -> bool)(ls : list A) a, filter P (a :: ls) = if (P a) then (a :: (filter P ls)) else (filter P ls).
proof: Proof. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation