diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr
index 2c0a67a..75a1248 100644
--- a/lib/Quox/Whnf/Main.idr
+++ b/lib/Quox/Whnf/Main.idr
@@ -255,7 +255,7 @@ CanWhnf Term Interface.isRedexT where
       Left _ => case p of
         Nat p _               => pure $ nred $ Nat (S p) loc
         E (Ann (Nat p _) _ _) => pure $ nred $ Nat (S p) loc
-      Right nc => pure $ Element (Succ p loc) nc
+      Right nc => pure $ nred $ Succ p loc
 
   whnf defs ctx sg (Let _ rhs body _) =
     whnf defs ctx sg $ sub1 body rhs