diff --git a/CHANGELOG.md b/CHANGELOG.md
index e926aad99efc4141c103ad5bd532df24a14c6b03..117be49b1478850974bd56bc1893d9a655c228fa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -75,6 +75,9 @@ Coq 8.13 is no longer supported.
   - Add some `apply bi.entails_wand`/`apply bi.wand_entails` to 'convert'
     between the old and new way of interpreting `P -∗ Q`.
 * Add `auto` hint to introduce the BI version of `↔`.
+* Change `big_sepM2_alt` to use `dom m1 = dom2 m2` instead of
+  `∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)`. The old lemma is still
+  available as `big_sepM2_alt_lookup`.
 
 **Changes in `proofmode`:**
 
@@ -148,6 +151,8 @@ s/\bloc_add(_assoc|_0|_inj|)\b/Loc.add\1/g
 s/\bfresh_locs(_fresh|)\b/Loc.fresh\1/g
 # unseal
 s/\bMonPred\.unseal\b/monPred\.unseal/g
+# big op
+s/\bbig_sepM2_alt\b/big_sepM2_alt_lookup/g
 EOF
 ```