diff --git a/CHANGES.md b/CHANGES.md
index ce10eac5..8db8b405 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -12,8 +12,9 @@
     polymporphically, and (except reverse and zip) all take a function as an argument. SBV firstifies these
     functions, and the resulting code is compatible with Z3 and CVC5. (Firstification might change in the
     future, as SMTLib gains support for more higher-order features itself.) Proof-support in backend solvers
-    for higher-order functions is still quite weak, though KnuckleDragger makes things easier. See
-    Documentation.SBV.Examples.KnuckleDragger.Lists for several examples.
+    for higher-order functions is still quite weak, though KnuckleDragger makes things easier.
+
+  * New examples added: Documentation.SBV.Examples.KnuckleDragger.{Lists|EquationalReasoning}.
 
   * [BACKWARDS COMPATIBILITY] Removed rarely used functions mapi, foldli, foldri from Data.SBV.List. These
     can now be defined by the user as we have proper support for fold and map using lambdas.