proposition: Lemma el_make_vec {n} (f : ⟦ n ⟧ → A) : el (make_vec f) ~ f .
proof: 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.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers