Definition hel_h1map_vec {A: UU} {n: nat} {v: vec A n} {P: A → UU} {B: UU} (f: ∏ (a: A), P a → B) (hv: hvec (vec_map P v)) (i:⟦ n ⟧) : el (h1map_vec f hv) i = f (el v i) (eqweqmap (el_vec_map P v i) (hel hv i)). Proof. induction n as [|m IHn0]. + use fromstn0. exact i. + induction v as [vhead vtail]. induction hv as [hvhead hvtail]. induction i as [j jlt]. induction j as [| k]. - apply idpath. - use IHn0. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.