proposition: 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: Proof. apply vec_extens. intro i. rewrite el_vec_map. rewrite el_make_vec. apply idpath. Defined.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers