diff --git a/exe/Main.idr b/exe/Main.idr
index 1470184..e92cb90 100644
--- a/exe/Main.idr
+++ b/exe/Main.idr
@@ -56,7 +56,7 @@ banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
 export
 tm : Term Three 1 2
 tm =
-  (Pi One "a" (BVT 0) (TUsed $ E (F "F" :@@ [BVT 0, FT "w"]))
+  (Pi_ One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
     `DCloT` (K One ::: id))
     `CloT`  (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)