Definition foldr1_map_ind {A B : UU} (f : B -> B -> B) (b : B) (h : A -> B) (P : list A -> B -> UU) (P0 : P nil b) (P1 : ∏ a, P (cons a nil) (h a)) (P2 : ∏ a1 xs a2 res, P (cons a1 xs) res -> P (cons a2 (cons a1 xs)) (f (h a2) res)) (xs : list A) : P xs (foldr1_map f b h xs). Proof. revert xs. induction xs as [[|n] xs]. - induction xs. apply P0. - induction n as [|n IH]. + induction xs as [m []]. apply P1. + induction xs as [m [k xs]]. assert (IHinst := IH (k,,xs)). exact (P2 k (n,,xs) m (foldr1_map f b h (S n,, k,, xs)) IHinst). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.