diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 9a69ffb..3ec9c0a 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -305,10 +305,10 @@ namespace Term
       (E _,      Nat 0 {}) => clashT s.loc ctx nat s t
       (E _,      Succ  {}) => clashT s.loc ctx nat s t
 
-      (Nat 0 {}, t) => wrongType t.loc ctx nat t
-      (Succ  {}, t) => wrongType t.loc ctx nat t
-      (E _,      t) => wrongType t.loc ctx nat t
-      (s,        _) => wrongType s.loc ctx nat s
+      (Nat  {}, t) => wrongType t.loc ctx nat t
+      (Succ {}, t) => wrongType t.loc ctx nat t
+      (E _,     t) => wrongType t.loc ctx nat t
+      (s,       _) => wrongType s.loc ctx nat s
 
   compare0' defs ctx sg str@(STRING {}) s t = local_ Equal $
     case (s, t) of