Definition hel {n: nat} {v: vec UU n} (hv: hvec v): ∏ i: ⟦ n ⟧, el v i. Proof. revert n v hv. refine (vec_ind _ _ _). - intros. apply (fromempty (negnatlthn0 (pr1 i) (pr2 i))). - intros x n xs IHxs. induction i as [i iproof]. induction i. + exact (hhd hv). + exact (IHxs (htl hv) (make_stn _ i iproof)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.