Lemma make_vec_el {n} (v : vec A n) : make_vec (el v) = v. Proof. apply vec_extens. intros i. rewrite el_make_vec. reflexivity. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.