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