proposition: Lemma concat_map : forall A B (f : A -> B) l, map f (concat l) = concat (map (map f) l).
proof: Proof. intros A B f l; induction l as [|x l IH]; simpl. - reflexivity. - rewrite map_app, IH; reflexivity. Qed.
imports: PeanoNat