diff --git a/examples/example1.v b/examples/example1.v
index 67d6eb6..ce94024 100644
--- a/examples/example1.v
+++ b/examples/example1.v
@@ -29,7 +29,6 @@
 
 
 Require Export checker.
-Require Export notation.
 
 
 (* v≥0∧A≥0 → [x'=v,v'=A&true] v≥0 *)