diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 557e115..a434cdc 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -88,43 +88,3 @@ public export %inline
 lookupElim : forall isGlobal.
              Name -> Definitions' q isGlobal -> Maybe (Elim q d n)
 lookupElim x defs = toElim !(lookup x defs)
-
-
-parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
-  namespace Term
-    public export %inline
-    isRedex : Term q d n -> Bool
-    isRedex = isRedex $ \x => lookupElim x defs
-
-    public export
-    0 IsRedex, NotRedex : Pred $ Term q d n
-    IsRedex  = So . isRedex
-    NotRedex = No . isRedex
-
-  namespace Elim
-    public export %inline
-    isRedex : Elim q d n -> Bool
-    isRedex = isRedex $ \x => lookupElim x defs
-
-    public export
-    0 IsRedex, NotRedex : Pred $ Elim q d n
-    IsRedex  = So . isRedex
-    NotRedex = No . isRedex
-
-public export
-0 NonRedexElim, NonRedexTerm :
-  (q : Type) -> (d, n : Nat) -> {isGlobal : Pred q} ->
-  Definitions' q isGlobal -> Type
-NonRedexElim q d n defs = Subset (Elim q d n) (NotRedex defs)
-NonRedexTerm q d n defs = Subset (Term q d n) (NotRedex defs)
-
-parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
-  namespace Term
-    export covering %inline
-    whnfD : Term q d n -> NonRedexTerm q d n defs
-    whnfD = whnf $ \x => lookupElim x defs
-
-  namespace Elim
-    export covering %inline
-    whnfD : Elim q d n -> NonRedexElim q d n defs
-    whnfD = whnf $ \x => lookupElim x defs
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index f741131..444b920 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -1,7 +1,5 @@
 module Quox.Equal
 
-import public Quox.Syntax
-import public Quox.Definition
 import public Quox.Typing
 import public Control.Monad.Either
 import public Control.Monad.Reader
@@ -83,7 +81,7 @@ parameters (defs : Definitions' q g)
   public export
   isSubSing : Term q 0 n -> Bool
   isSubSing ty =
-    let Element ty nc = whnfD defs ty in
+    let Element ty nc = whnf defs ty in
     case ty of
       TYPE _             => False
       Pi   {res, _}      => isSubSing res.term
@@ -118,9 +116,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m ()
       compare0 ctx ty s t =
         wrapErr (WhileComparingT (MkTyContext new ctx) !mode ty s t) $ do
-          let Element ty nty = whnfD defs ty
-              Element s  ns  = whnfD defs s
-              Element t  nt  = whnfD defs t
+          let Element ty nty = whnf defs ty
+              Element s  ns  = whnf defs s
+              Element t  nt  = whnf defs t
           tty <- ensureTyCon ty
           compare0' ctx ty s t
 
@@ -192,8 +190,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
     export covering %inline
     compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
     compareType ctx s t = do
-      let Element s ns = whnfD defs s
-          Element t nt = whnfD defs t
+      let Element s ns = whnf defs s
+          Element t nt = whnf defs t
       ts <- ensureTyCon s
       tt <- ensureTyCon t
       st <- either pure (const $ clashT (TYPE UAny) s t) $
@@ -245,7 +243,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
 
     compareType' ctx (E e) (E f) = do
       -- no fanciness needed here cos anything other than a neutral
-      -- has been inlined by whnfD
+      -- has been inlined by whnf
       Elim.compare0 ctx e f
 
     ||| performs the minimum work required to recompute the type of an elim.
@@ -291,8 +289,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
       compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m ()
       compare0 ctx e f =
         wrapErr (WhileComparingE (MkTyContext new ctx) !mode e f) $ do
-          let Element e ne = whnfD defs e
-              Element f nf = whnfD defs f
+          let Element e ne = whnf defs e
+              Element f nf = whnf defs f
           -- [fixme] there is a better way to do this "isSubSing" stuff for sure
           unless (isSubSing defs !(computeElimType ctx e ne)) $
             compare0' ctx e f ne nf
diff --git a/lib/Quox/Syntax/Term/Reduce.idr b/lib/Quox/Reduce.idr
similarity index 92%
rename from lib/Quox/Syntax/Term/Reduce.idr
rename to lib/Quox/Reduce.idr
index b101dc8..f985624 100644
--- a/lib/Quox/Syntax/Term/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -1,8 +1,8 @@
-module Quox.Syntax.Term.Reduce
+module Quox.Reduce
 
 import Quox.No
-import Quox.Syntax.Term.Base
-import Quox.Syntax.Term.Subst
+import Quox.Syntax
+import Quox.Definition
 import Data.Vect
 import Data.Maybe
 
@@ -125,10 +125,6 @@ parameters (th : DSubst dfrom dto) (ph : TSubst q dto from to)
     pushSubstsWith' e = (pushSubstsWith th ph e).fst
 
 
-public export 0
-Lookup : TermLike
-Lookup q d n = Name -> Maybe $ Elim q d n
-
 public export %inline
 isLamHead : Elim {} -> Bool
 isLamHead (Lam {} :# Pi {}) = True
@@ -154,12 +150,12 @@ isAnn : Elim {} -> Bool
 isAnn (_ :# _) = True
 isAnn _        = False
 
-parameters (g : Lookup q d n)
+parameters (defs : Definitions' q g)
   mutual
     namespace Elim
       public export
       isRedex : Elim q d n -> Bool
-      isRedex (F x)                = isJust $ g x
+      isRedex (F x) {d, n}         = isJust $ lookupElim x defs {d, n}
       isRedex (B _)                = False
       isRedex (f :@ _)             = isRedex f || isLamHead f
       isRedex (CasePair {pair, _}) = isRedex pair || isPairHead pair
@@ -188,18 +184,19 @@ parameters (g : Lookup q d n)
     IsRedex  = So . isRedex
     NotRedex = No . isRedex
 
-public export
-0 NonRedexElim, NonRedexTerm : (q, d, n : _) -> Lookup q d n -> Type
-NonRedexElim q d n g = Subset (Elim q d n) (NotRedex g)
-NonRedexTerm q d n g = Subset (Term q d n) (NotRedex g)
+parameters (q : Type) (d, n : Nat) {g : q -> Type} (defs : Definitions' q g)
+  public export
+  0 NonRedexElim, NonRedexTerm : Type
+  NonRedexElim = Subset (Elim q d n) (NotRedex defs)
+  NonRedexTerm = Subset (Term q d n) (NotRedex defs)
 
 
-parameters (g : Lookup q d n)
+parameters (defs : Definitions' q g)
   mutual
     namespace Elim
       export covering
-      whnf : Elim q d n -> NonRedexElim q d n g
-      whnf (F x) with (g x) proof eq
+      whnf : Elim q d n -> NonRedexElim q d n defs
+      whnf (F x) with (lookupElim x defs) proof eq
         _ | Just y  = whnf y
         _ | Nothing = Element (F x) $ rewrite eq in Ah
 
@@ -251,7 +248,7 @@ parameters (g : Lookup q d n)
 
     namespace Term
       export covering
-      whnf : Term q d n -> NonRedexTerm q d n g
+      whnf : Term q d n -> NonRedexTerm q d n defs
       whnf t@(TYPE {}) = Element t Ah
       whnf t@(Pi   {}) = Element t Ah
       whnf t@(Lam  {}) = Element t Ah
diff --git a/lib/Quox/Syntax/Term.idr b/lib/Quox/Syntax/Term.idr
index f9acfe6..76894ec 100644
--- a/lib/Quox/Syntax/Term.idr
+++ b/lib/Quox/Syntax/Term.idr
@@ -3,5 +3,4 @@ module Quox.Syntax.Term
 import public Quox.Syntax.Term.Base
 import public Quox.Syntax.Term.Split
 import public Quox.Syntax.Term.Subst
-import public Quox.Syntax.Term.Reduce
 import public Quox.Syntax.Term.Pretty
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index f473788..7de1e4c 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -1,14 +1,11 @@
 module Quox.Typing
 
 import public Quox.Syntax
-import public Quox.Context
 import public Quox.Definition
+import public Quox.Reduce
 
-import Data.Nat
 import public Data.SortedMap
-import Control.Monad.Either
-import Control.Monad.Reader
-import Control.Monad.State
+import public Control.Monad.Either
 import Generics.Derive
 
 %hide TT.Name
@@ -206,27 +203,27 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
   export covering %inline
   expectTYPE : Term q d n -> m Universe
   expectTYPE s =
-    case fst $ whnfD defs s of
+    case fst $ whnf defs s of
       TYPE l => pure l
       _      => throwError $ ExpectedTYPE s
 
   export covering %inline
   expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n)
   expectPi s =
-    case fst $ whnfD defs s of
+    case fst $ whnf defs s of
       Pi {qty, arg, res, _} => pure (qty, arg, res)
       _                     => throwError $ ExpectedPi s
 
   export covering %inline
   expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n)
   expectSig s =
-    case fst $ whnfD defs s of
+    case fst $ whnf defs s of
       Sig {fst, snd, _} => pure (fst, snd)
       _                 => throwError $ ExpectedSig s
 
   export covering %inline
   expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n)
   expectEq s =
-    case fst $ whnfD defs s of
+    case fst $ whnf defs s of
       Eq {ty, l, r, _} => pure (ty, l, r)
       _                => throwError $ ExpectedEq s
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 2407bf9..064cee6 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -22,12 +22,12 @@ modules =
   Quox.Syntax.Term,
   Quox.Syntax.Term.Base,
   Quox.Syntax.Term.Pretty,
-  Quox.Syntax.Term.Reduce,
   Quox.Syntax.Term.Split,
   Quox.Syntax.Term.Subst,
   Quox.Syntax.Universe,
   Quox.Syntax.Var,
   Quox.Definition,
+  Quox.Reduce,
   Quox.Context,
   Quox.Equal,
   Quox.Name,
diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr
index bb5b3a8..59e8348 100644
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@@ -8,35 +8,30 @@ import TAP
 
 
 testWhnf : Eq b => Show b => (a -> (Subset b _)) -> String -> a -> b -> Test
-testWhnf whnf label from to = test "\{label}  (whnf)" $
-  let result = fst (whnf from) in
-  if result == to
-     then Right ()
-     else with Prelude.(::)
-          Left [("expected", to), ("received", result)]
+testWhnf whnf label from to = test "\{label}  (whnf)" $ do
+  let result = fst (whnf from)
+  unless (result == to) $
+    Left [("exp", to), ("got", result)] {a = List (String, b)}
 
 testNoStep : Eq a => Show a => (a -> (Subset a _)) -> String -> a -> Test
-testNoStep whnf label e = test "\{label}  (no step)" $
-  let result = fst (whnf e) in
-  if result == e
-     then Right ()
-     else with Prelude.(::)
-          Left [("reduced", result)]
+testNoStep whnf label e = test "\{label}  (no step)" $ do
+  let result = fst (whnf e)
+  unless (result == e) $ Left [("reduced", result)] {a = List (String, a)}
 
 
 
 parameters {default empty defs : Definitions Three} {default 0 d, n : Nat}
   testWhnfT : String -> Term Three d n -> Term Three d n -> Test
-  testWhnfT = testWhnf (whnfD defs)
+  testWhnfT = testWhnf (whnf defs)
 
   testWhnfE : String -> Elim Three d n -> Elim Three d n -> Test
-  testWhnfE = testWhnf (whnfD defs)
+  testWhnfE = testWhnf (whnf defs)
 
   testNoStepE : String -> Elim Three d n -> Test
-  testNoStepE = testNoStep (whnfD defs)
+  testNoStepE = testNoStep (whnf defs)
 
   testNoStepT : String -> Term Three d n -> Test
-  testNoStepT = testNoStep (whnfD defs)
+  testNoStepT = testNoStep (whnf defs)
 
 
 tests = "whnf" :- [
diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr
index be9ebb8..c09139c 100644
--- a/tests/TypingImpls.idr
+++ b/tests/TypingImpls.idr
@@ -50,8 +50,8 @@ PrettyHL q => ToInfo (Error q) where
      ("left",  prettyStr True p),
      ("right", prettyStr True q)]
   toInfo (NotType ty) =
-    [("type",   "NotType"),
-     ("actual", prettyStr True ty)]
+    [("type", "NotType"),
+     ("got",  prettyStr True ty)]
   toInfo (WrongType ty s t) =
     [("type",  "WrongType"),
      ("ty",    prettyStr True ty),