diff --git a/src/Elaboration/Context.hs b/src/Elaboration/Context.hs
index 70a30a1..0358ea4 100644
--- a/src/Elaboration/Context.hs
+++ b/src/Elaboration/Context.hs
@@ -74,7 +74,6 @@ data Context (v :: Data.Kind.Type) = Context
   , indices :: Index.Map v Var
   , surfaceNames :: HashMap Name.Surface (Domain.Value, Domain.Type)
   , varNames :: EnumMap Var Name
-  , values :: EnumMap Var Domain.Value
   , types :: EnumMap Var Domain.Type
   , boundVars :: IntSeq Var
   , metas :: !(IORef (Meta.State M))
@@ -115,7 +114,6 @@ empty definitionKind definitionName = do
       , surfaceNames = mempty
       , varNames = mempty
       , indices = Index.Map.Empty
-      , values = mempty
       , types = mempty
       , boundVars = mempty
       , metas = ms
@@ -134,7 +132,6 @@ emptyFrom context =
     , surfaceNames = mempty
     , varNames = mempty
     , indices = Index.Map.Empty
-    , values = mempty
     , types = mempty
     , boundVars = mempty
     , metas = context.metas
@@ -220,7 +217,10 @@ extendSurfaceDef context surfaceName@(Name.Surface nameText) value type_ = do
         { surfaceNames = HashMap.insert surfaceName (Domain.var var, type_) context.surfaceNames
         , varNames = EnumMap.insert var (Name nameText) context.varNames
         , indices = context.indices Index.Map.:> var
-        , values = EnumMap.insert var value context.values
+        , equations =
+            context.equations
+              { equal = HashMap.insert (Domain.Var var) [(Domain.Empty, value)] context.equations.equal
+              }
         , types = EnumMap.insert var type_ context.types
         }
     , var
@@ -244,7 +244,10 @@ extendDef context name value type_ = do
     ( context
         { varNames = EnumMap.insert var name context.varNames
         , indices = context.indices Index.Map.:> var
-        , values = EnumMap.insert var value context.values
+        , equations =
+            context.equations
+              { equal = HashMap.insert (Domain.Var var) [(Domain.Empty, value)] context.equations.equal
+              }
         , types = EnumMap.insert var type_ context.types
         }
     , var
@@ -272,10 +275,15 @@ extendBefore context beforeVar binding type_ = do
     )
 
 defineWellOrdered :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> Context v
-defineWellOrdered context var value =
+defineWellOrdered context head spine value =
   context
