Lemma el_vec_map_vec_fill {A B : UU} (f : A → B) {n} (a:A) (i : ⟦ n ⟧) : el (vec_map f (vec_fill a n)) i = f a. Proof. etrans. { apply el_vec_map. } use maponpaths. use el_vec_fill. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.