diff --git a/nbe.rkt b/nbe.rkt
index 9c6701d..cf227be 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -21,7 +21,7 @@
                      'zero
                      'nat
                      (List 'λ Norm)
-                     (List 'U V)
+                     'U
                      (List 'succ Norm)
                      (List 'Π Norm Norm)))