diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 3e846c8..ff08764 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -12,7 +12,7 @@ record AnyTerm q where
   get : forall d, n. Term q d n
 
 public export
-record Definition' q (isGlobal : q -> Type) where
+record Definition' q (isGlobal : Pred q) where
   constructor MkDef'
   qty  : q
   type : AnyTerm q
@@ -46,12 +46,18 @@ public export %inline
 (.qtyP) : forall q, isGlobal. Definition' q isGlobal -> Subset q isGlobal
 g.qtyP = Element g.qty g.qtyGlobal
 
-public export %inline
-isZero : IsQty q => Definition q -> Bool
-isZero g = isYes $ isZero g.qty
 
 public export
-0 Definitions' : (q : Type) -> (q -> Type) -> Type
+0 IsZero : IsQty q => Pred $ Definition q
+IsZero g = IsZero g.qty
+
+public export %inline
+isZero : (p : IsQty q) => Dec1 $ Definition.IsZero @{p}
+isZero g = isZero g.qty
+
+
+public export
+0 Definitions' : (q : Type) -> Pred q -> Type
 Definitions' q isGlobal = SortedMap Name $ Definition' q isGlobal
 
 public export