diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3853fde1690ea8e268ab7956ecda3c129f0d6197..13fa9bd61569a46e6a3216db2f544b2c0ea1a2aa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,13 +7,19 @@ Coq development, but not every API-breaking change is listed. Changes marked
This version accompanies the final ICFP paper.
-* [# algebra] Make the core of an RA or CMRA a partial function.
+* [algebra] Make the core of an RA or CMRA a partial function.
* [heap_lang] No longer use dependent types for expressions. Instead, values
carry a proof of closedness. Substitution, closedness and value-ness proofs
are performed by computation after reflecting into a term langauge that knows
about values and closed expressions.
* [program_logic/language] The language does not define its own "atomic"
predicate. Instead, atomicity is defined as reducing in one step to a value.
+* [# program_logic/lifting] Lifting lemmas no longer round-trip through a
+ user-chosen predicate to define the configurations we can reduce to; they
+ directly relate to the operational semantics. This is equivalent and
+ much simpler to read.
+ Due to a lack of maintenance and usefulness, lifting lemmas for Hoare triples
+ are removed.
## Iris 2.0-rc1