Lemma el_make_vec_fun {n} (f : ⟦ n ⟧ → A) : el (make_vec f) = f. Proof. apply funextfun. apply el_make_vec. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.