proposition: 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: Proof. revert xs. induction xs as [[|n] xs]. - induction xs. apply idpath. - induction n as [|n IH]. + induction xs as [m []]. apply idpath. + induction xs as [m [k xs]]. assert (IHinst := IH (k,,xs)). change (S (S n),, m,, k,, xs) with (cons m (cons k (n,,xs))). do 2 rewrite map_cons. rewrite foldr1_cons. change (S n,, k,, xs) with (cons k (n,,xs)) in IHinst. rewrite map_cons in IHinst. rewrite <- IHinst. apply foldr1_map_cons. Qed.
imports: UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors