From cf6aa554b3e59a67243be49babbd88c19c108724 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 8 Sep 2024 13:01:33 +0200
Subject: [PATCH] CHANGELOG.

---
 CHANGELOG.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b8dc778c..fc289dd2 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
 ```
 
-- 
GitLab