proposition: Lemma map_map : forall (A B C : Set) (l : (list A)) (f : B -> C) (g : A ->B), map f (map g l) = map (fun x => f (g x)) l.
proof: Proof. intros A B C l f g; induction l as [ | x l]. trivial. simpl; rewrite IHl; trivial. Qed.
imports: List Arith