diff --git a/CHANGELOG.md b/CHANGELOG.md
index b8dc778c1e5303a0ebd4e1de94d2e6f70c93fa51..fc289dd2dd9838e10798d814b4883f5aecfaa49b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -47,6 +47,10 @@ API-breaking change is listed.
   open `string_scope`.
 - Add lemmas `Sorted_unique_strong` and `StronglySorted_unique_strong` that only
   require anti-symmetry for the elements that are in the list.
+- Rename `foldr_cons_permute` into `foldr_cons_permute_strong` and strengthen
+  (a) from function `f : A → A → A` to `f : A → B → B`, and (b) to only require
+  associativity/commutativity for the elements that are in the list.
+- Rename `foldr_cons_permute_eq` into `foldr_cons_permute`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -102,6 +106,9 @@ s/\bminimal_exists\b/minimal_exists_elem_of/g
 s/\bmap_not_Forall2\b/map_not_relation/g
 # map_fold
 s/\bmap_fold_ind2\b/map_fold_weak_ind/g
+# foldr_cons_permute
+s/\bfoldr_cons_permute\b/foldr_cons_permute_strong/g
+s/\bfoldr_cons_permute_eq\b/foldr_cons_permute/g
 EOF
 ```
 
diff --git a/stdpp/list.v b/stdpp/list.v
index cc575d69b64146d28567e4b9575265ee6e60eadc..a9b537ab392c0045c2d3b46551e8e131367679c6 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -4674,19 +4674,25 @@ Proof.
   intros a1 a2 b.
   by rewrite (assoc f), (comm f _ b), (assoc f), (comm f b), (comm f _ a2).
 Qed.
-Lemma foldr_cons_permute {A} (R : relation A) `{!PreOrder R}
-    (f : A → A → A) (a : A)
-    `{!∀ a, Proper (R ==> R) (f a), !Assoc R f, !Comm R f} x l :
-  R (foldr f a (x :: l)) (foldr f (f x a) l).
+
+Lemma foldr_cons_permute_strong {A B} (R : relation B) `{!PreOrder R}
+    (f : A → B → B) (b : B) `{!∀ a, Proper (R ==> R) (f a)} x l :
+  (∀ j1 a1 j2 a2 b,
+    j1 ≠ j2 → (x :: l) !! j1 = Some a1 → (x :: l) !! j2 = Some a2 →
+    R (f a1 (f a2 b)) (f a2 (f a1 b))) →
+  R (foldr f b (x :: l)) (foldr f (f x b) l).
 Proof.
-  rewrite <-foldr_snoc.
-  eapply foldr_permutation_proper'; [done..|].
-  rewrite Permutation_app_comm. done.
+  intros. rewrite <-foldr_snoc.
+  apply (foldr_permutation _ f b); [done|]. by rewrite Permutation_app_comm.
 Qed.
-Lemma foldr_cons_permute_eq {A} (f : A → A → A) (a : A)
-    `{!Assoc (=) f, !Comm (=) f} x l :
+Lemma foldr_cons_permute {A} (f : A → A → A) (a : A) x l :
+  Assoc (=) f →
+  Comm (=) f →
   foldr f a (x :: l) = foldr f (f x a) l.
-Proof. eapply (foldr_cons_permute eq); apply _. Qed.
+Proof.
+  intros. apply (foldr_cons_permute_strong (=) f a).
+  intros j1 a1 j2 a2 b _ _ _. by rewrite !(assoc_L f), (comm_L f a1).
+Qed.
 
 Lemma foldr_comm_acc_strong {A B} (R : relation B) `{!PreOrder R}
     (f : A → B → B) (g : B → B) b l :