Lemma foldr1_cons {A : UU} (f : A -> A -> A) (a : A) (x y : A) (xs : list A) : foldr1 f a (cons x (cons y xs)) = f x (foldr1 f a (cons y xs)). Proof. apply idpath. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.