fixup! foldl-cong: don't take d ≡ e

Author: mildsunrise

CHANGELOG.md

@@ -323,7 +323,7 @@ Additions to existing modules
   mapMaybe-cong         : f ≗ g → mapMaybe f ≗ mapMaybe g
   zipWith-cong          : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as
   unzipWith-cong        : f ≗ g → unzipWith f ≗ unzipWith g
-  foldl-cong            : (∀ x y → f x y ≡ g x y) → d ≡ e → foldl f d ≗ foldl g e
+  foldl-cong            : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x
   alignWith-flip        : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs
   alignWith-comm        : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs
   align-flip            : align xs ys ≡ map swap (align ys xs)

src/Data/List/Properties.agda

@@ -696,11 +696,10 @@ module _ {P : Pred A p} {f : A → A → A} where
 ------------------------------------------------------------------------
 -- foldl
 
-foldl-cong : ∀ {f g : B → A → B} {d e : B} →
-             (∀ x y → f x y ≡ g x y) → d ≡ e →
-             foldl f d ≗ foldl g e
-foldl-cong f≗g refl []      = refl
-foldl-cong f≗g d≡e (x ∷ xs) rewrite d≡e = foldl-cong f≗g (f≗g _ x) xs
+foldl-cong : ∀ {f g : B → A → B} → (∀ x y → f x y ≡ g x y) →
+             ∀ x → foldl f x ≗ foldl g x
+foldl-cong f≗g x []       = refl
+foldl-cong f≗g x (y ∷ xs) rewrite f≗g x y = foldl-cong f≗g _ xs
 
 foldl-++ : ∀ (f : A → B → A) x ys zs →
            foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs