Definition vec_foldr1 {A : UU} (f : A -> A -> A) {n} : vec A (S n) → A := nat_rect (λ n : nat, vec A (S n) → A) hd (λ (m : nat) (h : vec A (S m) → A), uncurry (λ (x : A) (u : vec A (S m)), f x (h u))) n.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.