-    { values = EnumMap.insert var value context.values
-    , boundVars = IntSeq.delete var context.boundVars
+    { equations =
+        context.equations
+          { equal = HashMap.insertWith (<>) head [(spine, value)] context.equations.equal
+          }
+    , boundVars = case (head, spine) of
+        (Domain.Var var, Domain.Empty) -> IntSeq.delete var context.boundVars
+        _ -> context.boundVars
     }
 
 skip :: Context v -> M (Context (Succ v))
@@ -283,10 +291,10 @@ skip context = do
   (context', _) <- extendDef context "skip" Builtin.Type Builtin.Type
   pure context'
 
-define :: Context v -> Var -> Domain.Value -> M (Context v)
-define context var value = do
-  deps <- evalStateT (dependencies context value) mempty
-  let context' = defineWellOrdered context var value
+define :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> M (Context v)
+define context head spine value = do
+  deps <- evalStateT (freeVars context value) mempty
+  let context' = defineWellOrdered context head spine value
       (pre, post) =
         Tsil.partition (`EnumSet.member` deps) $
           IntSeq.toTsil context'.boundVars
@@ -297,51 +305,51 @@ define context var value = do
       }
 
 -- TODO: Move
-dependencies
+freeVars
   :: Context v
   -> Domain.Value
   -> StateT (EnumMap Var (EnumSet Var)) M (EnumSet Var)
-dependencies context value = do
+freeVars context value = do
   value' <- lift $ forceHeadGlue context value
   case value' of
     Domain.Neutral hd spine -> do
       hdVars <- headVars hd
-      elimVars <- Domain.mapM eliminationDependencies spine
+      elimVars <- Domain.mapM eliminationVars spine
       pure $ hdVars <> fold elimVars
     Domain.Con _ args ->
-      fold <$> mapM (dependencies context . snd) args
+      fold <$> mapM (freeVars context . snd) args
     Domain.Lit _ ->
       pure mempty
     Domain.Glued (Domain.Global _) spine _ ->
-      fold <$> Domain.mapM eliminationDependencies spine
+      fold <$> Domain.mapM eliminationVars spine
     Domain.Glued _ _ value'' ->
-      dependencies context value''
+      freeVars context value''
     Domain.Lazy lazyValue -> do
       value'' <- lift $ force lazyValue
-      dependencies context value''
+      freeVars context value''
     Domain.Lam bindings type' _ closure ->
-      abstractionDependencies (Bindings.toName bindings) type' closure
+      abstractionVars (Bindings.toName bindings) type' closure
     Domain.Pi binding type' _ closure ->
-      abstractionDependencies (Binding.toName binding) type' closure
+      abstractionVars (Binding.toName binding) type' closure
     Domain.Fun domain _ target -> do
-      domainVars <- dependencies context domain
-      targetVars <- dependencies context target
+      domainVars <- freeVars context domain
+      targetVars <- freeVars context target
       pure $ domainVars <> targetVars
   where
-    eliminationDependencies elimination =
+    eliminationVars elimination =
       case elimination of
         Domain.App _plicity arg ->
-          dependencies context arg
+          freeVars context arg
         Domain.Case (Domain.Branches env branches defaultBranch) -> do
-          defaultBranchVars <- mapM (dependencies context <=< lift . Evaluation.evaluate env) defaultBranch
+          defaultBranchVars <- mapM (freeVars context <=< lift . Evaluation.evaluate env) defaultBranch
           brVars <- branchVars context env branches
           pure $ fold defaultBranchVars <> brVars
 
-    abstractionDependencies name type' closure = do
-      typeVars <- dependencies context type'
+    abstractionVars name type' closure = do
+      typeVars <- freeVars context type'
       (context', var) <- lift $ extend context name type'
       body <- lift $ Evaluation.evaluateClosure closure $ Domain.var var
-      bodyVars <- dependencies context' body
+      bodyVars <- freeVars context' body
       pure $ typeVars <> EnumSet.delete var bodyVars
 
     headVars hd =
@@ -351,7 +359,7 @@ dependencies context value = do
               cache <- get
               typeDeps <- case EnumMap.lookup v cache of
                 Nothing -> do
-                  typeDeps <- dependencies context $ lookupVarType v context
+                  typeDeps <- freeVars context $ lookupVarType v context
                   modify $ EnumMap.insert v typeDeps
                   pure typeDeps
                 Just typeDeps ->
@@ -378,7 +386,7 @@ dependencies context value = do
           Syntax.LiteralBranches literalBranches ->
             forM (toList literalBranches) \(_, branch) -> do
               branch' <- lift $ Evaluation.evaluate env branch
-              dependencies context' branch'
+              freeVars context' branch'
 
     telescopeVars
       :: Context v
@@ -389,10 +397,10 @@ dependencies context value = do
       case tele of
         Telescope.Empty body -> do
           body' <- lift $ Evaluation.evaluate env body
-          dependencies context' body'
+          freeVars context' body'
         Telescope.Extend binding domain _ tele' -> do
           domain' <- lift $ Evaluation.evaluate env domain
-          domainVars <- dependencies context' domain'
+          domainVars <- freeVars context' domain'
           (context'', var) <- lift $ extend context' (Bindings.toName binding) domain'
           let env' =
                 Environment.extendVar env var
@@ -427,10 +435,6 @@ lookupVarType :: Var -> Context v -> Domain.Type
 lookupVarType var context =
   EnumMap.findWithDefault (panic $ "Context.lookupVarType " <> show var) var context.types
 
-lookupVarValue :: Var -> Context v -> Maybe Domain.Type
-lookupVarValue var context =
-  EnumMap.lookup var context.values
-
 -------------------------------------------------------------------------------
 -- Prettyable terms
 
@@ -492,12 +496,7 @@ newMetaReturningIndex context type_ = do
 piBoundVars :: Context v -> Domain.Type -> M (Syntax.Type Void, Int)
 piBoundVars context type_ = do
   let arity = IntSeq.length context.boundVars
-  piType <-
-    varPis
-      context
-      Environment.empty {Environment.values = context.values}
-      ((Explicit,) <$> toList context.boundVars)
-      type_
+  piType <- varPis context Environment.empty ((Explicit,) <$> toList context.boundVars) type_
   pure (piType, arity)
 
 varPis
@@ -600,7 +599,7 @@ forceHead context value =
         Meta.EagerUnsolved {} ->
           pure value
     Domain.Neutral head spine
-      | Just spineValues <- HashMap.lookup head context.equalities.equal -> do
+      | Just spineValues <- HashMap.lookup head context.equations.equal -> do
           let go [] = pure value
               go ((eqSpine, eqValue) : rest)
                 | Just (spinePrefix, spineSuffix) <- Domain.matchSpinePrefix spine eqSpine = do
@@ -639,7 +638,7 @@ forceHeadGlue context value =
         Meta.EagerUnsolved {} ->
           pure value
     Domain.Neutral head spine
-      | Just spineValues <- HashMap.lookup head context.equalities.equal -> do
+      | Just spineValues <- HashMap.lookup head context.equations.equal -> do
           let go [] = pure value
               go ((eqSpine, eqValue) : rest)
                 | Just (spinePrefix, spineSuffix) <- Domain.matchSpinePrefix spine eqSpine = do
diff --git a/src/Elaboration/Matching.hs b/src/Elaboration/Matching.hs
index 0244bde..fa0ba4a 100644
--- a/src/Elaboration/Matching.hs
+++ b/src/Elaboration/Matching.hs
@@ -603,7 +603,7 @@ expandAnnotations context matches =
                 pure ()
               pure $ Match value forcedValue plicity (unresolvedPattern pat) type_ : matches'
             _ ->
-              fail "couldn't create instantitation for prefix"
+              fail "couldn't create instantiation for prefix"
 
 matchInstantiation :: Match -> Maybe PatternInstantiation
 matchInstantiation match =
@@ -615,7 +615,7 @@ matchInstantiation match =
     Match _ _ _ (Pattern _ (Forced _)) _ ->
       pure mempty
     _ ->
-      fail "No match instantitation"
+      fail "No match instantiation"
 
 solved :: [Match] -> Maybe PatternInstantiation
 solved =
@@ -665,18 +665,17 @@ splitConstructor outerContext config scrutineeValue scrutineeHead scrutineeSpine
         _ -> do
           typeType <- fetch $ Query.ElaboratedType typeName
           typeType' <- Evaluation.evaluate Environment.empty typeType
-          let
-            contextWithoutScrutineeVar =
-              case scrutineeHead of
-                Domain.Var scrutineeVar ->
-                  -- Ensure the metas don't depend on the scrutineeVar, because that
-                  -- is guaranteed to lead to circularity when solving scrutineeVar
-                  -- later.
-                  outerContext
-                    { Context.boundVars = IntSeq.delete scrutineeVar outerContext.boundVars
-                    }
-                -- TODO: is this correct?
-                _ -> outerContext
+          let contextWithoutScrutineeVar =
+                case scrutineeHead of
+                  Domain.Var scrutineeVar ->
+                    -- Ensure the metas don't depend on the scrutineeVar, because that
+                    -- is guaranteed to lead to circularity when solving scrutineeVar
+                    -- later.
+                    outerContext
+                      { Context.boundVars = IntSeq.delete scrutineeVar outerContext.boundVars
+                      }
+                  -- TODO: is this correct?
+                  _ -> outerContext
           (metas, _) <- Elaboration.insertMetas contextWithoutScrutineeVar Elaboration.UntilTheEnd typeType'
           f <- Unification.tryUnify outerContext (Domain.Neutral (Domain.Global typeName) $ Domain.Apps $ fromList metas) outerType
           result <- goParams (Context.spanned span outerContext) metas mempty tele'