proposition: Lemma map_flat_map : forall {A B C} (f: B -> C) (g: A -> list B) (xs: list A), map f (flat_map g xs) = flat_map (fun x : A => map f (g x)) xs.
proof: Proof. intros; rewrite flat_map_flatten, map_flatten, map_map, <- flat_map_flatten; reflexivity. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Fiat.Common Coq.Arith.Arith