Lemma el_vec_map {A B : UU} (f : A → B) {n} (v : vec A n) (i : ⟦ n ⟧) : el (vec_map f v) i = f (el v i). Proof. induction n as [|m H]. - exact (fromstn0 i). - induction i as (j, jlt). induction j as [|k _]. + apply hd_vec_map. + change (el (tl (vec_map f v)) (make_stn _ k jlt) = f (el (tl v) (make_stn _ k jlt))). use H. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.