Definition vec_foldr {A B : UU} (f : A -> B -> B) (b : B) {n} : vec A n -> B := vec_ind (λ (n : nat) (_ : vec A n), B) b (λ (a : A) (m : nat) (_ : vec A m) (acc : B), f a acc) n.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.