Definition h1lower {A: UU} {n: nat} {v: vec A n} {B: UU} (h1v: hvec (vec_map (λ _, B) v)) : vec B n. Proof. revert n v h1v. refine (vec_ind _ _ _). - apply idfun. - intros x n xs IHxs h1v. exact (vcons (hhd h1v) (IHxs (htl h1v))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.