proposition: Lemma flatten_map_eq : forall (A B : Set)(ls : list A)(f : A -> B), flatten (map (fun a => (f a) :: nil) ls) = map f ls.
proof: Proof. induction ls; intuition; simpl in *. f_equal; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation