proposition: Lemma length_map {A B: UU} (l: list A) (f: A → B): length (map f l) = length l.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe