proposition: 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: 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.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers