diff --git a/theories/Examples.v b/theories/Examples.v
index 963a677..fb6b0da 100644
--- a/theories/Examples.v
+++ b/theories/Examples.v
@@ -1,7 +1,7 @@
 (*** Examples from the paper
 
-  We show how we can discriminate booleans and thus natural numbers.
-  This in turn let us write head and tail functions.
+  We show how we can discriminate booleans and thus natural numbers and thus
+  erased natural numbers.
 
 ***)