Definition foldr1_map_ind_nodep {A B : UU} (f : B -> B -> B) (b : B) (h : A -> B) (P : B -> UU) (P0 : P b) (P1 : ∏ a, P (h a)) (P2 : ∏ a res, P res -> P (f (h a) res)) (xs : list A) : P (foldr1_map f b h xs). Proof. set (Pdep := fun (_ : list A) (res : B) => P res). apply (foldr1_map_ind f b h Pdep). - exact P0. - exact P1. - intros a1 xs' a2 res H. apply P2. exact H. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.