proposition: Lemma map_flatten : forall {B C} (f: B -> C) (xs: list (list B)), map f (flatten xs) = flatten (map (fun x => map f x) xs).
proof: Proof. induction xs; simpl; [ | rewrite map_app, IHxs ]; reflexivity. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Fiat.Common Coq.Arith.Arith