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