diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index efe9cf9..9b4a2be 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -94,8 +94,11 @@ tests = "whnf" :- [
 
   "term closure" :- [
     testWhnfT "(λy. x){a/x}"
-      (CloT (Lam "x" $ TUnused $ BVT 0) (F "a" ::: id))
-      (Lam "x" $ TUnused $ FT "a")
+      (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id))
+      (Lam "y" $ TUnused $ FT "a"),
+    testWhnfT "(λy. y){a/x}"
+      (CloT (Lam "y" $ TUsed $ BVT 0) (F "a" ::: id))
+      (Lam "y" $ TUsed $ BVT 0)
   ],
 
   "looking inside […]" :- [
@@ -111,6 +114,10 @@ tests = "whnf" :- [
         (Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0,
     testNoStepE "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
       F "a" :@
-      E ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
+      E ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
+    testNoStepT "λx. [y [x]]{x/x,a/y}" {n = 1} $
+      Lam "x" $ TUsed $ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
+    testNoStepE "f ([y [x]]{x/x,a/y})" {n = 1} $
+      F "f" :@ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id)
   ]
 ]