proposition: Lemma map_map : forall A B C (l:list A) (f:A->B) (g:B->C), map g (map f l) = map (fun x => g (f x)) l.
proof: Proof. Proof using. intros. induction l as [|x l']. { auto. } { repeat rewrite map_cons. fequals. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)