Lemma h1map_idfun {A: UU} {n: nat} {v: vec A n} {P: A → UU} (h1v: hvec (vec_map P v)) : h1map (λ a: A, idfun (P a)) h1v = h1v. Proof. revert n v h1v. refine (vec_ind _ _ _). - induction h1v. apply idpath. - simpl. intros x n xs IHxs h1v. change h1v with (pr1 h1v ::: pr2 h1v). apply maponpaths. apply (IHxs (pr2 h1v)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.