diff --git a/src/Quox/Reduce.idr b/src/Quox/Reduce.idr
index 19fbd2b..50f4038 100644
--- a/src/Quox/Reduce.idr
+++ b/src/Quox/Reduce.idr
@@ -5,9 +5,9 @@ import public Quox.Syntax
 
 public export
 data IsRedexT : Term d n -> Type where
-  IsUpsilon : IsRedexT $ E (_ :# _)
-  IsCloT    : IsRedexT $ CloT {}
-  IsDCloT   : IsRedexT $ DCloT {}
+  IsUpsilonT : IsRedexT $ E (_ :# _)
+  IsCloT     : IsRedexT $ CloT {}
+  IsDCloT    : IsRedexT $ DCloT {}
 
 public export %inline
 NotRedexT : Term d n -> Type
@@ -15,9 +15,10 @@ NotRedexT = Not . IsRedexT
 
 public export
 data IsRedexE : Elim d n -> Type where
-  IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _
-  IsCloE    : IsRedexE $ CloE {}
-  IsDCloE   : IsRedexE $ DCloE {}
+  IsUpsilonE : IsRedexE $ E _ :# _
+  IsBetaLam  : IsRedexE $ (Lam {} :# Pi {}) :@ _
+  IsCloE     : IsRedexE $ CloE {}
+  IsDCloE    : IsRedexE $ DCloE {}
 
 public export %inline
 NotRedexE : Elim d n -> Type
@@ -26,7 +27,7 @@ NotRedexE = Not . IsRedexE
 
 export %inline
 isRedexT : (t : Term d n) -> Dec (IsRedexT t)
-isRedexT (E (_ :# _))   = Yes IsUpsilon
+isRedexT (E (_ :# _))   = Yes IsUpsilonT
 isRedexT (CloT {})      = Yes IsCloT
 isRedexT (DCloT {})     = Yes IsDCloT
 isRedexT (TYPE _)       = No $ \x => case x of {}
@@ -40,6 +41,7 @@ isRedexT (E (DCloE {})) = No $ \x => case x of {}
 
 export %inline
 isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
+isRedexE (E _ :# _)                    = Yes IsUpsilonE
 isRedexE ((Lam {} :# Pi {}) :@ _)      = Yes IsBetaLam
 isRedexE (CloE {})                     = Yes IsCloE
 isRedexE (DCloE {})                    = Yes IsDCloE
@@ -60,7 +62,11 @@ isRedexE ((CloT {}  :# _)        :@ _) = No $ \x => case x of {}
 isRedexE ((DCloT {} :# _)        :@ _) = No $ \x => case x of {}
 isRedexE (CloE {}                :@ _) = No $ \x => case x of {}
 isRedexE (DCloE {}               :@ _) = No $ \x => case x of {}
-isRedexE (_ :# _)                      = No $ \x => case x of {}
+isRedexE (TYPE _   :# _)               = No $ \x => case x of {}
+isRedexE (Pi {}    :# _)               = No $ \x => case x of {}
+isRedexE (Lam {}   :# _)               = No $ \x => case x of {}
+isRedexE (CloT {}  :# _)               = No $ \x => case x of {}
+isRedexE (DCloT {} :# _)               = No $ \x => case x of {}
 
 
 public export %inline
@@ -89,9 +95,9 @@ substScope arg argTy (TUnused body) = body
 
 export %inline
 stepT' : (s : Term d n) -> IsRedexT s -> Term d n
-stepT' (E (s :# _)) IsUpsilon = s
-stepT' (CloT  s th) IsCloT    = pushSubstsTWith' id th s
-stepT' (DCloT s th) IsDCloT   = pushSubstsTWith' th id s
+stepT' (E (s :# _)) IsUpsilonT = s
+stepT' (CloT  s th) IsCloT     = pushSubstsTWith' id th s
+stepT' (DCloT s th) IsDCloT    = pushSubstsTWith' th id s
 
 export %inline
 stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
@@ -99,6 +105,7 @@ stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
 
 export %inline
 stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
+stepE' (E e :# _) IsUpsilonE = e
 stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
   substScope s arg body :# substScope s arg res
 stepE' (CloE  e th) IsCloE  = pushSubstsEWith' id th e