diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f928dd8..6e9d7a0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -5,7 +5,9 @@
 ### Added
 
 - in `finmap.v`:
-  + lemmas `bigfcup_imfset`, `fbig_pred1_inj`
+  + lemmas `bigfcup_imfset1`, `fbig_pred1_inj`
+  + lemmas `fset_seq1`, `imfset0`, `imfset_fset1`, `imfset_fset2`, `imfsetU`,
+    `imfsetU1`, `imfsetI`, `bigfcup_imfset`
 
 ### Changed