proposition: Lemma flatten_map_eq : forall (A B : Type)(ls : list (list A))(f : A -> B), map f (flatten ls) = flatten (map (fun ls' => map f ls') ls).
proof: Proof. induction ls; intuition; simpl in *. rewrite map_app. f_equal; eauto. Qed.
imports: FCF.FCF Permutation