diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 2fbfb5c..33298e2 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -13,22 +13,20 @@ record AnyTerm where
 public export
 record Definition where
   constructor MkDef'
-  qty         : Qty
-  0 qtyGlobal : IsGlobal qty
-  type        : AnyTerm
-  term        : Maybe AnyTerm
+  qty  : Qty
+  type : AnyTerm
+  term : Maybe AnyTerm
+  {auto 0 qtyGlobal : IsGlobal qty}
 
 public export %inline
-MkDef : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
-           (type, term : forall d, n. Term d n) -> Definition
-MkDef {qty, type, term} =
-  MkDef' {qty, qtyGlobal = %search, type = T type, term = Just (T term)}
+mkDef : (qty : Qty) -> (0 _ : IsGlobal qty) =>
+        (type, term : forall d, n. Term d n) -> Definition
+mkDef qty type term = MkDef' {qty, type = T type, term = Just (T term)}
 
 public export %inline
-MkAbstract : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
+mkAbstract : (qty : Qty) -> (0 _ : IsGlobal qty) =>
              (type : forall d, n. Term d n) -> Definition
-MkAbstract {qty, type} =
-  MkDef' {qty, qtyGlobal = %search, type = T type, term = Nothing}
+mkAbstract qty type = MkDef' {qty, type = T type, term = Nothing}
 
 
 public export %inline
diff --git a/lib/Quox/Syntax/Term/Reduce.idr b/lib/Quox/Syntax/Term/Reduce.idr
index 9ee5ab1..8be3336 100644
--- a/lib/Quox/Syntax/Term/Reduce.idr
+++ b/lib/Quox/Syntax/Term/Reduce.idr
@@ -202,11 +202,11 @@ mutual
   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
+  isRedexT (TYPE {}) = No $ \case _ impossible
+  isRedexT (Pi   {}) = No $ \case _ impossible
+  isRedexT (Lam  {}) = No $ \case _ impossible
+  isRedexT (E (F _)) = No $ \case IsERedex _ impossible
+  isRedexT (E (B _)) = No $ \case IsERedex _ impossible
 
   export %inline
   isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
@@ -214,28 +214,28 @@ mutual
   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 {}
+  isRedexE (F x)                         = No $ \case _ impossible
+  isRedexE (B i)                         = No $ \case _ impossible
+  isRedexE (F _                    :@ _) = No $ \case _ impossible
+  isRedexE (B _                    :@ _) = No $ \case _ impossible
+  isRedexE (_ :@ _                 :@ _) = No $ \case _ impossible
+  isRedexE ((TYPE _   :# _)        :@ _) = No $ \case _ impossible
+  isRedexE ((Pi {}    :# _)        :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# TYPE _)   :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# E _)      :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \case _ impossible
+  isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \case _ impossible
+  isRedexE ((E _      :# _)        :@ _) = No $ \case _ impossible
+  isRedexE ((CloT {}  :# _)        :@ _) = No $ \case _ impossible
+  isRedexE ((DCloT {} :# _)        :@ _) = No $ \case _ impossible
+  isRedexE (CloE {}                :@ _) = No $ \case _ impossible
+  isRedexE (DCloE {}               :@ _) = No $ \case _ impossible
+  isRedexE (TYPE _   :# _)               = No $ \case _ impossible
+  isRedexE (Pi {}    :# _)               = No $ \case _ impossible
+  isRedexE (Lam {}   :# _)               = No $ \case _ impossible
+  isRedexE (CloT {}  :# _)               = No $ \case _ impossible
+  isRedexE (DCloT {} :# _)               = No $ \case _ impossible
 
 
 public export %inline
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 8e9d5d1..6bde70a 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -161,11 +161,11 @@ tests = "equality & subtyping" :- [
 
     "free var" :-
     let au_bu = fromList
-          [("A", MkDef Any (TYPE (U 1)) (TYPE (U 0))),
-           ("B", MkDef Any (TYPE (U 1)) (TYPE (U 0)))]
+          [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))),
+           ("B", mkDef Any (TYPE (U 1)) (TYPE (U 0)))]
         au_ba = fromList
-          [("A", MkDef Any (TYPE (U 1)) (TYPE (U 0))),
-           ("B", MkDef Any (TYPE (U 1)) (FT "A"))]
+          [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))),
+           ("B", mkDef Any (TYPE (U 1)) (FT "A"))]
     in [
       testEq "A ≡ A" $
         equalE (F "A") (F "A"),