diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 5cd3cdb..2fbfb5c 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -8,7 +8,7 @@ import public Control.Monad.State
 public export
 record AnyTerm where
   constructor T
-  def : forall d, n. Term d n
+  get : forall d, n. Term d n
 
 public export
 record Definition where
@@ -33,11 +33,11 @@ MkAbstract {qty, type} =
 
 public export %inline
 (.type0) : Definition -> Term 0 0
-g.type0 = g.type.def
+g.type0 = g.type.get
 
 public export %inline
 (.term0) : Definition -> Maybe (Term 0 0)
-g.term0 = map (\t => t.def) g.term
+g.term0 = map (\t => t.get) g.term
 
 public export %inline
 (.qtyP) : Definition -> Subset Qty IsGlobal
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 8a70149..cbbf6cc 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -37,7 +37,7 @@ parameters {auto _ : MonadError Error m} {auto _ : MonadReader Env m}
   defE : Name -> m (Maybe (Elim d n))
   defE x = asks $ \env => do
     g <- lookup x env.defs
-    pure $ (!g.term).def :# g.type.def
+    pure $ (!g.term).get :# g.type.get
 
   private %inline
   defT : Name -> m (Maybe (Term d n))
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 93b9391..5156040 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -129,7 +129,7 @@ parameters {auto _ : CanTC m}
   infer' ctx sg (Element (F x) _) = do
     Just g <- asks $ lookup x  | Nothing => throwError $ NotInScope x
     when (isZero g) $ expectEqualQ sg Zero
-    pure $ InfRes {type = g.type.def, qout = zero}
+    pure $ InfRes {type = g.type.get, qout = zero}
 
   infer' ctx sg (Element (B i) _) =
     pure $ lookupBound sg i ctx