proposition: Lemma fold_preserves {A B} P Q (f : A -> B -> A) (Hf : forall x y, P x -> Q y -> P (f x y)) : forall acc (Ha : P acc) l (Hl : for_all Q l), P (fold_left f acc l).
proof: Proof. intros acc Ha l Hl;revert l Hl acc Ha. intros l;induction l as [|x l IHl]. - intros _ acc Ha. exact Ha. - simpl. intros [Hx Hl] acc Ha. apply IHl;auto. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra