diff --git a/CHANGELOG.md b/CHANGELOG.md
index f7a79c72b0bfda539f125b660160d7fb8298141d..d0f2c9485fe0b5acb3332dca1a5d12506e398a63 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -81,6 +81,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   and either affine or absorbing.
 * Fix the statement of the lemma `fupd_plainly_laterN`; the old lemma was a
   duplicate of `fupd_plain_laterN`.
+* Strengthen `big_sepL2_app_inv` by weakening a premise (it is sufficient for
+  one of the two pairs of lists to have equal length).
 
 **Changes in `proofmode`:**