diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 38dc637..00a5836 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -261,27 +261,27 @@ comp' th ps ph = map (/// th) ps . ph
 
 ||| true if an elimination has a closure or dimension closure at the top level
 public export %inline
-isCloE : Elim d n -> Bool
-isCloE (CloE  _ _) = True
-isCloE (DCloE _ _) = True
-isCloE _           = False
+topCloE : Elim d n -> Bool
+topCloE (CloE  _ _) = True
+topCloE (DCloE _ _) = True
+topCloE _           = False
 
 ||| true if a term has a closure or dimension closure at the top level,
 ||| or is `E` applied to such an elimination
 public export %inline
-isCloT : Term d n -> Bool
-isCloT (CloT  _ _) = True
-isCloT (DCloT _ _) = True
-isCloT (E e)       = isCloE e
-isCloT _           = False
+topCloT : Term d n -> Bool
+topCloT (CloT  _ _) = True
+topCloT (DCloT _ _) = True
+topCloT (E e)       = topCloE e
+topCloT _           = False
 
 ||| an elimination which is not a top level closure
 public export NotCloElim : Nat -> Nat -> Type
-NotCloElim d n = Subset (Elim d n) $ So . not . isCloE
+NotCloElim d n = Subset (Elim d n) $ So . not . topCloE
 
 ||| a term which is not a top level closure
 public export NotCloTerm : Nat -> Nat -> Type
-NotCloTerm d n = Subset (Term d n) $ So . not . isCloT
+NotCloTerm d n = Subset (Term d n) $ So . not . topCloT
 
 
 mutual