{A B : Type} (f : A -> B) (l : list A) : length (list_map f l) = length l. Proof. induction l as [|x l IHl] using list_ind. - reflexivity. - simpl. exact (ap S IHl). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum