Lemma vec_map_const {A: UU} {n: nat} {v: vec A n} {B: UU} (b: B) : vec_map (λ _, b) v = vec_fill b n. Proof. revert n v. apply vec_ind. - apply idpath. - intros x n xs HPind. change (b ::: vec_map (λ _: A, b) xs = b ::: vec_fill b n). apply maponpaths. exact HPind. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.