diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index fed340c..0248a21 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -6,6 +6,8 @@ import public Control.Monad.Either
 import public Control.Monad.Reader
 import Data.Maybe
 
+%default total
+
 
 public export
 record CmpContext where
@@ -98,7 +100,7 @@ parameters (defs : Definitions' q g)
   ||| * all equality types are subsingletons because uip is admissible by
   |||   boundary separation.
   ||| * an enum type is a subsingleton if it has zero or one tags.
-  public export
+  public export covering
   isSubSing : HasErr q m => {n : Nat} -> Term q 0 n -> m Bool
   isSubSing ty = do
     Element ty nc <- whnfT defs ty