Definition foldr {B : UU} (f : A -> B -> B) (b : B) : list -> B := list_ind (λ _, B) b (λ a _ b', f a b').
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.