proposition: 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: 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.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers