diff --git a/CHANGELOG.md b/CHANGELOG.md
index a25e051f789583dafd45c18e8b4388e3a47b4f88..185bb7e8953b6a8bdeb8148a395c98973562fcdc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -70,6 +70,8 @@ Coq 8.13 is no longer supported.
   timeless hypotheses when proving an invariant (without an update).
 * Make `uPred.unseal` tactic more robust by using types to unfold the right
   BI projections.
+* Turn `internal_eq_entails` into a bi-implication.
+* Add lemmas to relate internal/external non-expansiveness and contractiveness.
 
 **Changes in `heap_lang`:**