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