Definition foldr1_map {B : UU} (f : B -> B -> B) (b : B) (h : A -> B) : list → B. Proof. apply list_ind. - exact b. - intros a' l fl. revert l. apply list_ind. + exact (h a'). + intros _ _ _. exact (f (h a') fl). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.