renaming etc in closure stuff

src/Quox/Syntax/Term.idr

@@ -259,13 +259,7 @@ comp' : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
 comp' th ps ph = map (/// th) ps . ph
 
 
-||| true if an elimination has a closure or dimension closure at the top level
+mutual
-public export %inline
-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
@@ -275,13 +269,36 @@ topCloT (DCloT _ _) = True
   topCloT (E e)       = topCloE e
   topCloT _           = False
 
-||| an elimination which is not a top level closure
+  ||| true if an elimination has a closure or dimension closure at the top level
-public export NotCloElim : Nat -> Nat -> Type
+  public export %inline
-NotCloElim d n = Subset (Elim d n) $ So . not . topCloE
+  topCloE : Elim d n -> Bool
+  topCloE (CloE  _ _) = True
+  topCloE (DCloE _ _) = True
+  topCloE _           = False
+
+
+public export IsNotCloT : Term d n -> Type
+IsNotCloT = So . not . topCloT
 
 ||| a term which is not a top level closure
 public export NotCloTerm : Nat -> Nat -> Type
-NotCloTerm d n = Subset (Term d n) $ So . not . topCloT
+NotCloTerm d n = Subset (Term d n) IsNotCloT
+
+public export IsNotCloE : Elim d n -> Type
+IsNotCloE = So . not . topCloE
+
+||| an elimination which is not a top level closure
+public export NotCloElim : Nat -> Nat -> Type
+NotCloElim d n = Subset (Elim d n) IsNotCloE
+
+public export %inline
+ncloT : (t : Term d n) -> (0 _ : IsNotCloT t) => NotCloTerm d n
+ncloT t = Element t %search
+
+public export %inline
+ncloE : (t : Elim d n) -> (0 _ : IsNotCloE t) => NotCloElim d n
+ncloE e = Element e %search
+
 
 
 mutual
@@ -301,13 +318,13 @@ mutual
   pushSubstsT' : DSubst dfrom dto -> TSubst dto from to ->
                  Term dfrom from -> NotCloTerm dto to
   pushSubstsT' th ph (TYPE l) =
-    Element (TYPE l) Oh
+    ncloT $ TYPE l
   pushSubstsT' th ph (Pi qty qtm x a b) =
-    Element (Pi qty qtm x (subs a th ph) (subs b th (push ph))) Oh
+    ncloT $ Pi qty qtm x (subs a th ph) (subs b th (push ph))
   pushSubstsT' th ph (Lam x t) =
-    Element (Lam x $ subs t th $ push ph) Oh
+    ncloT $ Lam x $ subs t th $ push ph
   pushSubstsT' th ph (E e) =
-    let Element e prf = pushSubstsE' th ph e in Element (E e) prf
+    let Element e _ = pushSubstsE' th ph e in ncloT $ E e
   pushSubstsT' th ph (CloT  s ps) =
     pushSubstsT' th (comp' th ps ph) s
   pushSubstsT' th ph (DCloT s ps) =
@@ -317,13 +334,13 @@ mutual
   pushSubstsE' : DSubst dfrom dto -> TSubst dto from to ->
                  Elim dfrom from -> NotCloElim dto to
   pushSubstsE' th ph (F x) =
-    Element (F x) Oh
+    ncloE $ F x
   pushSubstsE' th ph (B i) =
     assert_total pushSubstsE $ ph !! i
   pushSubstsE' th ph (f :@ s) =
-    Element (subs f th ph :@ subs s th ph) Oh
+    ncloE $ subs f th ph :@ subs s th ph
   pushSubstsE' th ph (s :# a) =
-    Element (subs s th ph :# subs a th ph) Oh
+    ncloE $ subs s th ph :# subs a th ph
   pushSubstsE' th ph (CloE  e ps) =
     pushSubstsE' th (comp' th ps ph) e
   pushSubstsE' th ph (DCloE e ps) =