diff --git a/CHANGELOG.md b/CHANGELOG.md
index 768bf1001e50a7477a00ab99bf54d5930eb9619c..2aaa768eb7eb84f0713b9fa719b00cf8e1aee0a2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -28,6 +28,12 @@ Coq 8.11 is no longer supported in this version of Iris.
   is not very well-behaved.
 * Extend `gmap_view` with lemmas for "big" operations on maps.
 
+**Changes in `bi`:**
+
+* Add new lemmas `big_sepM2_delete_l` and `big_sepM2_delete_r`.
+* Rename `big_sepM2_lookup_1` → `big_sepM2_lookup_l` and
+  `big_sepM2_lookup_2` → `big_sepM2_lookup_r`.
+
 **Changes in `proofmode`:**
 
 * Add support for pure names `%H` in intro patterns. This is now natively
@@ -77,6 +83,8 @@ s/\b(auth|view)_(auth|both|update)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_va
 s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
 s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
 s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
+s/\bbig_sepM2_lookup_1\b/big_sepM2_lookup_l/g
+s/\bbig_sepM2_lookup_2\b/big_sepM2_lookup_r/g
 EOF
 ```