Lemma map_const {A B: UU} (b: B) (l: list A): map (λ _, b) l = fill b (length l). Proof. revert l. apply list_ind. - apply idpath. - intros x xs HPind. change (b :: map (λ _: A, b) xs = b :: fill b (length xs)). apply maponpaths. exact HPind. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.