Definition el {n} (v : vec A n) : ⟦ n ⟧ → A. Proof. induction n as [|m f]. - apply (λ i, fromstn0 i). - intro i. induction i as (j,jlt). induction j as [|k _]. + exact (hd v). + exact (f (tl v) (k,, jlt)). Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.