Lemma length_map {A B: UU} (l: list A) (f: A → B): length (map f l) = length l. Proof. revert l. apply list_ind. - apply idpath. - intros x xs HPind. change (map f (x :: xs)) with (f x :: map f xs). change (S (length (map f xs)) = S(length xs)). apply maponpaths. exact HPind. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.