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