proposition: Lemma list_map_compose : forall A B C (f : A -> B) (g : B -> C) l, LibList.map g (LibList.map f l) = LibList.map (g \o f) l.
proof: Proof. Proof using. introv. induction l. reflexivity. rew_listx. fequals~. Qed.
imports: TLC(LibTactics LibLogic LibContainer LibSet)