diff --git a/src/core-logic/level.ml b/src/core-logic/level.ml
index d9c59b7c..12a28f58 100644
--- a/src/core-logic/level.ml
+++ b/src/core-logic/level.ml
@@ -183,7 +183,7 @@ let as_int self : _ option =
 
 let is_int self : bool = Option.is_some (as_int self)
 
-let leq_judge st l1 l2 : bool =
+let judge_leq st l1 l2 : bool =
   assert (store_id l1 = st.id);
   assert (store_id l2 = st.id);
 
@@ -232,5 +232,8 @@ let leq_judge st l1 l2 : bool =
   let l2, n = as_offset l2 in
   prove l1 l2 n
 
-let eq_judge st l1 l2 : bool =
-  equal l1 l2 || (leq_judge st l1 l2 && leq_judge st l2 l1)
+let judge_eq st l1 l2 : bool =
+  equal l1 l2 || (judge_leq st l1 l2 && judge_leq st l2 l1)
+
+let judge_is_zero st l : bool = judge_leq st l (zero st)
+let judge_is_nonzero st l : bool = judge_leq st (one st) l
diff --git a/src/core-logic/level.mli b/src/core-logic/level.mli
index 3ecfc6fc..41416052 100644
--- a/src/core-logic/level.mli
+++ b/src/core-logic/level.mli
@@ -40,12 +40,21 @@ val is_one : t -> bool
 val is_int : t -> bool
 val as_int : t -> int option
 
-(** {2 Equivalence} *)
+(** {2 Judgements}
 
-val leq_judge : store -> t -> t -> bool
-(** [leq_judge st l1 l2] is [true] if [l1] is proven to be lower
+    These are little proofs of some symbolic properties of levels, even
+    those which contain variables. *)
+
+val judge_leq : store -> t -> t -> bool
+(** [judge_leq st l1 l2] is [true] if [l1] is proven to be lower
     or equal to [l2] *)
 
-val eq_judge : store -> t -> t -> bool
-(** [eq_judge st l1 l2] is [true] iff [leq_judge l1 l2]
-    and [leq_judge l2 l1] *)
+val judge_eq : store -> t -> t -> bool
+(** [judge_eq st l1 l2] is [true] iff [judge_leq l1 l2]
+    and [judge_leq l2 l1] *)
+
+val judge_is_zero : store -> t -> bool
+(** [judge_is_zero st l] is [true] iff [l <= 0] holds *)
+
+val judge_is_nonzero : store -> t -> bool
+(** [judge_is_nonzero st l] is [true] iff [1 <= l] holds *)