fact: 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.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers