diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index c65a1e7..52212ca 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -1,7 +1,6 @@
 module Quox.Equal
 
 import public Quox.Syntax
-import public Quox.Reduce
 import Control.Monad.Either
 import Generics.Derive
 
diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
deleted file mode 100644
index 8e25794..0000000
--- a/lib/Quox/Reduce.idr
+++ /dev/null
@@ -1,130 +0,0 @@
-module Quox.Reduce
-
-import public Quox.Syntax
-
-%default total
-
-
-public export
-data IsRedexT : Term d n -> Type where
-  IsUpsilonT : IsRedexT $ E (_ :# _)
-  IsCloT     : IsRedexT $ CloT {}
-  IsDCloT    : IsRedexT $ DCloT {}
-
-public export %inline
-NotRedexT : Term d n -> Type
-NotRedexT = Not . IsRedexT
-
-public export
-data IsRedexE : Elim d n -> Type where
-  IsUpsilonE : IsRedexE $ E _ :# _
-  IsBetaLam  : IsRedexE $ (Lam {} :# Pi {}) :@ _
-  IsCloE     : IsRedexE $ CloE {}
-  IsDCloE    : IsRedexE $ DCloE {}
-
-public export %inline
-NotRedexE : Elim d n -> Type
-NotRedexE = Not . IsRedexE
-
-
-export %inline
-isRedexT : (t : Term d n) -> Dec (IsRedexT t)
-isRedexT (E (_ :# _))   = Yes IsUpsilonT
-isRedexT (CloT {})      = Yes IsCloT
-isRedexT (DCloT {})     = Yes IsDCloT
-isRedexT (TYPE _)       = No $ \x => case x of {}
-isRedexT (Pi {})        = No $ \x => case x of {}
-isRedexT (Lam {})       = No $ \x => case x of {}
-isRedexT (E (F _))      = No $ \x => case x of {}
-isRedexT (E (B _))      = No $ \x => case x of {}
-isRedexT (E (_ :@ _))   = No $ \x => case x of {}
-isRedexT (E (CloE {}))  = No $ \x => case x of {}
-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
-isRedexE (F x)                         = No $ \x => case x of {}
-isRedexE (B i)                         = No $ \x => case x of {}
-isRedexE (F _                    :@ _) = No $ \x => case x of {}
-isRedexE (B _                    :@ _) = 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 {}   :# TYPE _)   :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# E _)      :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \x => case x of {}
-isRedexE ((E _      :# _)        :@ _) = No $ \x => case x of {}
-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 (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
-RedexTerm : Nat -> Nat -> Type
-RedexTerm d n = Subset (Term d n) IsRedexT
-
-public export %inline
-NonRedexTerm : Nat -> Nat -> Type
-NonRedexTerm d n = Subset (Term d n) NotRedexT
-
-
-public export %inline
-RedexElim : Nat -> Nat -> Type
-RedexElim d n = Subset (Elim d n) IsRedexE
-
-public export %inline
-NonRedexElim : Nat -> Nat -> Type
-NonRedexElim d n = Subset (Elim d n) NotRedexE
-
-
-||| substitute a term with annotation for the bound variable of a `ScopeTerm`
-export %inline
-substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
-substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
-substScope arg argTy (TUnused body) = body
-
-export %inline
-stepT' : (s : Term d n) -> IsRedexT s -> Term d n
-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)
-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
-stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
-
-export %inline
-stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
-stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
-
-export covering
-whnfT : Term d n -> NonRedexTerm d n
-whnfT s = case stepT s of
-               Right s'   => whnfT s'
-               Left  done => Element s done
-
-export covering
-whnfE : Elim d n -> NonRedexElim d n
-whnfE e = case stepE e of
-               Right e'   => whnfE e'
-               Left  done => Element e done
diff --git a/lib/Quox/Syntax/Term/Reduce.idr b/lib/Quox/Syntax/Term/Reduce.idr
index f0266ef..c9456b5 100644
--- a/lib/Quox/Syntax/Term/Reduce.idr
+++ b/lib/Quox/Syntax/Term/Reduce.idr
@@ -162,3 +162,135 @@ weakT t = t //. shift 1
 public export %inline
 weakE : Elim d n -> Elim d (S n)
 weakE t = t //. shift 1
+
+
+mutual
+  public export
+  data IsRedexT : Term d n -> Type where
+    IsUpsilonT : IsRedexT $ E (_ :# _)
+    IsCloT     : IsRedexT $ CloT {}
+    IsDCloT    : IsRedexT $ DCloT {}
+    IsERedex   : IsRedexE e -> IsRedexT $ E e
+
+  public export %inline
+  NotRedexT : Term d n -> Type
+  NotRedexT = Not . IsRedexT
+
+  public export
+  data IsRedexE : Elim d n -> Type where
+    IsUpsilonE : IsRedexE $ E _ :# _
+    IsBetaLam  : IsRedexE $ (Lam {} :# Pi {}) :@ _
+    IsCloE     : IsRedexE $ CloE {}
+    IsDCloE    : IsRedexE $ DCloE {}
+
+  public export %inline
+  NotRedexE : Elim d n -> Type
+  NotRedexE = Not . IsRedexE
+
+
+mutual
+  export %inline
+  isRedexT : (t : Term d n) -> Dec (IsRedexT t)
+  isRedexT (E (tm :# ty)) = Yes IsUpsilonT
+  isRedexT (CloT {})      = Yes IsCloT
+  isRedexT (DCloT {})     = Yes IsDCloT
+  isRedexT (E (CloE  {})) = Yes $ IsERedex IsCloE
+  isRedexT (E (DCloE {})) = Yes $ IsERedex IsDCloE
+  isRedexT (E e@(_ :@ _)) with (isRedexE e)
+    _ | Yes yes = Yes $ IsERedex yes
+    _ | No  no  = No \case IsERedex p => no p
+  isRedexT (TYPE {}) = No $ \x => case x of {}
+  isRedexT (Pi   {}) = No $ \x => case x of {}
+  isRedexT (Lam  {}) = No $ \x => case x of {}
+  isRedexT (E (F _)) = No $ \x => case x of IsERedex _ impossible
+  isRedexT (E (B _)) = No $ \x => case x of IsERedex _ impossible
+
+  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
+  isRedexE (F x)                         = No $ \x => case x of {}
+  isRedexE (B i)                         = No $ \x => case x of {}
+  isRedexE (F _                    :@ _) = No $ \x => case x of {}
+  isRedexE (B _                    :@ _) = 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 {}   :# TYPE _)   :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# E _)      :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \x => case x of {}
+  isRedexE ((E _      :# _)        :@ _) = No $ \x => case x of {}
+  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 (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
+RedexTerm : Nat -> Nat -> Type
+RedexTerm d n = Subset (Term d n) IsRedexT
+
+public export %inline
+NonRedexTerm : Nat -> Nat -> Type
+NonRedexTerm d n = Subset (Term d n) NotRedexT
+
+
+public export %inline
+RedexElim : Nat -> Nat -> Type
+RedexElim d n = Subset (Elim d n) IsRedexE
+
+public export %inline
+NonRedexElim : Nat -> Nat -> Type
+NonRedexElim d n = Subset (Elim d n) NotRedexE
+
+
+||| substitute a term with annotation for the bound variable of a `ScopeTerm`
+export %inline
+substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
+substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
+substScope arg argTy (TUnused body) = body
+
+mutual
+  export %inline
+  stepT' : (s : Term d n) -> IsRedexT s -> Term d n
+  stepT' (E (s :# _)) IsUpsilonT   = s
+  stepT' (CloT  s th) IsCloT       = pushSubstsTWith' id th s
+  stepT' (DCloT s th) IsDCloT      = pushSubstsTWith' th id s
+  stepT' (E e)        (IsERedex p) = E $ stepE' e p
+
+  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
+  stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
+
+export %inline
+stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
+stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
+
+export %inline
+stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
+stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
+
+export covering
+whnfT : Term d n -> NonRedexTerm d n
+whnfT s = case stepT s of
+               Right s'   => whnfT s'
+               Left  done => Element s done
+
+export covering
+whnfE : Elim d n -> NonRedexElim d n
+whnfE e = case stepE e of
+               Right e'   => whnfE e'
+               Left  done => Element e done
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index e31db43..d98ce18 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -32,6 +32,5 @@ modules =
   Quox.Context,
   Quox.Equal,
   Quox.Name,
-  Quox.Reduce,
   Quox.Typing,
   Quox.Typechecker