Definition h2map {A: UU} {n: nat} {v: vec A n} {P: A → UU} {h1v: hvec (vec_map P v)} {Q: ∏ (a: A) (p: P a), UU} {R: ∏ (a: A) (p: P a), UU} (f: ∏ (a: A) (p: P a), Q a p → R a p) (h2v: hvec (h1map_vec Q h1v)) : hvec (h1map_vec R h1v). Proof. revert n v f h1v h2v. refine (vec_ind _ _ _ ). - intros. exact [()]. - intros x n xs IHv f h1v h2v. exact (f x (pr1 h1v) (pr1 h2v) ::: IHv f (pr2 h1v) (pr2 h2v)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.