Definition h1foldr {A: UU} {n: nat} {v: vec A n} {P: A → UU} {B: UU} (comb: ∏ (a: A), P a → B → B) (s: B) (h1v: hvec (vec_map P v)): B. Proof. revert n v h1v. refine (vec_ind _ _ _). - intro. exact s. - intros x n xs IHxs. simpl. intro. exact (comb _ (pr1 h1v) (IHxs (pr2 h1v))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets.