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