Lemma foldr1_foldr1_map {A B : UU} (f : B -> B -> B) (b : B) (h : A -> B) (xs : list A) : foldr1_map f b h xs = foldr1 f b (map h xs). Proof. set (P := fun xs res => res = foldr1 f b (map h xs)). apply (foldr1_map_ind f b h P). - apply idpath. - intro a. apply idpath. - intros a1 xs' a2 res H. red. do 2 rewrite map_cons. rewrite foldr1_cons. apply maponpaths. red in H. rewrite map_cons in H. exact H. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.