diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 3782de3..3c35354 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -74,6 +74,8 @@ isEmpty : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
           Eff EqualInner Bool
 isEmpty defs ctx sg ty0 = do
   Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
+  let Left  y = choose $ isTyConE ty0
+    | Right n => pure False
   case ty0 of
     TYPE {} => pure False
     Pi {arg, res, _} => pure False
@@ -85,15 +87,7 @@ isEmpty defs ctx sg ty0 = do
     Eq {} => pure False
     Nat {} => pure False
     BOX {ty, _} => isEmpty defs ctx sg ty
-    E (Ann {tm, _}) => isEmpty defs ctx sg tm
     E _ => pure False
-    Lam  {} => pure False
-    Pair {} => pure False
-    Tag  {} => pure False
-    DLam {} => pure False
-    Zero {} => pure False
-    Succ {} => pure False
-    Box  {} => pure False
 
 ||| true if a type is known to be a subsingleton purely by its form.
 ||| a subsingleton is a type with only zero or one possible values.
@@ -110,6 +104,8 @@ isSubSing : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
             Eff EqualInner Bool
 isSubSing defs ctx sg ty0 = do
   Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
+  let Left  y = choose $ isTyConE ty0
+    | Right n => pure False
   case ty0 of
     TYPE {} => pure False
     Pi {arg, res, _} =>
@@ -123,15 +119,7 @@ isSubSing defs ctx sg ty0 = do
     Eq {} => pure True
     Nat {} => pure False
     BOX {ty, _} => isSubSing defs ctx sg ty
-    E (Ann {tm, _}) => isSubSing defs ctx sg tm
     E _ => pure False
-    Lam  {} => pure False
-    Pair {} => pure False
-    Tag  {} => pure False
-    DLam {} => pure False
-    Zero {} => pure False
-    Succ {} => pure False
-    Box  {} => pure False
 
 
 ||| the left argument if the current mode is `Super`; otherwise the right one.