Lemma vec_map_as_make_vec {A B: UU} (f: A → B) {n} (v: vec A n) : vec_map f v = make_vec (λ i, f (el v i)). Proof. apply vec_extens. intro i. rewrite el_vec_map. rewrite el_make_vec. apply idpath. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.