Lemma el_make_vec {n} (f : ⟦ n ⟧ → A) : el (make_vec f) ~ f . Proof. intro i. induction n as [|m meq]. - exact (fromstn0 i). - induction i as (j,jlt). induction j as [|k _]. + cbn. apply maponpaths. apply stn_extens. apply idpath. + etrans. { apply meq. } unfold drop. apply maponpaths. apply idpath. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.