proposition: 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: Proof. etrans. { apply el_vec_map. } use maponpaths. use el_vec_fill. Defined.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers