diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs
index ea1d7847c..8795e196b 100644
--- a/primer/src/Primer/Eval/NormalOrder.hs
+++ b/primer/src/Primer/Eval/NormalOrder.hs
@@ -88,6 +88,7 @@ import Primer.Eval.Redex (
     origBinder,
     var
   ),
+  cxtAddLet,
   viewRedex,
   viewRedexType,
   _freeVarsLetBinding,
@@ -128,29 +129,34 @@ data RedexWithContext
 data ViewLet = ViewLet
   { bindingVL :: LetBinding
   -- ^ the binding itself
-  , bodyVL :: Accum Cxt (Dir, ExprZ)
-  -- ^ the body (i.e. after the `in`)
-  , typeChildrenVL :: [Accum Cxt TypeZ]
-  -- ^ any non-body type children
-  , termChildrenVL :: [Accum Cxt (Dir, ExprZ)]
-  -- ^ any non-body term children (i.e. rhs of the binding)
+  , bodyVL :: (Maybe LetBinding, (Dir, ExprZ))
+  -- ^ the body (i.e. after the `in`), along with the newly in-scope bindings (this will always be @Just bindingVL@, but record it here for consistency)
+  -- , bodyVL::Accum Cxt (Dir, ExprZ) -- ^ the body (i.e. after the `in`)
+  , typeChildrenVL :: [(Maybe LetBinding, TypeZ)]
+  -- ^ any non-body type children, along with (potentially) the newly in-scope binding
+  , termChildrenVL :: [(Maybe LetBinding, (Dir, ExprZ))]
+  -- ^ any non-body term children (i.e. rhs of the binding), along with (potentially) the newly in-scope binding
+  -- , typeChildrenVL::[Accum Cxt TypeZ] -- ^ any non-body type children
+  -- , termChildrenVL ::[Accum Cxt (Dir, ExprZ)] -- ^ any non-body term children (i.e. rhs of the binding)
   }
 viewLet :: (Dir, ExprZ) -> Maybe ViewLet
 viewLet dez@(_, ez) = case (target ez, exprChildren dez) of
-  (Let _ x e _b, [ez', bz]) -> Just (ViewLet (LetBind x e) bz [] [ez'])
-  (Letrec _ x e ty _b, [ez', bz]) -> Just (ViewLet (LetrecBind x e ty) bz tz [ez'])
-  (LetType _ a ty _b, [bz]) -> bz `seq` Just (ViewLet (LetTyBind $ LetTypeBind a ty) bz tz [])
+  (Let _ x e _b, [ez', bz]) -> let l = LetBind x e in Just (ViewLet l (Just l, bz) [] [(Nothing, ez')])
+  (Letrec _ x e ty _b, [ez', bz]) -> let l = LetrecBind x e ty in Just (ViewLet l (Just l, bz) tz [(Just l, ez')])
+  (LetType _ a ty _b, [bz]) -> bz `seq` let l = LetTyBind $ LetTypeBind a ty in Just (ViewLet l (Just l, bz) tz [])
   _ -> Nothing
   where
-    tz :: [Accum Cxt TypeZ]
+    tz :: [(Maybe LetBinding, TypeZ)]
     -- as with focusType', we don't need to bind anything here
-    tz = maybe [] ((: []) . pure) $ focusType ez
+    tz = maybe [] ((: []) . (Nothing,)) $ focusType ez
 
 -- | This is similar to 'foldMap', with a few differences:
 -- - 'Expr' is not foldable
 -- - We target every subexpression and also every (nested) subtype (e.g. in an annotation)
 -- - We keep track of context and directionality (necessitating an extra 'Dir' argument, for "what directional context this whole expression is in")
+-- TODO: the "context" is just of the immediately-enclosing lets, which are the only ones that may "cross a binder"
 -- - We handle @let@s specially, since we need to handle them differently when finding the normal order redex.
+-- TODO: do we still "handle lets specially", i.e. do we ever set subst = Just ...?
 --   (When we hit the body of a @let@ (of any flavor), we use the provided 'subst' or 'substTy' argument, if provided, and do no further recursion.
 --   If the corresponding argument is 'Nothing', then we recurse as normal.)
 -- - We accumulate in some 'f a' for 'MonadPlus f' rather than an arbitrary monoid
@@ -163,35 +169,36 @@ viewLet dez@(_, ez) = case (target ez, exprChildren dez) of
 -- both reducing type annotations more than needed, and reducing type applications when not needed.
 -- Since computation in types is strongly normalising, this will not cause us to fail to find any normal forms.
 foldMapExpr :: forall f a. MonadPlus f => FMExpr (f a) -> Dir -> Expr -> f a
-foldMapExpr extract topDir = flip evalAccumT mempty . go . (topDir,) . focus
+foldMapExpr extract topDir = go mempty . (topDir,) . focus
   where
-    go :: (Dir, ExprZ) -> AccumT Cxt f a
-    go dez@(d, ez) =
-      readerToAccumT (ReaderT $ extract.expr ez d)
+    cxtAddLet' l c = maybe c (`cxtAddLet` c) l
+    go :: Cxt -> (Dir, ExprZ) -> f a
+    go lets dez@(d, ez) =
+      extract.expr ez d lets
         <|> case (extract.subst, viewLet dez) of
-          (Just goSubst, Just (ViewLet{bindingVL, bodyVL})) -> (readerToAccumT . ReaderT . (\(d', b) -> goSubst bindingVL b d')) =<< hoistAccum bodyVL
+          (Just goSubst, Just (ViewLet{bindingVL, bodyVL = (l, (d', b))})) -> goSubst bindingVL b d' $ cxtAddLet' l lets -- ((\(d', b) -> goSubst bindingVL b d')) =<< hoistAccum bodyVL
           -- Prefer to compute inside the body of a let, but otherwise compute in the binding
-          (Nothing, Just (ViewLet{bodyVL, typeChildrenVL, termChildrenVL})) ->
+          (Nothing, Just (ViewLet{bodyVL = (bodyLet, b), typeChildrenVL, termChildrenVL})) ->
             msum $
-              (go =<< hoistAccum bodyVL)
-                : map (goType <=< hoistAccum) typeChildrenVL
-                  <> map (go <=< hoistAccum) termChildrenVL
+              go (cxtAddLet' bodyLet lets) b
+                : map (\(l, tz) -> goType (cxtAddLet' l lets) tz) typeChildrenVL
+                  <> map (\(l, c) -> go (cxtAddLet' l lets) c) termChildrenVL
           -- Since stuck things other than lets are stuck on the first child or
           -- its type annotation, we can handle them all uniformly
           _ ->
             msum $
-              (goType =<< focusType' ez)
-                : map (go <=< hoistAccum) (exprChildren dez)
-    goType :: TypeZ -> AccumT Cxt f a
-    goType tz =
-      readerToAccumT (ReaderT $ extract.ty tz)
+              (goType mempty =<< focusType' ez)
+                : map (go mempty) (exprChildren dez)
+    goType :: Cxt -> TypeZ -> f a
+    goType lets tz =
+      extract.ty tz lets
         <|> case (extract.substTy, target tz) of
           (Just goSubstTy, TLet _ a t _body)
-            | [_, bz] <- typeChildren tz -> (readerToAccumT . ReaderT . goSubstTy a t) =<< hoistAccum bz
-          (Nothing, TLet _ a _t _body)
+            | [_, bz] <- typeChildren tz -> goSubstTy a t bz lets
+          (Nothing, TLet _ a t _body)
             -- Prefer to compute inside the body of a let, but otherwise compute in the binding
-            | [tz', bz] <- typeChildren tz -> (goType =<< hoistAccum bz) <|> (goType =<< hoistAccum tz')
-          _ -> msum $ map (goType <=< hoistAccum) $ typeChildren tz
+            | [tz, bz] <- typeChildren tz -> goType (cxtAddLet (LetTyBind $ LetTypeBind a t) lets) bz <|> goType lets tz
+          _ -> msum $ map (goType mempty) $ typeChildren tz
 
 data FMExpr m = FMExpr
   { expr :: ExprZ -> Dir -> Cxt -> m
@@ -200,9 +207,7 @@ data FMExpr m = FMExpr
   , substTy :: Maybe (TyVarName -> Type -> TypeZ -> Cxt -> m)
   }
 
-focusType' :: MonadPlus m => ExprZ -> AccumT Cxt m TypeZ
--- Note that nothing in Expr binds a variable which scopes over a type child
--- so we don't need to 'add' anything
+focusType' :: MonadPlus m => ExprZ -> m TypeZ
 focusType' = maybe empty pure . focusType
 
 hoistAccum :: Monad m => Accum Cxt b -> AccumT Cxt m b
@@ -232,7 +237,7 @@ children' z = case down z of
   Nothing -> mempty
   Just z' -> z' : unfoldr (fmap (\x -> (x, x)) . right) z'
 
-exprChildren :: (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)]
+exprChildren :: (Dir, ExprZ) -> [(Dir, ExprZ)]
 exprChildren (d, ez) =
   children' ez <&> \c -> do
     let bs = getBoundHere' (target ez) (Just $ target c)
@@ -251,15 +256,13 @@ exprChildren (d, ez) =
             | e == target c -> Chk
             | otherwise -> d
           _ -> Chk
-    addBinds ez bs
-    pure (d', c)
+    (d', c)
 
-typeChildren :: TypeZ -> [Accum Cxt TypeZ]
+typeChildren :: TypeZ -> [TypeZ]
 typeChildren tz =
   children' tz <&> \c -> do
     let bs = getBoundHereTy' (target tz) (Just $ target c)
-    addBinds tz $ bimap unLocalName LetTyBind <$> bs
-    pure c
+    c
 
 addBinds :: HasID i => i -> [Either Name LetBinding] -> Accum Cxt ()
 addBinds i' bs = do
diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs
index e1bd8b048..228b6310b 100644
--- a/primer/src/Primer/Eval/Redex.hs
+++ b/primer/src/Primer/Eval/Redex.hs
@@ -12,6 +12,7 @@ module Primer.Eval.Redex (
   runRedexTy,
   Dir (Syn, Chk),
   Cxt (Cxt),
+  cxtAddLet,
   _freeVarsLetBinding,
   EvalLog (..),
   MonadEval,
@@ -614,6 +615,7 @@ viewCaseRedex tydefs = \case
     formCaseRedex con argTys params args binders rhs (orig, scrut, conID) =
       CaseRedex{con, args, argTys, params, binders, rhs, orig, scrutID = getID scrut, conID}
 
+-- TODO: don't need to record nearly so much anymore -- a list of directly-enclosing let bindings would be good enough
 -- We record each binder, along with its let-bound RHS (if any)
 -- and its original binding location and  context (to be able to detect capture)
 -- Invariant: lookup x c == Just (Just l,_,_) ==> letBindingName l == x
@@ -622,6 +624,9 @@ newtype Cxt = Cxt (M.Map Name (Maybe LetBinding, ID, Cxt))
   -- and want later 'add's to overwrite earlier (more-global) context entries
   deriving (Semigroup, Monoid) via Dual (M.Map Name (Maybe LetBinding, ID, Cxt))
 
+cxtAddLet :: LetBinding -> Cxt -> Cxt
+cxtAddLet l (Cxt c) = Cxt $ M.insert (letBindingName l) (Just l, 0, mempty) c -- TODO: the 0, mempty are LIES, but we never care about these positions...
+
 lookup :: Name -> Cxt -> Maybe (Maybe LetBinding, ID, Cxt)
 lookup n (Cxt cxt) = M.lookup n cxt
 
diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs
index 2f6a00b17..db10101af 100644
--- a/primer/test/Tests/Eval.hs
+++ b/primer/test/Tests/Eval.hs
@@ -848,7 +848,6 @@ unit_findNodeByID_1 = do
     Just (locals, Left (_, z)) -> do
       case lookupNonCaptured "x" locals of
         Just (i, LetBind _ e) -> do
-          i @?= 2
           e ~= c
         Just _ -> assertFailure "expected to find 'x' let-bound, but found some other flavor of let"
         Nothing -> assertFailure "expected to find 'x' bound, but did not"
@@ -880,11 +879,8 @@ unit_findNodeByID_2 = do
   case findNodeByID 0 Syn expr of
     Just (locals, Right z) -> do
       case lookupNonCaptured "x" locals of
-        Just (i, LetTyBind (LetTypeBind _ e)) -> do
-          i @?= 2
-          e ~~= t
-        Just _ -> assertFailure "expected to find a type 'x' bound, but found a term"
-        Nothing -> assertFailure "expected to find 'x' bound, but did not"
+        Nothing -> pure ()
+        Just _ -> assertFailure "expected 'x' to not be bound by an immediately enclosing let, but it was"
       target z ~~= x
     _ -> assertFailure "node 0 not found"
 
@@ -902,7 +898,6 @@ unit_findNodeByID_tlet = do
     Just (locals, Right z) -> do
       case lookupNonCaptured "x" locals of
         Just (i, LetTyBind (LetTypeBind _ e)) -> do
-          i @?= 4
           e ~~= t
         Just _ -> assertFailure "expected to find a type 'x' bound, but found a term"
         Nothing -> assertFailure "expected to find 'x' bound, but did not"
@@ -914,9 +909,9 @@ unit_findNodeByID_scoping_1 = do
   let expr = create' $ let_ "x" (con0' ["M"] "C") $ lam "x" $ lvar "x"
   case findNodeByID 3 Syn expr of
     Just (Cxt locals, Left _)
-      | Just (Nothing, _, _) <- Map.lookup "x" locals ->
+      | Nothing <- Map.lookup "x" locals ->
           pure ()
-      | otherwise -> assertFailure "Expected 'x' to be in scope but not have a substitution"
+      | otherwise -> assertFailure "expected 'x' to not be bound by an immediately enclosing let, but it was"
     _ -> assertFailure "Expected to find the lvar 'x'"
 
 unit_findNodeByID_scoping_2 :: Assertion
@@ -928,7 +923,7 @@ unit_findNodeByID_scoping_2 = do
   case findNodeByID 4 Syn expr of
     Just (locals@(Cxt locals'), Left _)
       | Map.size locals' == 1
-      , lookupNonCaptured "x" locals == Just (3, LetBind "x" bind) ->
+      , (snd <$> lookupNonCaptured "x" locals) == Just (LetBind "x" bind) ->
           pure ()
     Just (_, Left _) -> assertFailure "Expected to have inner let binding of 'x' reported"
     _ -> assertFailure "Expected to find the lvar 'x'"
@@ -946,10 +941,10 @@ unit_findNodeByID_capture =
    in do
         case findNodeByID varOcc Syn expr of
           Just (locals@(Cxt locals'), Left _)
-            | Map.size locals' == 2
-            , Just (1, LetrecBind{}) <- lookupCaptured "x" locals ->
+            | Map.size locals' == 0
+            , Nothing <- lookupCaptured "x" locals ->
                 pure ()
-          Just (_, Left _) -> assertFailure "Expected let binding of 'x' to be reported as captured-if-inlined"
+            | otherwise -> assertFailure "expected 'x' to not be bound by an immediately enclosing let, but it was"
           _ -> assertFailure "Expected to find the lvar 'x'"
         reduct <- runStep maxID mempty mempty (expr, varOcc)
         case reduct of
@@ -965,11 +960,11 @@ unit_findNodeByID_capture_type =
    in do
         case findNodeByID varOcc Syn expr of
           Just (locals@(Cxt locals'), Right _)
-            | Map.size locals' == 3
-            , Just (1, LetTyBind _) <- lookupCaptured "x" locals
-            , Just (5, LetTyBind _) <- lookupCaptured "z" locals ->
+            | Map.size locals' == 0
+            , Nothing <- lookupCaptured "x" locals
+            , Nothing <- lookupCaptured "z" locals ->
                 pure ()
-          Just (_, Right _) -> assertFailure "Expected lettype binding of 'x' and the tlet binding of 'z' to be reported as captured-if-inlined" -- TODO: can probably remove all the "captured-if-inlined" stuff as don't do inlining like that now
+            | otherwise -> assertFailure "expected 'x' to not be bound by an immediately enclosing let, but it was"
           _ -> assertFailure "Expected to find the lvar 'x'"
         reduct <- runStep maxID mempty mempty (expr, varOcc)
         case reduct of
@@ -1166,12 +1161,7 @@ unit_redexes_let_capture =
 unit_redexes_lettype_capture :: Assertion
 unit_redexes_lettype_capture = do
   -- We can push the letType down once
-  -- TODO: we don't really want the "forall y" to be a redex -- it is only a
-  -- rename, and not blocking anything yet. It would be preferable to only
-  -- consider renaming binders when they are immediately under the corresponding
-  -- @let@ (actually, immediately under a group of @let@s containing the
-  -- corresponding one).
-  redexesOf (letType "x" (tvar "y") (emptyHole `ann` tforall "y" KType (tvar "x"))) <@?=> Set.fromList [0, 4]
+  redexesOf (letType "x" (tvar "y") (emptyHole `ann` tforall "y" KType (tvar "x"))) <@?=> Set.singleton 0 -- TODO: we don't want the "forall y" to be a redex, do we? It is only a rename, and not blocking anything yet...
   -- But now we should rename the forall and not push the tlet further
   redexesOf (emptyHole `ann` tlet "x" (tvar "y") (tforall "y" KType (tvar "x"))) <@?=> Set.singleton 4