diff --git a/README.md b/README.md
index 24900e6acdae00aa90c77dcd687130f497110cc4..6367378670289ddb4e3256aa3068a04b964b8ddc 100644
--- a/README.md
+++ b/README.md
@@ -38,6 +38,7 @@ they can illustrate the usage of the logic.
   + `lock.v` - symbolic execution rules for a simple spin lock
   + `counter.v` - symbolic execution rules and refinements for two different counters
   + `list.v` - rules for the recursive type of lists
+  + `polyeq.v` - polymoprhic equality predicate
 - `examples`
   + `bit.v` - "representation independence example" for a simple bit interface
   + `or.v` - expressing non-determinism with concurrency