{A B C} (f : A -> B) (g : B -> C) (l : list A) : list_map (fun x => g (f x)) l = list_map g (list_map f l). Proof. induction l as [|a l IHl]. 1: reflexivity. simpl; f_ap. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum