diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4029e711901fd5d6573e6a71a7d9fec21e2787fe..5ab682fcd0fc1dcbd6dac92ed5d2d1e1f56f9245 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -125,6 +125,11 @@ Changes in Coq:
   - Use `auth_auth` and `auth_frag` for the injections into authoritative
     elements and non-authoritative elements respectively.
   - Lemmas for the projections and injections are renamed accordingly.
+    For examples:
+    + `authoritative_validN` → `auth_auth_proj_validN`
+    + `auth_own_validN` → `auth_frag_proj_validN`
+    + `auth_auth_valid` was not renamed because it was already used for the
+      authoritative injection.
   - `auth_both_valid` → `auth_both_valid_2`
   - `auth_valid_discrete_2` → `auth_both_valid`