proposition: Theorem filter_flatten : forall (A : Set)(ls : list (list A)) f, filter f (flatten ls) = flatten (map (filter f) ls).
proof: Proof. induction ls; intuition idtac; simpl in *. rewrite filter_app. f_equal. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation