diff --git a/CHANGELOG.md b/CHANGELOG.md
index d8478647c5481af1d530cea679f61017ddb6fad6..1b38eea0282f2e6154b9ffc170bd3932cb5b8eef 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -64,6 +64,9 @@ Coq 8.11 is no longer supported in this version of Iris.
   - Use `□`/`-∗` instead of `<pers>`/`→`.
   - Strengthen to ensure that functions for recursive calls are non-expansive.
 * Add `big_andM` (big conjunction on finite maps) with lemmas similar to `big_andL`.
+* Add transitive embedding that constructs an embedding of `PROP1` into `PROP3`
+  by combining the embeddings of `PROP1` into `PROP2` and `PROP2` into `PROP3`.
+  This construct is *not* declared as an instance to avoid TC search divergence.
 
 **Changes in `proofmode`:**