Lemma vec_map_id {A : UU} {n} (v: vec A n) : vec_map (idfun A) v = v. Proof. revert n v. refine (vec_ind _ _ _). - apply idpath. - intros x n xs HPxs. simpl. apply maponpaths. apply HPxs. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.