diff --git a/CHANGELOG.md b/CHANGELOG.md
index f3bd2388a2e1ddd69c6ce2713ce67819110b6313..b05d3f0bf3110fe60057472b3bd318b6020089f9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -95,6 +95,12 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Better support for telescopes in the proof mode, i.e., all tactics should
   recognize and distribute telescopes now.
 * Remove namespace `N` from `is_lock`.
+* Make lemma `Excl_included` a bi-implication.
+* Add lemma `singleton_included : {[ i := x ]} ≼ ({[ i := y ]} ↔ x ≡ y ∨ x ≼ y`,
+  and rename existing asymmetric lemmas (with a singleton on just the LHS):
+  + `singleton_includedN` → `singleton_includedN_l`.
+  + `singleton_included` → `singleton_included_l`.
+  + `singleton_included_exclusive_l` → `singleton_included_exclusive`
 
 **Changes in heap_lang:**