{A B : Type} (P : A -> Type) (Q : B -> Type) (f : A -> B -> A) (Hf : forall x y, P x -> Q y -> P (f x y)) (acc : A) (Ha : P acc) (l : list B) (Hl : for_all Q l) : P (fold_left f l acc). Proof. revert acc Ha Hl; simple_list_induction l x l IHl; intros acc Ha Hl. - exact Ha. - simpl. destruct Hl as [Qx Hl]. apply IHl; auto. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum