diff --git a/CHANGELOG.md b/CHANGELOG.md
index f6636b984f825e5b7ddeb959afb5cfff5b094708..8f493379ca79df38974e716322219717a2b00cff 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -23,6 +23,7 @@ API-breaking change is listed.
 - Add `inv` tactic as a more well-behaved alternative to `inversion_clear`
   (inspired by CompCert), and `oinv` as its version on open terms.
 - Add `prod_swap : A * B → B * A` and some basic theory about it.
+- Add lemma `lookup_total_fmap`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).