diff --git a/primer/primer.cabal b/primer/primer.cabal
index fc1f27669..776229139 100644
--- a/primer/primer.cabal
+++ b/primer/primer.cabal
@@ -79,6 +79,7 @@ library
     Primer.Eval.Let
     Primer.Eval.NormalOrder
     Primer.Eval.Prim
+    Primer.Eval.Push
     Primer.Primitives.PrimDef
     Primer.Typecheck.Cxt
     Primer.Typecheck.Kindcheck
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 2d51bf1ab..e038b3d3d 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -181,7 +181,7 @@ import Primer.Def (
 import Primer.Def.Utils (globalInUse, typeInUse)
 import Primer.Eval qualified as Eval
 import Primer.Eval.Detail (EvalDetail)
-import Primer.Eval.Redex (EvalLog)
+import Primer.Eval.Redex (EvalLog, RunRedexOptions (RunRedexOptions,pushAndElide), ViewRedexOptions (ViewRedexOptions, pushMulti))
 import Primer.EvalFull (Dir (Syn), EvalFullError (TimedOut), TerminationBound, evalFull)
 import Primer.JSON
 import Primer.Log (ConvertLogMessage)
@@ -592,7 +592,9 @@ handleEvalFullRequest ::
 handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxSteps}) = do
   app <- ask
   let prog = appProg app
-  result <- runFreshM app $ evalFull (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
+  let optsV = ViewRedexOptions { pushMulti = True, aggressiveElision = True }
+  let optsR = RunRedexOptions { pushAndElide = True }
+  result <- runFreshM app $ evalFull optsV optsR (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
   pure $ case result of
     Left (TimedOut e) -> EvalFullRespTimedOut e
     Right nf -> EvalFullRespNormal nf
diff --git a/primer/src/Primer/Eval.hs b/primer/src/Primer/Eval.hs
index 40ae50a28..30bf997cb 100644
--- a/primer/src/Primer/Eval.hs
+++ b/primer/src/Primer/Eval.hs
@@ -5,6 +5,8 @@ module Primer.Eval (
   -- The public API of this module
   step,
   redexes,
+  RunRedexOptions (..),
+  ViewRedexOptions (..),
   EvalLog (..),
   EvalError (..),
   EvalDetail (..),
@@ -16,10 +18,11 @@ module Primer.Eval (
   GlobalVarInlineDetail (..),
   LetRemovalDetail (..),
   ApplyPrimFunDetail (..),
+  PushLetDetail (..),
   -- Only exported for testing
   Cxt (Cxt),
   singletonCxt,
-  getNonCapturedLocal,
+  lookupEnclosingLet,
   tryReduceExpr,
   tryReduceType,
   findNodeByID,
@@ -49,10 +52,11 @@ import Primer.Eval.Detail (
   GlobalVarInlineDetail (..),
   LetRemovalDetail (..),
   LocalVarInlineDetail (..),
+  PushLetDetail (..),
  )
 import Primer.Eval.EvalError (EvalError (..))
 import Primer.Eval.NormalOrder (
-  FMExpr (FMExpr, expr, subst, substTy, ty),
+  FMExpr (FMExpr, expr, ty),
   foldMapExpr,
   singletonCxt,
  )
@@ -61,11 +65,11 @@ import Primer.Eval.Redex (
   Dir (..),
   EvalLog (..),
   MonadEval,
-  getNonCapturedLocal,
+  lookupEnclosingLet,
   runRedex,
   runRedexTy,
   viewRedex,
-  viewRedexType,
+  viewRedexType, RunRedexOptions (RunRedexOptions,pushAndElide), ViewRedexOptions (ViewRedexOptions,aggressiveElision, pushMulti),
  )
 import Primer.Log (ConvertLogMessage)
 import Primer.TypeDef (TypeDefMap)
@@ -101,8 +105,8 @@ step tydefs globals expr d i = runExceptT $ do
       pure (expr', detail)
 
 -- | Search for the given node by its ID.
--- Collect all local bindings in scope and return them
--- (with their local definition, if applicable)
+-- Collect all immediately-surrounding let bindings and return them
+-- (these are the ones we may push into this node)
 -- along with the focused node.
 -- Returns Nothing if the node is a binding, (note that no reduction rules can apply there).
 findNodeByID :: ID -> Dir -> Expr -> Maybe (Cxt, Either (Dir, ExprZ) TypeZ)
@@ -111,10 +115,14 @@ findNodeByID i =
     FMExpr
       { expr = \ez d c -> if getID ez == i then Just (c, Left (d, ez)) else Nothing
       , ty = \tz c -> if getID tz == i then Just (c, Right tz) else Nothing
-      , subst = Nothing
-      , substTy = Nothing
       }
 
+-- We hardcode a permissive set of options for the interactive eval
+-- (i.e. these see more redexes)
+evalOpts :: ViewRedexOptions
+evalOpts = ViewRedexOptions {pushMulti = True
+  , aggressiveElision = True}
+
 -- | Return the IDs of nodes which are reducible.
 -- We assume that the expression is well scoped. There are no
 -- guarantees about whether we will claim that an ill-sorted variable
@@ -131,10 +139,8 @@ redexes tydefs globals =
   (ListT.toList .)
     . foldMapExpr
       FMExpr
-        { expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex tydefs globals d (target ez))
-        , ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType (target tz))
-        , subst = Nothing
-        , substTy = Nothing
+        { expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex evalOpts tydefs globals d (target ez))
+        , ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType evalOpts (target tz))
         }
   where
     liftMaybeT :: Monad m' => MaybeT m' a -> ListT m' a
@@ -142,6 +148,10 @@ redexes tydefs globals =
     -- whenJust :: Alternative f => a -> Maybe b -> f a
     whenJust = maybe empty . const . pure
 
+-- We hardcode a particular set of reduction options for the interactive evaluator
+reductionOpts :: RunRedexOptions
+reductionOpts = RunRedexOptions {pushAndElide = True}
+
 -- | Given a context of local and global variables and an expression, try to reduce that expression.
 -- Expects that the expression is redex and will throw an error if not.
 tryReduceExpr ::
@@ -154,8 +164,8 @@ tryReduceExpr ::
   Expr ->
   m (Expr, EvalDetail)
 tryReduceExpr tydefs globals cxt dir expr =
-  runMaybeT (flip runReaderT cxt $ viewRedex tydefs globals dir expr) >>= \case
-    Just r -> runRedex r
+  runMaybeT (flip runReaderT cxt $ viewRedex evalOpts tydefs globals dir expr) >>= \case
+    Just r -> runRedex reductionOpts r
     _ -> throwError NotRedex
 
 tryReduceType ::
@@ -167,6 +177,6 @@ tryReduceType ::
   Type ->
   m (Type, EvalDetail)
 tryReduceType _globals cxt =
-  flip runReader cxt . viewRedexType <&> \case
-    Just r -> runRedexTy r
+  flip runReader cxt . viewRedexType evalOpts <&> \case
+    Just r -> runRedexTy reductionOpts r
     _ -> throwError NotRedex
diff --git a/primer/src/Primer/Eval/Detail.hs b/primer/src/Primer/Eval/Detail.hs
index db57ff522..f10533257 100644
--- a/primer/src/Primer/Eval/Detail.hs
+++ b/primer/src/Primer/Eval/Detail.hs
@@ -9,6 +9,7 @@ module Primer.Eval.Detail (
   module Case,
   module Let,
   module Prim,
+  module Push,
 ) where
 
 import Foreword
@@ -23,6 +24,7 @@ import Primer.Eval.Case as Case
 import Primer.Eval.Inline as Inline
 import Primer.Eval.Let as Let
 import Primer.Eval.Prim as Prim
+import Primer.Eval.Push as Push
 import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
 
 -- | Detailed information about a reduction step
@@ -41,6 +43,9 @@ data EvalDetail
     LetRemoval (LetRemovalDetail Expr)
   | -- | Removing a type-level @let@ whose bound variable is unused
     TLetRemoval (LetRemovalDetail Type)
+  | -- | Explicit-substitution style pushing a 'let' down the tree
+    PushLetDown (PushLetDetail Expr)
+  | PushLetDownTy (PushLetDetail Type)
   | -- | Renaming of binding in an expression
     BindRename (BindRenameDetail Expr)
   | -- | Renaming of binding in a type
diff --git a/primer/src/Primer/Eval/Let.hs b/primer/src/Primer/Eval/Let.hs
index 44ba839c6..b4b68526a 100644
--- a/primer/src/Primer/Eval/Let.hs
+++ b/primer/src/Primer/Eval/Let.hs
@@ -2,23 +2,13 @@
 
 module Primer.Eval.Let (
   LetRemovalDetail (..),
-  findFreeOccurrencesExpr,
-  findFreeOccurrencesType,
 ) where
 
 import Foreword
 
-import Control.Arrow ((***))
-import Optics (filtered, getting, to, (%), (^..), _1)
 import Primer.Core (
-  Expr,
   ID,
-  LocalName (unLocalName),
-  TyVarName,
-  Type,
-  getID,
  )
-import Primer.Core.Utils (_freeVars, _freeVarsTy)
 import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
 import Primer.Name (Name)
 
@@ -32,20 +22,12 @@ data LetRemovalDetail t = LetRemovalDetail
   -- ^ the let expression before reduction
   , after :: t
   -- ^ the resulting expression after reduction
-  , bindingName :: Name
-  -- ^ the name of the unused bound variable (either term or type variable)
-  , letID :: ID
-  -- ^ the full let expression
+  , bindingNames :: NonEmpty Name
+  -- ^ the names of the unused bound variables (either term or type variable)
+  , letIDs :: NonEmpty ID
+  -- ^ the dropped let expressions
   , bodyID :: ID
   -- ^ the right hand side of the let
   }
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON (LetRemovalDetail t)
-
-findFreeOccurrencesExpr :: LocalName k -> Expr -> [ID]
-findFreeOccurrencesExpr x e = e ^.. _freeVars % to idName % filtered ((== unLocalName x) . snd) % _1
-  where
-    idName = either (getID *** unLocalName) (getID *** unLocalName)
-
-findFreeOccurrencesType :: TyVarName -> Type -> [ID]
-findFreeOccurrencesType x ty = ty ^.. getting _freeVarsTy % to (first getID) % filtered ((== x) . snd) % _1
diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs
index 0a196e99b..dd041401c 100644
--- a/primer/src/Primer/Eval/NormalOrder.hs
+++ b/primer/src/Primer/Eval/NormalOrder.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE DisambiguateRecordFields #-}
-{-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 
 module Primer.Eval.NormalOrder (
@@ -12,31 +11,9 @@ module Primer.Eval.NormalOrder (
 ) where
 
 import Foreword hiding (hoistAccum)
-import Foreword qualified
 
 import Control.Monad.Log (MonadLog, WithSeverity)
-import Control.Monad.Morph (generalize)
-import Control.Monad.Trans.Accum (
-  Accum,
-  AccumT,
-  add,
-  evalAccumT,
-  execAccum,
-  look,
-  readerToAccumT,
- )
 import Control.Monad.Trans.Maybe (MaybeT)
-import Data.Map qualified as M
-import Data.Set qualified as S
-import Data.Set.Optics (setOf)
-import Optics (
-  elemOf,
-  folded,
-  getting,
-  to,
-  (%),
-  _2,
- )
 import Primer.Core (
   Expr,
   Expr' (
@@ -48,18 +25,9 @@ import Primer.Core (
     LetType,
     Letrec
   ),
-  HasID,
-  LocalName (unLocalName),
-  TyVarName,
-  Type,
   Type' (
     TLet
   ),
-  bindName,
-  getID,
- )
-import Primer.Core.Utils (
-  _freeVarsTy,
  )
 import Primer.Def (
   DefMap,
@@ -68,35 +36,13 @@ import Primer.Eval.Redex (
   Cxt (..),
   Dir (..),
   EvalLog,
-  Redex (
-    ElideLet,
-    InlineLet,
-    InlineLetrec,
-    RenameBindingsCase,
-    RenameBindingsLAM,
-    RenameBindingsLam,
-    RenameSelfLet,
-    RenameSelfLetType,
-    branches,
-    letBinding,
-    tyvar,
-    var
-  ),
-  RedexType (
-    ElideLetInType,
-    InlineLetInType,
-    RenameForall,
-    RenameSelfLetInType,
-    letBinding,
-    origBinder,
-    var
-  ),
+  Redex,
+  RedexType,
+  cxtAddLet,
   viewRedex,
-  viewRedexType,
-  _freeVarsLetBinding,
+  viewRedexType, ViewRedexOptions,
  )
 import Primer.Log (ConvertLogMessage)
-import Primer.Name (Name)
 import Primer.TypeDef (
   TypeDefMap,
  )
@@ -109,16 +55,11 @@ import Primer.Zipper (
   down,
   focus,
   focusType,
-  getBoundHere,
-  getBoundHere',
-  getBoundHereTy,
-  letBindingName,
   right,
   target,
  )
 import Primer.Zipper.Type (
   LetTypeBinding' (LetTypeBind),
-  getBoundHereTy',
  )
 
 -- We don't really want a zipper here, but a one-hole context, but it is easier
@@ -128,17 +69,31 @@ data RedexWithContext
   = RExpr ExprZ Redex
   | RType TypeZ RedexType
 
-viewLet :: (Dir, ExprZ) -> Maybe (LetBinding, Accum Cxt (Dir, ExprZ))
+data ViewLet = ViewLet
+  { bindingVL :: LetBinding
+  -- ^ the binding itself
+  , bodyVL :: (Dir, ExprZ)
+  -- ^ the body (i.e. after the `in`)
+  , typeChildrenVL :: [TypeZ]
+  -- ^ any non-body type children
+  , termChildrenVL :: [(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, [_, bz]) -> Just (LetBind x e, bz)
-  (Letrec _ x e ty _b, [_, bz]) -> Just (LetrecBind x e ty, bz)
-  (LetType _ a ty _b, [bz]) -> bz `seq` Just (LetTyBind $ LetTypeBind a ty, bz)
+  (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 [])
   _ -> Nothing
+  where
+    tz :: [TypeZ]
+    tz = maybeToList $ 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")
+--   (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.
 --   (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.)
@@ -152,149 +107,69 @@ 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)
-        <|> case (extract.subst, viewLet dez) of
-          (Just goSubst, Just (l, bz)) -> (readerToAccumT . ReaderT . (\(d', b) -> goSubst l b d')) =<< hoistAccum bz
+    go :: Cxt -> (Dir, ExprZ) -> f a
+    go lets dez@(d, ez) =
+      extract.expr ez d lets
+        <|> case viewLet dez of
+          -- Prefer to compute inside the body of a let, but otherwise compute in the binding
+          -- NB: we never push lets into lets, so the Cxt is reset for non-body children
+          Just (ViewLet{bindingVL, bodyVL, typeChildrenVL, termChildrenVL}) ->
+            msum $
+              go (cxtAddLet bindingVL lets) bodyVL
+                : map (goType mempty) typeChildrenVL
+                  <> map (go mempty) termChildrenVL
           -- Since stuck things other than lets are stuck on the first child or
           -- its type annotation, we can handle them all uniformly
+          -- Since this node is not a let, the context is reset
           _ ->
             msum $
-              (goType =<< focusType' ez)
-                : map (go <=< hoistAccum) (exprChildren dez)
-    goType :: TypeZ -> AccumT Cxt f a
-    goType tz =
-      readerToAccumT (ReaderT $ extract.ty tz)
-        <|> case (extract.substTy, target tz) of
-          (Just goSubstTy, TLet _ a t _body)
-            | [_, bz] <- typeChildren tz -> (readerToAccumT . ReaderT . goSubstTy a t) =<< hoistAccum bz
-          _ -> msum $ map (goType <=< hoistAccum) $ typeChildren tz
+              (goType mempty =<< focusType' ez)
+                : map (go mempty) (exprChildren dez)
+    goType :: Cxt -> TypeZ -> f a
+    goType lets tz =
+      extract.ty tz lets
+        <|> case target tz of
+          TLet _ a t _body
+            -- Prefer to compute inside the body of a let, but otherwise compute in the binding
+            | [tz', bz] <- typeChildren tz -> goType (cxtAddLet (LetTyBind $ LetTypeBind a t) lets) bz <|> goType mempty tz'
+          _ -> msum $ map (goType mempty) $ typeChildren tz
 
 data FMExpr m = FMExpr
   { expr :: ExprZ -> Dir -> Cxt -> m
   , ty :: TypeZ -> Cxt -> m
-  , subst :: Maybe (LetBinding -> ExprZ {- The body of the let-} -> Dir -> Cxt -> m)
-  , 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
-hoistAccum = Foreword.hoistAccum generalize
-
 -- We find the normal-order redex.
--- Annoyingly this is not quite leftmost-outermost wrt our Expr type, as we
--- are using 'let's to encode something similar to explicit substitution, and
--- reduce them by substituting one occurrance at a time, removing the 'let'
--- when there are no more substitutions to be done. Note that the 'let' itself
--- doesn't get "pushed down" in the tree.
--- example:
---   lettype a = Bool -> Bool in (λx.not x : a) True
--- reduces to
---   lettype a = Bool -> Bool in (λx.not x : Bool -> Bool) True
--- and then to
---   (λx.not x : Bool -> Bool) True
--- This can be seen as "leftmost-outermost" if you consider the location of the
--- "expand a" redex to be the 'lettype' rather than the variable occurrance.
 findRedex ::
   forall l m.
   (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
+  ViewRedexOptions ->
   TypeDefMap ->
   DefMap ->
   Dir ->
   Expr ->
   MaybeT m RedexWithContext
-findRedex tydefs globals =
+findRedex opts tydefs globals =
   foldMapExpr
     ( FMExpr
-        { expr = \ez d -> runReaderT (RExpr ez <$> viewRedex tydefs globals d (target ez))
-        , ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType (target tz))
-        , subst = Just (\l -> fmap evalAccumT . goSubst l)
-        , substTy = Just (\v t -> fmap hoistMaybe . evalAccumT . goSubstTy v t)
+        { expr = \ez d -> runReaderT (RExpr ez <$> viewRedex opts tydefs globals d (target ez))
+        , ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType opts (target tz))
         }
     )
-  where
-    goSubst :: LetBinding -> ExprZ -> Dir -> AccumT Cxt (MaybeT m) RedexWithContext
-    goSubst l ez d = do
-      let here =
-            readerToAccumT (viewRedex tydefs globals d $ target ez) >>= \case
-              -- We should inline such 'v' (note that we will not go under any 'v' binders)
-              r@(InlineLet{var}) | letBindingName l == unLocalName var -> pure $ RExpr ez r
-              r@(InlineLetrec{var}) | letBindingName l == unLocalName var -> pure $ RExpr ez r
-              -- Elide a let only if it blocks the reduction
-              r@(ElideLet{letBinding}) | elemOf _freeVarsLetBinding (letBindingName letBinding) l -> pure $ RExpr ez r
-              -- Rename a binder only if it blocks the reduction
-              r@(RenameBindingsLam{var}) | elemOf _freeVarsLetBinding (unLocalName var) l -> pure $ RExpr ez r
-              r@(RenameBindingsLAM{tyvar}) | elemOf _freeVarsLetBinding (unLocalName tyvar) l -> pure $ RExpr ez r
-              r@(RenameBindingsCase{branches})
-                | not $ S.disjoint (setOf _freeVarsLetBinding l) (setOf (folded % #_CaseBranch % _2 % folded % to bindName % to unLocalName) branches) ->
-                    pure $ RExpr ez r
-              r@(RenameSelfLet{var}) | elemOf _freeVarsLetBinding (unLocalName var) l -> pure $ RExpr ez r
-              r@(RenameSelfLetType{tyvar}) | elemOf _freeVarsLetBinding (unLocalName tyvar) l -> pure $ RExpr ez r
-              _ -> mzero
-          -- Switch to an inner let if substituting under it would cause capture
-          innerLet = case viewLet (d, ez) of
-            Just (l', bz)
-              | letBindingName l' /= letBindingName l
-              , elemOf _freeVarsLetBinding (letBindingName l') l ->
-                  (\(d', b) -> goSubst l' b d') =<< hoistAccum bz
-            _ -> mzero
-          dive =
-            let substChild (d', c) = do
-                  -- We should not go under 'v' binders, but otherwise substitute in each child
-                  guard $ S.notMember (letBindingName l) $ getBoundHere (target ez) (Just $ target c)
-                  goSubst l c d'
-                substTyChild c = case l of
-                  LetTyBind (LetTypeBind v t) -> goSubstTy v t c
-                  _ -> mzero
-             in msum @[] $
-                  Foreword.hoistAccum hoistMaybe (substTyChild =<< focusType' ez)
-                    : map (substChild <=< hoistAccum) (exprChildren (d, ez))
-       in here <|> innerLet <|> dive
-    goSubstTy :: TyVarName -> Type -> TypeZ -> AccumT Cxt Maybe RedexWithContext
-    goSubstTy v t tz =
-      let isFreeIn = elemOf (getting _freeVarsTy % _2)
-       in do
-            hoistAccum (readerToAccumT $ viewRedexType $ target tz) >>= \case
-              -- We should inline such 'v' (note that we will not go under any 'v' binders)
-              Just r@(InlineLetInType{var}) | var == v -> pure $ RType tz r
-              -- Elide a let only if it blocks the reduction
-              Just r@(ElideLetInType{letBinding = (LetTypeBind w _)}) | w `isFreeIn` t -> pure $ RType tz r
-              -- Rename a binder only if it blocks the reduction
-              Just r@(RenameSelfLetInType{letBinding = (LetTypeBind w _)}) | w `isFreeIn` t -> pure $ RType tz r
-              Just r@(RenameForall{origBinder}) | origBinder `isFreeIn` t -> pure $ RType tz r
-              -- We switch to an inner let if substituting under it would cause capture
-              Nothing
-                | TLet _ w s _ <- target tz
-                , [_, bz] <- typeChildren tz
-                , v /= w
-                , w `isFreeIn` t ->
-                    goSubstTy w s =<< hoistAccum bz
-              -- We should not go under 'v' binders, but otherwise substitute in each child
-              _ ->
-                let substChild c = do
-                      guard $
-                        S.notMember (unLocalName v) $
-                          S.map unLocalName $
-                            getBoundHereTy (target tz) (Just $ target c)
-                      goSubstTy v t c
-                 in msum $ map (substChild <=< hoistAccum) (typeChildren tz)
 
 children' :: IsZipper za a => za -> [za]
 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)
     let d' = case target ez of
           App _ f _ | f == target c -> Syn
           APP _ f _ | f == target c -> Syn
@@ -310,26 +185,10 @@ exprChildren (d, ez) =
             | e == target c -> Chk
             | otherwise -> d
           _ -> Chk
-    addBinds ez bs
-    pure (d', c)
-
-typeChildren :: TypeZ -> [Accum Cxt TypeZ]
-typeChildren tz =
-  children' tz <&> \c -> do
-    let bs = getBoundHereTy' (target tz) (Just $ target c)
-    addBinds tz $ bimap unLocalName LetTyBind <$> bs
-    pure c
+    (d', c)
 
-addBinds :: HasID i => i -> [Either Name LetBinding] -> Accum Cxt ()
-addBinds i' bs = do
-  let i = getID i'
-  cxt <- look
-  add $
-    Cxt $
-      M.fromList $
-        bs <&> \case
-          Left n -> (n, (Nothing, i, cxt))
-          Right l -> (letBindingName l, (Just l, i, cxt))
+typeChildren :: TypeZ -> [TypeZ]
+typeChildren = children'
 
-singletonCxt :: HasID i => i -> LetBinding -> Cxt
-singletonCxt i l = addBinds i [Right l] `execAccum` mempty
+singletonCxt :: LetBinding -> Cxt
+singletonCxt l = Cxt [l]
diff --git a/primer/src/Primer/Eval/Push.hs b/primer/src/Primer/Eval/Push.hs
new file mode 100644
index 000000000..ec4d46d34
--- /dev/null
+++ b/primer/src/Primer/Eval/Push.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE DuplicateRecordFields #-}
+
+module Primer.Eval.Push (PushLetDetail (..)) where
+
+import Foreword
+
+import Primer.Core.Meta (ID)
+import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
+import Primer.Name (Name)
+
+-- | Detailed information about pushing a group of 'let's down the tree
+-- This each can be any of: a term-level non-recursive let, a
+-- term-level recursive let, a term-level let binding a type
+-- or a type-level let.
+-- If term-level: t ~ Expr; if type-level: t ~ Type
+data PushLetDetail t = PushLetDetail
+  { before :: t
+  -- ^ the expression before reduction
+  , after :: t
+  -- ^ the resulting expression after reduction
+  , letIDs :: [ID]
+  -- ^ the 'ID' of each original let
+  , letBindingNames :: [Name]
+  -- ^ the names of the variables bound by the @let@s
+  , intoID :: ID
+  -- ^ the 'ID' of the term we push into
+  }
+  deriving stock (Eq, Show, Read, Generic)
+  deriving (FromJSON, ToJSON) via PrimerJSON (PushLetDetail t)
diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs
index 769902afe..5216dd972 100644
--- a/primer/src/Primer/Eval/Redex.hs
+++ b/primer/src/Primer/Eval/Redex.hs
@@ -1,52 +1,59 @@
 {-# LANGUAGE DuplicateRecordFields #-}
 {-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE NoFieldSelectors #-}
+{-# LANGUAGE OverloadedRecordDot #-}
 
 module Primer.Eval.Redex (
   Redex (..),
   viewRedex,
+  ViewRedexOptions (..),
+  RunRedexOptions (..),
   runRedex,
   RedexType (..),
   viewRedexType,
   runRedexTy,
   Dir (Syn, Chk),
   Cxt (Cxt),
+  cxtAddLet,
   _freeVarsLetBinding,
   EvalLog (..),
   MonadEval,
   -- Exported for testing
-  getNonCapturedLocal,
+  lookupEnclosingLet,
 ) where
 
 import Foreword
 
 import Control.Monad.Fresh (MonadFresh)
 import Control.Monad.Log (MonadLog, WithSeverity)
-import Control.Monad.Trans.Maybe (MaybeT (runMaybeT))
+import Control.Monad.Trans.Maybe (MaybeT)
+import Data.Bitraversable (bitraverse)
 import Data.Data (Data)
+import Data.Generics.Uniplate.Data (children, descendM)
 import Data.List (zip3)
+import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map qualified as M
 import Data.Set qualified as S
 import Data.Set.Optics (setOf)
-import Data.Tuple.Extra (snd3)
 import GHC.Err (error)
 import Optics (
   AffineFold,
   Fold,
   afolding,
-  allOf,
-  elemOf,
+  folded,
   getting,
   ifiltered,
   isnd,
   notElemOf,
   summing,
   to,
+  traverseOf,
   (%),
   (<%),
+  _Just,
   _1,
   _2,
-  _Just,
  )
 import Primer.Core (
   Bind,
@@ -93,6 +100,7 @@ import Primer.Core (
   bindName,
   caseBranchName,
   getID,
+  typesInExpr,
  )
 import Primer.Core.DSL (ann, letType, let_, letrec, lvar, tlet, tvar)
 import Primer.Core.Transform (decomposeTAppCon)
@@ -132,6 +140,8 @@ import Primer.Eval.Detail (
     LetRemoval,
     LocalTypeVarInline,
     LocalVarInline,
+    PushLetDown,
+    PushLetDownTy,
     RemoveAnn,
     TBindRename,
     TLetRemoval
@@ -139,9 +149,8 @@ import Primer.Eval.Detail (
   GlobalVarInlineDetail (GlobalVarInlineDetail),
   LetRemovalDetail (LetRemovalDetail),
   LocalVarInlineDetail (LocalVarInlineDetail),
+  PushLetDetail (PushLetDetail),
   RemoveAnnDetail (RemoveAnnDetail),
-  findFreeOccurrencesExpr,
-  findFreeOccurrencesType,
  )
 import Primer.Eval.Detail qualified
 import Primer.Eval.Prim (tryPrimFun)
@@ -168,8 +177,19 @@ import Primer.Zipper (
 import Primer.Zipper.Type (
   LetTypeBinding,
   LetTypeBinding' (LetTypeBind),
+  getBoundHereDnTy,
+  letTypeBindingName,
  )
 
+data ViewRedexOptions = ViewRedexOptions
+  { pushMulti :: Bool
+  , aggressiveElision :: Bool
+  }
+
+data RunRedexOptions = RunRedexOptions
+  { pushAndElide :: Bool
+  }
+
 data EvalLog
   = -- | Found something that may have been a case redex,
     -- but the scrutinee's head is an out-of-scope constructor.
@@ -213,8 +233,8 @@ data Redex
       , def :: ASTDef
       -- ^ What is its definition
       }
-  | -- x  ~>  e   where we are inside the scope of a  let x = e in ...
-    InlineLet
+  | -- let x = e in x  ~>  e
+    InlineLet -- TODO/REVIEW: don't know if I want to change this def for push-down-lets, as only inline an immediate usage
       { var :: LVarName
       -- ^ What variable are we inlining
       , expr :: Expr
@@ -224,8 +244,8 @@ data Redex
       , varID :: ID
       -- ^ Where was the occurrence (used for details)
       }
-  | -- x  ~>  letrec x:T=t in t:T   where we are inside the scope of a  letrec x : T = t in ...
-    InlineLetrec
+  | -- letrec x = t : T in x  ~>  letrec x = t : T in t : T
+    InlineLetrec -- TODO/REVIEW: don't know if I want to change this def for push-down-lets, as only inline an immediate usage
       { var :: LVarName
       -- ^ What variable are we inlining
       , expr :: Expr
@@ -237,12 +257,33 @@ data Redex
       , varID :: ID
       -- ^ Where was the occurrence (used for details)
       }
+  | -- let x = e in f s  ~>  (let x = e in f) (let x = e in s)  etc
+    -- [for any non-leaf @f s@ which neither binds @x@ (else we should elide)
+    --  nor any free variable of @e@ (to avoid capture)]
+    -- [We actually do this rule for a whole sequence of let bindings at once]
+    -- [If we push into an annotation, we drop term variables:  let x = e in (t : T)  ~> (let x = e in t) : T]
+    -- [We actually drop all "pointless" variables:
+    --   let x = e in f s  ~>  (let x = e in f) (let x = e in s)    if @x@ is free in @f@, and free in @s@
+    --   let x = e in f s  ~>  f (let x = e in s)                   if @x@ is not free in @f@, but free in @s@
+    --   let x = e in f s  ~>  (let x = e in f) s                   if @x@ is free in @f@, but not free in @s@
+    --   let x = e in f s  ~>  f s                                  if @x@ is not free in @f@, and not free in @s@
+    PushLet
+      { bindings :: NonEmpty (ID, LetBinding)
+      -- ^ The bindings we push
+      , expr :: Expr
+      -- ^ The expression we are pushing into, i.e. the original body of the above bindings
+      , orig :: Expr
+      -- ^ the original expression (used for details)
+      }
   | -- let(rec/type) x = e in t  ~>  t  if x does not appear in t
+    -- [We actually elide from a whole sequence of let bindings at once]
     ElideLet
-      { letBinding :: LetBinding
-      -- ^ Original binding
+      { letBindingsKeep :: [(ExprMeta, LetBinding)]
+      -- ^ Subset of bindings to keep
+      , letBindingsDrop :: NonEmpty (ID, LetBinding)
+      -- ^ Subset of bindings to drop
       , body :: Expr
-      -- ^ Body, in which the bound var does not occur
+      -- ^ Body, in which the elided variables do not occur
       , orig :: Expr
       -- ^ the original let (used for details)
       }
@@ -371,31 +412,6 @@ data Redex
       , orig :: Expr
       -- ^ The original redex (used for details)
       }
-  | -- let x = f x in g x x  ~>  let y = f x in let x = y in g x x
-    -- Note that we cannot substitute the let in the initial term, since
-    -- we only substitute one occurence at a time, and the 'let' would capture the 'x'
-    -- in the expansion if we did a substitution.
-    RenameSelfLet
-      { var :: LVarName
-      -- ^ The bound variable
-      , rhs :: Expr
-      -- ^ The local definition of @var@
-      , body :: Expr
-      -- ^ The body of the @let@, in which @var@ can occur free
-      , orig :: Expr
-      -- ^ The original redex (used for details)
-      }
-  | -- As RenameSelfLet, but for LetType. (Note that it is unnecessary for letrec.)
-    RenameSelfLetType
-      { tyvar :: TyVarName
-      -- ^ The bound variable
-      , trhs :: Type
-      -- ^ The local definition of @var@
-      , body :: Expr
-      -- ^ The body of the @let_type@, in which @var@ can occur free
-      , orig :: Expr
-      -- ^ The original redex (used for details)
-      }
   | ApplyPrimFun
       { result :: forall m. MonadFresh ID m => m Expr
       -- ^ The result of the applied primitive function
@@ -408,37 +424,40 @@ data Redex
       }
 
 data RedexType
-  = InlineLetInType
+  = -- let a = t in a  ~>  t
+    InlineLetInType
       { var :: TyVarName
       -- ^ What variable are we inlining (used for finding normal-order redex)
       , ty :: Type
       -- ^ What is its definition (used for reduction)
       , letID :: ID
       -- ^ Where was the binding (used for details)
+      -- TODO/REVIEW: it seems a bit silly recording both these IDs, since they'll be right next to each other...
       , varID :: ID
       -- ^ Where was the occurrence (used for details)
       }
+  | -- let a = s in t1 t2  ~>  (let a = s in t1) (let a = s in t2)  etc
+    -- (see notes on the analogous rule for Redex)
+    PushLetType
+      { bindings :: NonEmpty (ID, LetTypeBinding)
+      -- ^ what bindings we are pushing (IDs used for details, bindings used for reduction)
+      , intoTy :: Type
+      -- ^ the type they are being pushed into (used for reduction)
+      , origTy :: Type
+      -- ^ what was the original ("let-outside") (used for details)
+      }
   | -- let a = s in t  ~>  t  if a does not appear in t
+    -- [We actually elide from a whole sequence of let bindings at once]
     ElideLetInType
-      { letBinding :: LetTypeBinding
-      -- ^ original binding (name is used for finding normal-order redex; used for details)
+      { letBindingsKeep :: [(TypeMeta, LetTypeBinding)]
+      -- ^ Subset of bindings to keep
+      , letBindingsDrop :: NonEmpty (ID, LetTypeBinding)
+      -- ^ Subset of bindings to drop
       , body :: Type
-      -- ^ Body, in which the bound var does not occur (used for reduction)
+      -- ^ Body, in which the elided variables do not occur
       , orig :: Type
       -- ^ the original let (used for details)
       }
-  | -- let a = s a in t a a  ~>  let b = s a in let a = b in t a a
-    -- Note that we cannot substitute the let in the initial term, since
-    -- we only substitute one occurence at a time, and the 'let' would capture the 'a'
-    -- in the expansion if we did a substitution.
-    RenameSelfLetInType
-      { letBinding :: LetTypeBinding
-      -- ^ binding (name is used for finding normal-order redex; used for reduction)
-      , body :: Type
-      -- ^ body, in which th e bound var may occur (used for reduction)
-      , orig :: Type
-      -- ^  the original let (used for details)
-      }
   | -- ∀a:k.t  ~>  ∀b:k. let a = b in t  for fresh b, avoiding the given set
     RenameForall
       { meta :: TypeMeta
@@ -480,9 +499,6 @@ _freeVarsTy' = getting _freeVarsTy % _2 % to unLocalName
 _freeVarsLetBinding :: Fold LetBinding Name
 _freeVarsLetBinding =
   (_LetBind % _2 % _freeVars')
-    -- Since letrec bound variables expand with a local letrec,
-    -- we don't consider the recursively-bound variable free
-    -- (since it will not be in the inlining)
     `summing` ( _LetrecBind
                   <% ( to (\(a, b, c) -> (a, (b, c)))
                         % isnd
@@ -490,7 +506,10 @@ _freeVarsLetBinding =
                         & ifiltered ((/=) . unLocalName)
                      )
               )
-    `summing` (_LetTyBind % _LetTypeBind % _2 % _freeVarsTy')
+    `summing` (_LetTyBind % _freeVarsLetTypeBinding % to unLocalName)
+
+_freeVarsLetTypeBinding :: Fold LetTypeBinding TyVarName
+_freeVarsLetTypeBinding = _LetTypeBind % _2 % getting _freeVarsTy % _2
 
 data Dir = Syn | Chk
   deriving stock (Eq, Show, Read, Generic)
@@ -608,24 +627,14 @@ 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}
 
--- 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
-newtype Cxt = Cxt (M.Map Name (Maybe LetBinding, ID, Cxt))
-  -- We want right-biased mappend, as we will use this with 'Accum'
-  -- and want later 'add's to overwrite earlier (more-global) context entries
-  deriving (Semigroup, Monoid) via Dual (M.Map Name (Maybe LetBinding, ID, Cxt))
+-- We record each directly-enclosing let binding
+-- By "directly enclosing" we mean "those which may be pushed into this term"
+-- NB: we do not care about ordering
+newtype Cxt = Cxt [LetBinding]
+  deriving newtype (Semigroup, Monoid)
 
-lookup :: Name -> Cxt -> Maybe (Maybe LetBinding, ID, Cxt)
-lookup n (Cxt cxt) = M.lookup n cxt
-
--- We only care about LLetType if we are looking up tyvars,
--- as we assume that the input is well-typed, and the only things
--- that tyvars can refer to are lettype, or foralls
-lookupTy :: TyVarName -> Cxt -> Maybe (Maybe LetTypeBinding, ID, Cxt)
-lookupTy n c = case lookup (unLocalName n) c of
-  Just (Just (LetTyBind b), i, c') -> Just (Just b, i, c')
-  _ -> Nothing
+cxtAddLet :: LetBinding -> Cxt -> Cxt
+cxtAddLet l (Cxt c) = Cxt $ l : c
 
 -- This notices all redexes
 -- Note that if a term is not a redex, but stuck on some sub-term,
@@ -634,66 +643,110 @@ lookupTy n c = case lookup (unLocalName n) c of
 -- - stuck on its left-most child
 -- - stuck on the type annotation on its left-most child
 -- - stuck on expression under the type annotation in its left-most child
+--
+--
+-- TODO/REVIEW: we use this to choose order, by going into type annotations first.
+-- However, consider
+--    (Λa.Λb. t : ∀a.∀b. T) @x @y
+-- which reduces to
+--    (let a = x in Λb. t : let a=x in ∀b. T) @y
+-- one step in type and one in term would give
+--    (Λb. let a = x in t : ∀b. let a=x in T) @y
+-- which would then reduce the top application:
+--    (let b = y in let a = x in t : let b = y in let a=x in T) @y
+-- rather than forcing us to push the substitution through the annotation first.
+-- This way would be more efficient (with grouped lets): we only have to push one large
+-- substitution through T (and t) once, rather than two small ones.
+--
+-- IDEAS: either have an annotation "why stuck", or just say "do let-push in each (ty&tm) child first, before anything else)
 viewRedex ::
   (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
+  ViewRedexOptions ->
   TypeDefMap ->
   DefMap ->
   Dir ->
   Expr ->
   ReaderT Cxt (MaybeT m) Redex
-viewRedex tydefs globals dir = \case
+viewRedex opts tydefs globals dir = \case
   orig@(Var _ (GlobalVarRef gvar))
     | Just (DefAST def) <- gvar `M.lookup` globals ->
         pure $
           InlineGlobal{gvar, def, orig}
-  Var m (LocalVarRef var) -> do
-    let varID = getID m
-    runMaybeT (getNonCapturedLocal var) >>= \x -> do
-      case x of
-        Just (letID, LetBind _ expr) -> pure $ InlineLet{var, expr, letID, varID}
-        Just (letID, LetrecBind _ expr ty) -> pure $ InlineLetrec{var, expr, ty, letID, varID}
-        _ -> mzero
-  orig@(Let _ var rhs body)
+  Let mLet var rhs (Var mVar (LocalVarRef var'))
+    | var == var'
+    -> pure $
+          InlineLet
+            { var
+            , expr = rhs
+            , letID = getID mLet
+            , varID = getID mVar
+            }
+  Letrec mLet var rhs ty (Var mVar (LocalVarRef var'))
+    | var == var'
+    -> pure $
+          InlineLetrec
+            { var
+            , expr = rhs
+            , ty
+            , letID = getID mLet
+            , varID = getID mVar
+            }
+  orig@(viewLets -> Just (letBinding1,expr',letBindings,body))
+    | not opts.pushMulti
+    , not $ isLeaf expr'
+    , null letBindings
+    , n <- letBindingName $ snd letBinding1
+    , not opts.aggressiveElision || n `S.member` freeVars expr'
+    , S.disjoint (getBoundHereDn expr') (setOf (_2 % (_freeVarsLetBinding `summing` to letBindingName)) letBinding1)
+    -> pure $
+        PushLet
+          { bindings = pure $ first getID letBinding1
+          , expr = expr'
+          , orig
+          }
+    | opts.pushMulti
+    , not $ isLeaf body
+    , (_, unused) <- partitionLets (letBinding1 : letBindings) body
+    , not opts.aggressiveElision || null unused
+    , S.disjoint (getBoundHereDn body) (setOf (folded % _2 % (_freeVarsLetBinding `summing` to letBindingName)) $ letBinding1 : letBindings)
+    -> pure $
+        PushLet
+          { bindings = first getID <$> letBinding1 :| letBindings
+          , expr = body
+          , orig
+          }
     -- NB: we will recompute the freeVars set a lot (especially when doing EvalFull iterations)
     -- This could be optimised in the future. See
     -- https://github.com/hackworthltd/primer/issues/733
-    | unLocalName var `S.notMember` freeVars body ->
-        pure $
-          ElideLet
-            { letBinding = LetBind var rhs
-            , body
-            , orig
-            }
-    | unLocalName var `S.member` freeVars rhs -> pure $ RenameSelfLet{var, rhs, body, orig}
-    | otherwise -> mzero
-  orig@(LetType _ var trhs body)
-    | unLocalName var `S.notMember` freeVars body ->
-        pure $
-          ElideLet
-            { letBinding = LetTyBind $ LetTypeBind var trhs
-            , body
-            , orig
-            }
-    | var `S.member` freeVarsTy trhs -> pure $ RenameSelfLetType{tyvar = var, trhs, body, orig}
-    | otherwise -> mzero
-  orig@(Letrec _ v e1 t body)
-    | unLocalName v `S.notMember` freeVars body ->
-        pure $
-          ElideLet
-            { letBinding = LetrecBind v e1 t
-            , body
-            , orig
-            }
-    | otherwise -> mzero
+    | not opts.pushMulti
+    , letBindingName (snd letBinding1) `S.notMember` freeVars expr'
+    , opts.aggressiveElision || isLeaf expr'
+    -> pure $
+        ElideLet
+          { letBindingsDrop = pure $ first getID letBinding1
+          , letBindingsKeep = []
+          , body = expr'
+          , orig
+          }
+    | opts.pushMulti
+    , (letBindingsKeep, nonEmpty -> Just letBindingsDrop) <- partitionLets (letBinding1 : letBindings) body
+    , opts.aggressiveElision || isLeaf body
+    -> pure $
+        ElideLet
+          { letBindingsDrop = first getID <$> letBindingsDrop
+          , letBindingsKeep
+          , body
+          , orig
+          }
   l@(Lam meta var body) -> do
-    fvcxt <- fvCxt $ freeVars l
-    if unLocalName var `S.member` fvcxt
-      then pure $ RenameBindingsLam{var, meta, body, avoid = fvcxt, orig = l}
+    avoid <- cxtToAvoid
+    if unLocalName var `S.member` avoid
+      then pure $ RenameBindingsLam{var, meta, body, avoid, orig = l}
       else mzero
   l@(LAM meta v body) -> do
-    fvcxt <- fvCxt $ freeVars l
-    if unLocalName v `S.member` fvcxt
-      then pure $ RenameBindingsLAM{tyvar = v, meta, body, avoid = fvcxt, orig = l}
+    avoid <- cxtToAvoid
+    if unLocalName v `S.member` avoid
+      then pure $ RenameBindingsLAM{tyvar = v, meta, body, avoid, orig = l}
       else mzero
   orig@(App _ (Ann _ (Lam m var body) (TFun _ srcTy tgtTy)) app) ->
     pure $
@@ -726,46 +779,131 @@ viewRedex tydefs globals dir = \case
         }
   APP{} -> mzero
   e@(Case meta scrutinee branches fallbackBranch) -> do
-    fvcxt <- fvCxt $ freeVars e
+    avoid <- cxtToAvoid
     -- TODO: we arbitrarily decide that renaming takes priority over reducing the case
     -- This is good for evalfull, but bad for interactive use.
     -- Maybe we want to offer both. See
     -- https://github.com/hackworthltd/primer/issues/734
-    if getBoundHereDn e `S.disjoint` fvcxt
+    if getBoundHereDn e `S.disjoint` avoid
       then lift $ viewCaseRedex tydefs e
-      else pure $ RenameBindingsCase{meta, scrutinee, branches, fallbackBranch, avoid = fvcxt, orig = e}
+      else pure $ RenameBindingsCase{meta, scrutinee, branches, fallbackBranch, avoid, orig = e}
   orig@(Ann _ expr ty) | Chk <- dir, concreteTy ty -> pure $ Upsilon{expr, ann = ty, orig}
   _ -> mzero
+ where
+   isLeaf = null . children
 
-viewRedexType :: Type -> Reader Cxt (Maybe RedexType)
-viewRedexType = \case
-  TVar m var ->
-    runMaybeT (getNonCapturedLocal var) <&> \case
-      Just (letID, LetTyBind (LetTypeBind _ ty)) -> pure $ InlineLetInType{var, ty, letID, varID = getID m}
+-- Decompose @let a = s in let b0 = t0 in ... let bn = tn in e@
+-- into @(LetBind a s, let b0=t0 in ... e, [LetBind b0 t0, ..., LetBind bn tn], e)@
+-- I.e. a combination of two views: first let & all lets.
+-- Note that this decomposes lets of all flavors.
+viewLets :: Expr -> Maybe ((ExprMeta, LetBinding), Expr, [(ExprMeta, LetBinding)], Expr)
+viewLets e = do
+    (l1,e') <- viewLet e
+    let (ls,e'') = viewLets' e'
+    pure (l1,e',ls,e'')
+ where
+  -- | Decompose multiple @let@s (of varying flavors) around a
+  -- non-let expression.
+  viewLets' :: Expr -> ([(ExprMeta, LetBinding)], Expr)
+  viewLets' e = case viewLet e of
+    Nothing -> ([],e)
+    Just (l,e') -> first (l:) $ viewLets' e'
+  -- | Decompose one @let@ (of any flavor)
+  viewLet :: Expr -> Maybe ((ExprMeta, LetBinding), Expr)
+  viewLet = \case
+     Let m v e b -> Just ((m,LetBind v e),b)
+     Letrec m v t ty b -> Just ((m,LetrecBind v t ty),b)
+     LetType m a ty b -> Just ((m, LetTyBind (LetTypeBind a ty)),b)
+     _ -> Nothing
+
+-- TODO: rename?
+unviewLets :: [(ExprMeta, LetBinding)] -> Expr -> Expr
+unviewLets ls e = foldr
+        (\(m,l) e' -> case l of
+                LetBind v t -> Let m v t e'
+                LetrecBind v t ty -> Letrec m v t ty e'
+                LetTyBind (LetTypeBind v ty) -> LetType m v ty e'
+            )
+            e ls
+
+viewLetsTy :: Type -> Maybe ((TypeMeta, LetTypeBinding), Type, [(TypeMeta, LetTypeBinding)], Type)
+viewLetsTy ty = do
+    (l1,ty') <- viewOne ty
+    let (ls, ty'') = viewLets' ty'
+    pure (l1, ty', ls, ty'')
+  where
+    viewOne = \case
+      TLet m a t b -> Just ((m,LetTypeBind a t),b)
       _ -> Nothing
-  orig@(TLet _ v s body)
-    -- NB: we will recompute the freeVars set a lot (especially when doing EvalFull iterations)
-    -- This could be optimised in the future. See
-    -- https://github.com/hackworthltd/primer/issues/733
-    | notElemOf (getting _freeVarsTy % _2) v body ->
-        purer $
-          ElideLetInType
-            { letBinding = LetTypeBind v s
-            , body
-            , orig
-            }
-    | elemOf (getting _freeVarsTy % _2) v s ->
+    viewLets' t = case viewOne t of
+      Nothing -> ([],t)
+      Just (l,t') -> first (l:) $ viewLets' t'
+
+-- TODO: rename?
+unviewLetsTy :: [(TypeMeta, LetTypeBinding)] -> Type -> Type
+unviewLetsTy ls t = foldr
+        (\(m,LetTypeBind v ty) t' -> TLet m v ty t' )
+        t ls
+
+
+viewRedexType :: ViewRedexOptions -> Type -> Reader Cxt (Maybe RedexType)
+viewRedexType opts = \case
+  TLet mLet v s (TVar mVar var)
+    | v == var ->
         purer $
-          RenameSelfLetInType
-            { letBinding = LetTypeBind v s
-            , body
-            , orig
+          InlineLetInType
+            { var
+            , ty = s
+            , letID = getID mLet
+            , varID = getID mVar
             }
-    | otherwise -> pure Nothing
+  orig@(viewLetsTy -> Just (letBinding1,ty',letBindings,body))
+    | not opts.pushMulti
+    , not $ isLeaf ty'
+    , null letBindings
+    , not opts.aggressiveElision || letTypeBindingName' (snd letBinding1) `S.member` freeVarsTy ty'
+    , S.disjoint (getBoundHereDnTy ty') (setOf (_2 % (_freeVarsLetTypeBinding `summing` to letTypeBindingName')) letBinding1)
+    -> purer $
+        PushLetType
+          { bindings = pure $ first getID letBinding1
+          , intoTy = ty'
+          , origTy = orig
+          }
+    | opts.pushMulti
+    , not $ isLeaf body
+    , (_, unused) <- partitionLetsTy (letBinding1 : letBindings) body
+    , not opts.aggressiveElision || null unused
+    , S.disjoint (getBoundHereDnTy body) (setOf (folded % _2 % (_freeVarsLetTypeBinding `summing` to letTypeBindingName')) (letBinding1 : letBindings))
+    -> purer $
+        PushLetType
+          { bindings = first getID <$> letBinding1 :| letBindings
+          , intoTy = body
+          , origTy = orig
+          }
+    | not opts.pushMulti
+    , letTypeBindingName' (snd letBinding1) `S.notMember` freeVarsTy ty'
+    , opts.aggressiveElision || isLeaf ty'
+    -> purer $
+        ElideLetInType
+          { letBindingsDrop = pure $ first getID letBinding1
+          , letBindingsKeep = []
+          , body = ty'
+          , orig
+          }
+    | opts.pushMulti
+    , (letBindingsKeep, nonEmpty -> Just letBindingsDrop) <- partitionLetsTy (letBinding1 : letBindings) body
+    , opts.aggressiveElision || isLeaf body
+    -> purer $
+        ElideLetInType
+          { letBindingsDrop = first getID <$> letBindingsDrop
+          , letBindingsKeep
+          , body
+          , orig
+          }
   orig@(TForall meta origBinder kind body) -> do
-    fvcxt <- fvCxtTy $ freeVarsTy orig
+    avoid <- cxtToAvoidTy
     pure $
-      if origBinder `S.member` fvcxt
+      if origBinder `S.member` avoid
         then
           pure $
             -- If anything we may substitute would cause capture, we should rename this binder
@@ -774,59 +912,50 @@ viewRedexType = \case
               , origBinder
               , kind
               , body
-              , avoid = fvcxt
+              , avoid
               , orig
               }
         else Nothing
   _ -> pure Nothing
+ where
+   isLeaf = null . children
+   letTypeBindingName' (LetTypeBind n _) = n
 
--- Get the let-bound definition of this variable, if some such exists
--- and is substitutible in the current context. (We also return the
--- id of the binding site.)
-getNonCapturedLocal :: MonadReader Cxt m => LocalName k -> MaybeT m (ID, LetBinding)
-getNonCapturedLocal v = do
-  def <- asks (lookup $ unLocalName v)
-  curCxt <- ask
-  hoistMaybe $ do
-    (def', origID, origCxt) <- def
-    def'' <- def'
-    let uncaptured x = ((==) `on` fmap snd3 . lookup x) origCxt curCxt
-    if allOf _freeVarsLetBinding uncaptured def''
-      then Just (origID, def'')
-      else Nothing
+lookupEnclosingLet :: Name -> Cxt -> Maybe LetBinding
+lookupEnclosingLet n (Cxt cxt) = find ((== n) . letBindingName) cxt
 
--- What are the FVs of the RHS of these bindings?
-fvCxt :: MonadReader Cxt m => S.Set Name -> m (S.Set Name)
-fvCxt vs = do
-  cxt <- ask
-  pure $ foldMap' (setOf (_Just % _1 % _Just % _freeVarsLetBinding) . flip lookup cxt) vs
+-- We may want to push some let bindings (the Cxt) under a
+-- binder; what variable names must the binder avoid for this to be valid?
+cxtToAvoid :: MonadReader Cxt m => m (S.Set Name)
+cxtToAvoid = do
+  Cxt cxt <- ask
+  pure $ foldMap' (setOf (to letBindingName `summing` _freeVarsLetBinding)) cxt
 
-fvCxtTy :: S.Set TyVarName -> Reader Cxt (S.Set TyVarName)
-fvCxtTy vs = do
-  cxt <- ask
-  pure $ foldMap' (setOf (_Just % _1 % _Just % _LetTypeBind % _2 % getting _freeVarsTy % _2) . flip lookupTy cxt) vs
+cxtToAvoidTy :: MonadReader Cxt m => m (S.Set TyVarName)
+cxtToAvoidTy = do
+  Cxt cxt <- ask
+  pure $ foldMap' (setOf (_LetTyBind % _LetTypeBind % (_1 `summing` _2 % getting _freeVarsTy % _2))) cxt
 
 -- TODO: deal with metadata. https://github.com/hackworthltd/primer/issues/6
-runRedex :: forall l m. MonadEval l m => Redex -> m (Expr, EvalDetail)
-runRedex = \case
+runRedex :: forall l m. MonadEval l m => RunRedexOptions -> Redex -> m (Expr, EvalDetail)
+runRedex opts = \case
   InlineGlobal{def, orig} -> do
     after <- ann (regenerateExprIDs $ astDefExpr def) (regenerateTypeIDs $ astDefType def)
     let details = GlobalVarInlineDetail{def, var = orig, after}
     pure (after, GlobalVarInline details)
   InlineLet{var, expr, letID, varID} -> do
-    expr' <- regenerateExprIDs expr
     let details =
           LocalVarInlineDetail
             { letID
             , varID
             , valueID = getID expr
             , bindingName = var
-            , replacementID = getID expr'
+            , replacementID = getID expr
             , isTypeVar = False
             }
-    pure (expr', LocalVarInline details)
+    pure (expr, LocalVarInline details)
   InlineLetrec{var, expr, ty, letID, varID} -> do
-    expr' <- letrec var (regenerateExprIDs expr) (regenerateTypeIDs ty) $ ann (regenerateExprIDs expr) (regenerateTypeIDs ty)
+    expr' <- letrec var (pure expr) (pure ty) $ ann (regenerateExprIDs expr) (regenerateTypeIDs ty)
     let details =
           LocalVarInlineDetail
             { letID
@@ -837,19 +966,30 @@ runRedex = \case
             , isTypeVar = False
             }
     pure (expr', LocalVarInline details)
-  -- let(rec/type) x = e in t  ~>  t  if e does not appear in t
-  ElideLet{body, letBinding, orig} -> do
+  PushLet{bindings, expr, orig} -> do
+    let binds = snd <$> bindings
+    expr' <- descendM (addLets opts binds) =<< traverseOf typesInExpr (addTLets opts binds) expr
     let details =
+          PushLetDetail
+            { before = orig
+            , after = expr'
+            , letIDs = toList $ fst <$> bindings
+            , letBindingNames = toList $ letBindingName <$> binds
+            , intoID = getID expr
+            }
+    pure (expr', PushLetDown details)
+  -- let(rec/type) x = e in t  ~>  t  if e does not appear in t
+  ElideLet{body, letBindingsKeep, letBindingsDrop, orig} -> do
+    let expr = unviewLets letBindingsKeep body
+        details =
           LetRemovalDetail
             { before = orig
-            , after = body
-            , bindingName = letBindingName letBinding
-            , letID = getID orig
+            , after = expr
+            , bindingNames = letBindingName . snd <$> letBindingsDrop
+            , letIDs = fst <$> letBindingsDrop
             , bodyID = getID body
             }
-
-    pure (body, LetRemoval details)
-
+    pure (expr, LetRemoval details)
   -- (λx.t : S -> T) s  ~>  let x = s:S in t : T
   Beta{var, body, srcTy, tgtTy, app, orig, lamID} -> do
     expr' <- let_ var (pure app `ann` pure srcTy) (pure body) `ann` pure tgtTy
@@ -1037,42 +1177,6 @@ runRedex = \case
     -- We should replace this with a proper exception. See:
     -- https://github.com/hackworthltd/primer/issues/148
     | otherwise -> error "Internal Error: RenameBindingsCase found no applicable branches"
-  -- let x = f x in g x x  ~>  let y = f x in let x = y in g x x
-  RenameSelfLet{var, rhs, body, orig} -> do
-    y <- freshLocalName' (freeVars rhs <> freeVars body)
-    rl <- let_ var (lvar y) $ pure body
-    expr' <- let_ y (pure rhs) $ pure rl
-    let details =
-          BindRenameDetail
-            { before = orig
-            , after = expr'
-            , bindingNamesOld = [unLocalName var]
-            , bindingNamesNew = [unLocalName y]
-            , bindersOld = [getID orig]
-            , bindersNew = [getID expr']
-            , bindingOccurrences = findFreeOccurrencesExpr var rhs
-            , renamingLets = [getID rl]
-            , bodyID = getID body
-            }
-    pure (expr', BindRename details)
-  -- As RenameSelfLet, but for LetType
-  RenameSelfLetType{tyvar, trhs, body, orig} -> do
-    b <- freshLocalName' (S.map unLocalName (freeVarsTy trhs) <> freeVars body)
-    rl <- letType tyvar (tvar b) $ pure body
-    expr' <- letType b (pure trhs) $ pure rl
-    let details =
-          BindRenameDetail
-            { before = orig
-            , after = expr'
-            , bindingNamesOld = [unLocalName tyvar]
-            , bindingNamesNew = [unLocalName b]
-            , bindersOld = [getID orig]
-            , bindersNew = [getID expr']
-            , bindingOccurrences = findFreeOccurrencesType tyvar trhs
-            , renamingLets = [getID rl]
-            , bodyID = getID body
-            }
-    pure (expr', BindRename details)
   ApplyPrimFun{result, primFun, orig, args} -> do
     expr' <- result
     let details =
@@ -1084,50 +1188,103 @@ runRedex = \case
             }
     pure (expr', Primer.Eval.Detail.ApplyPrimFun details)
 
-runRedexTy :: MonadEval l m => RedexType -> m (Type, EvalDetail)
-runRedexTy (InlineLetInType{ty, letID, varID, var}) = do
-  ty' <- regenerateTypeIDs ty
+addLets :: MonadFresh ID m => RunRedexOptions -> NonEmpty LetBinding -> Expr -> m Expr
+addLets opts ls expr = foldrM addLet expr $ if opts.pushAndElide then filterLets ls expr else toList ls
+  where
+    addLet :: MonadFresh ID m => LetBinding -> Expr -> m Expr
+    addLet (LetBind v e) b = let_ v (regenerateExprIDs e) (pure b)
+    addLet (LetrecBind v t ty) b = letrec v (regenerateExprIDs t) (regenerateTypeIDs ty) (pure b)
+    addLet (LetTyBind (LetTypeBind v ty)) b = letType v (regenerateTypeIDs ty) (pure b)
+
+addTLets :: MonadFresh ID m => RunRedexOptions -> NonEmpty LetBinding -> Type -> m Type
+addTLets opts ls t = foldrM addTLet t $ if opts.pushAndElide then filterLetsTy ls t else toList ls
+  where
+    addTLet :: MonadFresh ID m => LetBinding -> Type -> m Type
+    -- drop let bindings of term variables
+    addTLet (LetTyBind (LetTypeBind v ty)) b = tlet v (regenerateTypeIDs ty) (pure b)
+    addTLet _ b = pure b
+
+filterLets :: NonEmpty LetBinding -> Expr -> [LetBinding]
+filterLets ls e = filterLets' (toList ls) (freeVars e)
+
+filterLetsTy :: NonEmpty LetBinding -> Type -> [LetBinding]
+filterLetsTy ls t = filterLets' (toList ls) (S.map unLocalName $ freeVarsTy t)
+
+filterLets' :: [LetBinding] -> Set Name -> [LetBinding]
+filterLets' ls fvs =
+  fst $
+    foldr
+      ( \l (ls', fvs') ->
+          let ln = letBindingName l
+           in if ln `S.member` fvs'
+                then (l : ls', S.delete ln fvs' `S.union` setOf _freeVarsLetBinding l)
+                else (ls', fvs')
+      )
+      ([], fvs)
+      ls
+
+-- | Partitions lets into used and unused in a given term
+-- note that some of the unused may be used in later unused, but not in later used or in the term
+partitionLets :: [(a, LetBinding)] -> Expr -> ([(a, LetBinding)],[(a, LetBinding)])
+partitionLets ls e = fst $ foldr
+     ( \l ((used,unused), fvs') ->
+          let ln = letBindingName $ snd l
+           in if ln `S.member` fvs'
+                then ((l : used, unused), S.delete ln fvs' `S.union` setOf (_2 % _freeVarsLetBinding) l)
+                else ((used, l:unused), fvs')
+      )
+     (([],[]),freeVars e)
+     ls
+
+-- | Partitions lets into used and unused in a given term
+-- note that some of the unused may be used in later unused, but not in later used or in the term
+partitionLetsTy :: [(a, LetTypeBinding)] -> Type -> ([(a, LetTypeBinding)],[(a, LetTypeBinding)])
+partitionLetsTy ls t = fst $ foldr
+     ( \l@(_,LetTypeBind n l') ((used,unused), fvs') ->
+           if n `S.member` fvs'
+                then ((l : used, unused), S.delete n fvs' `S.union` freeVarsTy l')
+                else ((used, l:unused), fvs')
+      )
+     (([],[]),freeVarsTy t)
+     ls
+
+runRedexTy :: MonadEval l m => RunRedexOptions -> RedexType -> m (Type, EvalDetail)
+runRedexTy _opts (InlineLetInType{ty, letID, varID, var}) = do
   let details =
         LocalVarInlineDetail
           { letID
           , varID
           , valueID = getID ty
           , bindingName = var
-          , replacementID = getID ty'
+          , replacementID = getID ty
           , isTypeVar = True
           }
-  pure (ty', LocalTypeVarInline details)
--- let a = s in t  ~>  t  if a does not appear in t
-runRedexTy (ElideLetInType{body, orig, letBinding = (LetTypeBind v _)}) = do
+  pure (ty, LocalTypeVarInline details)
+runRedexTy opts (PushLetType{bindings, intoTy, origTy}) = do
+  ty' <- descendM (addTLets opts $ LetTyBind . snd <$> bindings) intoTy
   let details =
-        LetRemovalDetail
-          { before = orig
-          , after = body
-          , bindingName = unLocalName v
-          , letID = getID orig
-          , bodyID = getID body
+        PushLetDetail
+          { before = origTy
+          , after = ty'
+          , letIDs = toList $ fst <$> bindings
+          , letBindingNames = toList $ letTypeBindingName . snd <$> bindings
+          , intoID = getID intoTy
           }
-  pure (body, TLetRemoval details)
--- let a = s a in t a a  ~>  let b = s a in let a = b in t a a
-runRedexTy (RenameSelfLetInType{letBinding = LetTypeBind a s, body, orig}) = do
-  b <- freshLocalName (freeVarsTy s <> freeVarsTy body)
-  insertedLet <- tlet a (tvar b) $ pure body
-  result <- tlet b (pure s) $ pure insertedLet
-  let details =
-        BindRenameDetail
+  pure (ty', PushLetDownTy details)
+-- let a = s in t  ~>  t  if a does not appear in t
+runRedexTy _opts (ElideLetInType{body, orig, letBindingsKeep, letBindingsDrop}) = do
+  let ty = unviewLetsTy letBindingsKeep body
+      details =
+        LetRemovalDetail
           { before = orig
-          , after = result
-          , bindingNamesOld = [unLocalName a]
-          , bindingNamesNew = [unLocalName b]
-          , bindersOld = [getID orig]
-          , bindersNew = [getID result]
-          , bindingOccurrences = findFreeOccurrencesType a s
-          , renamingLets = [getID insertedLet]
+          , after = ty
+            , bindingNames = letTypeBindingName . snd <$> letBindingsDrop
+            , letIDs = fst <$> letBindingsDrop
           , bodyID = getID body
           }
-  pure (result, TBindRename details)
+  pure (ty, TLetRemoval details)
 -- ∀a:k.t  ~>  ∀b:k. let a = b in t  for fresh b, avoiding the given set
-runRedexTy (RenameForall{meta, origBinder, kind, body, avoid, orig}) = do
+runRedexTy _opts (RenameForall{meta, origBinder, kind, body, avoid, orig}) = do
   newBinder <- freshLocalName (avoid <> freeVarsTy body <> bindersBelowTy (focus body))
   insertedLet <- tlet origBinder (tvar newBinder) (pure body)
   let result = TForall meta newBinder kind insertedLet
diff --git a/primer/src/Primer/EvalFull.hs b/primer/src/Primer/EvalFull.hs
index 8dca22531..1ea28ba2b 100644
--- a/primer/src/Primer/EvalFull.hs
+++ b/primer/src/Primer/EvalFull.hs
@@ -28,7 +28,7 @@ import Primer.Eval.Redex (
   EvalLog (..),
   MonadEval,
   runRedex,
-  runRedexTy,
+  runRedexTy, ViewRedexOptions, RunRedexOptions,
  )
 import Primer.TypeDef (
   TypeDefMap,
@@ -49,8 +49,8 @@ newtype EvalFullError
 type TerminationBound = Natural
 
 -- A naive implementation of normal-order reduction
-evalFull :: MonadEval l m => TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr)
-evalFull tydefs env n d expr = snd <$> evalFullStepCount tydefs env n d expr
+evalFull :: MonadEval l m => ViewRedexOptions -> RunRedexOptions -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr)
+evalFull optsV optsR tydefs env n d expr = snd <$> evalFullStepCount optsV optsR tydefs env n d expr
 
 -- | As 'evalFull', but also returns how many reduction steps were taken.
 -- (This is mostly useful for testing purposes.)
@@ -62,26 +62,28 @@ evalFull tydefs env n d expr = snd <$> evalFullStepCount tydefs env n d expr
 -- more to notice termination.
 evalFullStepCount ::
   MonadEval l m =>
+  ViewRedexOptions ->
+  RunRedexOptions ->
   TypeDefMap ->
   DefMap ->
   TerminationBound ->
   Dir ->
   Expr ->
   m (Natural, Either EvalFullError Expr)
-evalFullStepCount tydefs env n d = go 0
+evalFullStepCount optsV optsR tydefs env n d = go 0
   where
     go s expr
       | s >= n = pure (s, Left $ TimedOut expr)
       | otherwise =
-          runMaybeT (step tydefs env d expr) >>= \case
+          runMaybeT (step optsV optsR tydefs env d expr) >>= \case
             Nothing -> pure (s, Right expr) -- this is a normal form
             Just e -> go (s + 1) e
 
 -- The 'Dir' argument only affects what happens if the root is an annotation:
 -- do we keep it (Syn) or remove it (Chk). I.e. is an upsilon reduction allowed
 -- at the root?
-step :: MonadEval l m => TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m Expr
-step tydefs g d e =
-  findRedex tydefs g d e >>= \case
-    RExpr ez r -> lift $ unfocusExpr . flip replace ez . fst <$> runRedex r
-    RType et r -> lift $ unfocusExpr . unfocusType . flip replace et . fst <$> runRedexTy r
+step :: MonadEval l m => ViewRedexOptions -> RunRedexOptions -> TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m Expr
+step optsV optsR tydefs g d e =
+  findRedex optsV tydefs g d e >>= \case
+    RExpr ez r -> lift $ unfocusExpr . flip replace ez . fst <$> runRedex optsR r
+    RType et r -> lift $ unfocusExpr . unfocusType . flip replace et . fst <$> runRedexTy optsR r
diff --git a/primer/src/Primer/Pretty.hs b/primer/src/Primer/Pretty.hs
index bc70c1293..126634c26 100644
--- a/primer/src/Primer/Pretty.hs
+++ b/primer/src/Primer/Pretty.hs
@@ -60,6 +60,10 @@ data PrettyOptions = PrettyOptions
   -- ^ Attempt to print λs and Λs on one line
   , inlineForAll :: Bool
   -- ^ Attempt to print @for all@ and associated type sig on one line
+  , inlineCon :: Bool
+  -- ^ Attempt to print constructors and all arguments on one line
+  , inlineAnn :: Bool
+  -- ^ Attempt to print annotations on one line
   }
 
 -- | Default PrettyOptions - makes no attempt to group text
@@ -71,6 +75,8 @@ sparse =
     , inlineLet = False
     , inlineLambda = False
     , inlineForAll = False
+    , inlineCon = False
+    , inlineAnn = False
     }
 
 -- | Groups whenever possible
@@ -82,6 +88,8 @@ compact =
     , inlineLet = True
     , inlineLambda = True
     , inlineForAll = True
+    , inlineCon = True
+    , inlineAnn = True
     }
 
 -- | Pretty prints @Expr'@ using Prettyprinter library
@@ -91,7 +99,7 @@ prettyExpr opts = \case
   EmptyHole _ -> col Red "?"
   Con _ n tms ->
     let prettyTms = brac Round White . pE <$> tms
-     in vsep $ col Green (gname opts n) : prettyTms
+     in (if inlineCon opts then group else identity) $ vsep $ col Green (gname opts n) : prettyTms
   Var _ v -> case v of
     GlobalVarRef n -> col Blue (gname opts n)
     LocalVarRef n -> lname n
@@ -161,7 +169,7 @@ prettyExpr opts = \case
         <> inlineblock opts (pE e)
         <> col Yellow "in"
         <> line
-        <> indent' 2 (pE e')
+        <> indent' 2 (brac Round White $ pE e')
   LetType _ v t e ->
     col Yellow "let type"
       <+> lname v
@@ -169,7 +177,7 @@ prettyExpr opts = \case
         <> inlineblock opts (pT t)
         <> col Yellow "in"
         <> line
-        <> indent' 2 (pE e)
+        <> indent' 2 (brac Round White $ pE e)
   Letrec _ v e t e' ->
     col Yellow "let rec"
       <+> lname v
@@ -177,7 +185,7 @@ prettyExpr opts = \case
         <> inlineblock opts (typeann e t)
         <> col Yellow "in"
         <> line
-        <> indent' 2 (pE e')
+        <> indent' 2 (brac Round White $ pE e')
   PrimCon _ p -> prim p
   where
     pT = prettyType opts
@@ -185,7 +193,7 @@ prettyExpr opts = \case
     prim = \case
       PrimChar c -> "Char" <+> pretty @Text (show c)
       PrimInt n -> "Int" <+> pretty @Text (show n)
-    typeann e t = brac Round Yellow (pE e) <+> col Yellow "::" <> line <> brac Round Yellow (pT t)
+    typeann e t = brac Round Yellow (pE e) <+> (if inlineAnn opts then group else identity) (col Yellow "::" <> line <> brac Round Yellow (pT t))
 
 -- When grouped: " x "
 -- When ungrouped: "\n\tx\n"
@@ -226,10 +234,15 @@ rBrac Curly = "?}"
 
 -- Adds brackets of type b around "doc" with color c
 brac :: BracketType -> Color -> Doc AnsiStyle -> Doc AnsiStyle
-brac b c doc = col c (lBrac b) <> line' <> flatAlt (indent 2 doc) doc <> line' <> col c (rBrac b)
+--brac b c doc = col c (lBrac b) <> line' <> flatAlt (indent 2 doc) doc <> line' <> col c (rBrac b)
+brac b c doc = if 1 == length (T.words $ show doc) -- TODO: hack to avoid superfluous brackets
+  then doc
+  else col c (lBrac b) <> line' <> flatAlt (indent 2 doc) doc <> line' <> col c (rBrac b)
 
 col :: Color -> Doc AnsiStyle -> Doc AnsiStyle
-col = annotate . color
+col = \case
+  White -> identity -- TODO: hack! we use "White" to mean "terminal default"
+  c -> annotate $ color c
 
 -- | Pretty prints @Type'@ using Prettyprinter library
 prettyType :: PrettyOptions -> Type' b -> Doc AnsiStyle
@@ -254,7 +267,7 @@ prettyType opts typ = case typ of
         <> inlineblock opts (pT t)
         <> col Yellow "in"
         <> line
-        <> indent' 2 (pT b)
+        <> indent' 2 (brac Round White $ pT b)
   where
     pT = prettyType opts
 
diff --git a/primer/src/Primer/Zipper/Type.hs b/primer/src/Primer/Zipper/Type.hs
index 2c02d2fa2..152cd8db1 100644
--- a/primer/src/Primer/Zipper/Type.hs
+++ b/primer/src/Primer/Zipper/Type.hs
@@ -25,6 +25,7 @@ module Primer.Zipper.Type (
   bindersAboveTy,
   LetTypeBinding' (LetTypeBind),
   LetTypeBinding,
+  letTypeBindingName,
   getBoundHereTy',
   getBoundHereTy,
   getBoundHereUpTy,
@@ -54,11 +55,13 @@ import Primer.Core.Meta (
   ID,
   TyVarName,
   getID,
+  unLocalName,
  )
 import Primer.Core.Type (
   Type' (TForall, TLet),
   TypeMeta,
  )
+import Primer.Name (Name)
 
 type TypeZip' b = Zipper (Type' b) (Type' b)
 
@@ -193,6 +196,9 @@ data LetTypeBinding' a = LetTypeBind TyVarName (Type' a)
   deriving stock (Eq, Show)
 type LetTypeBinding = LetTypeBinding' TypeMeta
 
+letTypeBindingName :: LetTypeBinding' a -> Name
+letTypeBindingName (LetTypeBind n _) = unLocalName n
+
 getBoundHereTy' :: Eq a => Type' a -> Maybe (Type' a) -> [Either TyVarName (LetTypeBinding' a)]
 getBoundHereTy' t prev = case t of
   TForall _ v _ _ -> [Left v]
diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs
index 147b6de0e..f8ad267a5 100644
--- a/primer/test/Tests/Eval.hs
+++ b/primer/test/Tests/Eval.hs
@@ -4,7 +4,6 @@ module Tests.Eval where
 
 import Foreword
 
-import Control.Monad.Trans.Maybe (runMaybeT)
 import Data.List (delete)
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
@@ -20,24 +19,24 @@ import Primer.App (
  )
 import Primer.Builtins (
   boolDef,
+  cCons,
   cFalse,
   cNil,
   cTrue,
   cZero,
   tBool,
+  tList,
  )
 import Primer.Core (
   Expr,
   GlobalName (baseName, qualifiedModule),
   ID,
   Kind' (KFun, KType),
-  LocalName,
   Pattern (PatCon, PatPrim),
   PrimCon (PrimChar),
   Type,
   Type' (TCon, TEmptyHole, TFun, TVar),
   getID,
-  unLocalName,
   unsafeMkGlobalName,
   _id,
  )
@@ -58,8 +57,9 @@ import Primer.Eval (
   GlobalVarInlineDetail (..),
   LetRemovalDetail (..),
   LocalVarInlineDetail (..),
+  PushLetDetail (..),
   findNodeByID,
-  getNonCapturedLocal,
+  lookupEnclosingLet,
   redexes,
   singletonCxt,
   step,
@@ -90,7 +90,6 @@ import Primer.TypeDef (
  )
 import Primer.Typecheck (typeDefs)
 import Primer.Zipper (
-  LetBinding,
   LetBinding' (LetBind, LetTyBind, LetrecBind),
   LetTypeBinding' (LetTypeBind),
   target,
@@ -204,39 +203,19 @@ unit_tryReduce_BETA = do
 
 unit_tryReduce_local_term_var :: Assertion
 unit_tryReduce_local_term_var = do
-  -- We assume we're inside a larger expression (e.g. a let) where the node that binds x has ID 5.
+  -- We assume we're immediately inside a 'let x'
   let ((expr, val), i) = create $ (,) <$> lvar "x" <*> con0' ["M"] "C"
-      locals = singletonCxt @ID 5 $ LetBind "x" val
+      locals = singletonCxt $ LetBind "x" val
   result <- runTryReduce tydefs mempty locals (expr, i)
-  case result of
-    Right (expr', LocalVarInline detail) -> do
-      expr' ~= val
-
-      detail.letID @?= 5
-      detail.varID @?= 0
-      detail.bindingName @?= "x"
-      detail.valueID @?= 1
-      detail.replacementID @?= 2
-      detail.isTypeVar @?= False
-    _ -> assertFailure $ show result
+  result @?= Left NotRedex
 
 unit_tryReduce_local_type_var :: Assertion
 unit_tryReduce_local_type_var = do
-  -- We assume we're inside a larger expression (e.g. a let type) where the node that binds x has ID 5.
+  -- We assume we're immediately inside a 'let x'
   let ((tyvar, val), i) = create $ (,) <$> tvar "x" <*> tcon' ["M"] "C"
-      locals = singletonCxt @ID 5 $ LetTyBind $ LetTypeBind "x" val
+      locals = singletonCxt $ LetTyBind $ LetTypeBind "x" val
   result <- runTryReduceType mempty locals (tyvar, i)
-  case result of
-    Right (ty, LocalTypeVarInline detail) -> do
-      ty ~~= val
-
-      detail.letID @?= 5
-      detail.varID @?= 0
-      detail.bindingName @?= "x"
-      detail.valueID @?= 1
-      detail.replacementID @?= 2
-      detail.isTypeVar @?= True
-    _ -> assertFailure $ show result
+  result @?= Left NotRedex
 
 unit_tryReduce_global_var :: Assertion
 unit_tryReduce_global_var = do
@@ -269,30 +248,27 @@ unit_tryReduce_let = do
 
       detail.before @?= expr
       detail.after ~= expectedResult
-      detail.bindingName @?= "x"
-      detail.letID @?= 0
+      detail.bindingNames @?= ["x"]
+      detail.letIDs @?= [0]
       detail.bodyID @?= 2
     _ -> assertFailure $ show result
 
--- let x = x in x ==> let y = x in let x = y in x
+-- let x = x in x ==> x
 unit_tryReduce_let_self_capture :: Assertion
 unit_tryReduce_let_self_capture = do
   let (expr, i) = create $ let_ "x" (lvar "x") (lvar "x")
-      expectedResult = create' $ let_ "a3" (lvar "x") $ let_ "x" (lvar "a3") (lvar "x")
+      expectedResult = create' $ lvar "x"
   result <- runTryReduce tydefs mempty mempty (expr, i)
   case result of
-    Right (expr', BindRename detail) -> do
+    Right (expr', LocalVarInline detail) -> do
       expr' ~= expectedResult
 
-      detail.before @?= expr
-      detail.after ~= expectedResult
-      detail.bindingNamesOld @?= ["x"]
-      detail.bindingNamesNew @?= ["a3"]
-      detail.bindersOld @?= [0]
-      detail.bindersNew @?= [6]
-      detail.bindingOccurrences @?= [1]
-      detail.renamingLets @?= [4]
-      detail.bodyID @?= 2
+      detail.letID @?= 0
+      detail.varID @?= 2
+      detail.bindingName @?= "x"
+      detail.valueID @?= 1
+      detail.replacementID @?= 1
+      detail.isTypeVar @?= False
     _ -> assertFailure $ show result
 
 unit_tryReduce_lettype :: Assertion
@@ -306,30 +282,26 @@ unit_tryReduce_lettype = do
 
       detail.before @?= expr
       detail.after ~= expectedResult
-      detail.bindingName @?= "x"
-      detail.letID @?= 0
+      detail.bindingNames @?= ["x"]
+      detail.letIDs @?= [0]
       detail.bodyID @?= 2
     _ -> assertFailure $ show result
 
--- let type x = x in _ :: x ==> let type y = x in lettype x = y in _ :: x
+-- let type x = x in ? :: x ==> ? :: (tlet x = x in x)
 unit_tryReduce_lettype_self_capture :: Assertion
 unit_tryReduce_lettype_self_capture = do
   let (expr, i) = create $ letType "x" (tvar "x") (emptyHole `ann` tvar "x")
-      expectedResult = create' $ letType "a5" (tvar "x") $ letType "x" (tvar "a5") (emptyHole `ann` tvar "x")
+      expectedResult = create' $ emptyHole `ann` tlet "x" (tvar "x") (tvar "x")
   result <- runTryReduce tydefs mempty mempty (expr, i)
   case result of
-    Right (expr', BindRename detail) -> do
+    Right (expr', PushLetDown detail) -> do
       expr' ~= expectedResult
 
       detail.before @?= expr
       detail.after ~= expectedResult
-      detail.bindingNamesOld @?= ["x"]
-      detail.bindingNamesNew @?= ["a5"]
-      detail.bindersOld @?= [0]
-      detail.bindersNew @?= [8]
-      detail.bindingOccurrences @?= [1]
-      detail.renamingLets @?= [6]
-      detail.bodyID @?= 2
+      detail.letIDs @?= [0]
+      detail.letBindingNames @?= ["x"]
+      detail.intoID @?= 2
     _ -> assertFailure $ show result
 
 -- tlet x = C in ty ==> ty  when x not occur free in ty
@@ -344,31 +316,27 @@ unit_tryReduce_tlet_elide = do
 
       detail.before @?= ty
       detail.after ~~= expectedResult
-      detail.bindingName @?= "x"
-      detail.letID @?= 0
+      detail.bindingNames @?= ["x"]
+      detail.letIDs @?= [0]
       detail.bodyID @?= 2
     _ -> assertFailure $ show result
 
--- tlet x = x in x ==> tlet y = x in  tlet x = y in x
+-- tlet x = x in x ==> x
 unit_tryReduce_tlet_self_capture :: Assertion
 unit_tryReduce_tlet_self_capture = do
   let (ty, i) = create $ tlet "x" (tvar "x") (tvar "x")
-      n = "a3"
-      expectedResult = create' $ tlet n (tvar "x") $ tlet "x" (tvar n) (tvar "x")
+      expectedResult = create' $ tvar "x"
   result <- runTryReduceType mempty mempty (ty, i)
   case result of
-    Right (ty', TBindRename detail) -> do
+    Right (ty', LocalTypeVarInline detail) -> do
       ty' ~~= expectedResult
 
-      detail.before @?= ty
-      detail.after ~~= expectedResult
-      detail.bindingNamesOld @?= ["x"]
-      detail.bindingNamesNew @?= [unLocalName n]
-      detail.bindersOld @?= [0]
-      detail.bindersNew @?= [6]
-      detail.bindingOccurrences @?= [1]
-      detail.renamingLets @?= [4]
-      detail.bodyID @?= 2
+      detail.letID @?= 0
+      detail.varID @?= 2
+      detail.bindingName @?= "x"
+      detail.valueID @?= 1
+      detail.replacementID @?= 1
+      detail.isTypeVar @?= True
     _ -> assertFailure $ show result
 
 unit_tryReduce_letrec :: Assertion
@@ -382,8 +350,8 @@ unit_tryReduce_letrec = do
 
       detail.before @?= expr
       detail.after ~= expectedResult
-      detail.bindingName @?= "x"
-      detail.letID @?= 0
+      detail.bindingNames @?= ["x"]
+      detail.letIDs @?= [0]
       detail.bodyID @?= 3
     _ -> assertFailure $ show result
 
@@ -757,6 +725,42 @@ unit_tryReduce_prim_fail_unreduced_args = do
   result <- runTryReduce tydefs prims mempty (expr, i)
   result @?= Left NotRedex
 
+-- we should not elide @let x = ...@ here, as it is required for @let y@ which is not elided
+unit_tryReduce_push_elide_1 :: Assertion
+unit_tryReduce_push_elide_1 = do
+  let (expr, i) =
+        create $ let_ "x" (con0 cTrue) $ let_ "y" (lvar "x") $ lam "z" $ lvar "y"
+  result <- runTryReduce tydefs mempty mempty (expr, i)
+  case result of
+    Right (expr', _) -> expr' ~= create' (lam "z" $ let_ "x" (con0 cTrue) $ let_ "y" (lvar "x") $ lvar "y")
+    _ -> assertFailure $ show result
+
+-- we should elide the outer @let x = ...@ in one branch, and the inner in the other
+unit_tryReduce_push_elide_2 :: Assertion
+unit_tryReduce_push_elide_2 = do
+  let (expr, i) =
+        create $ let_ "x" (con0 cTrue) $ let_ "y" (lvar "x") $ let_ "x" (con0 cFalse) $ app (lvar "x") (lvar "y")
+  result <- runTryReduce tydefs mempty mempty (expr, i)
+  case result of
+    Right (expr', _) ->
+      expr'
+        ~= create'
+          ( app
+              (let_ "x" (con0 cFalse) $ lvar "x")
+              (let_ "x" (con0 cTrue) $ let_ "y" (lvar "x") $ lvar "y")
+          )
+    _ -> assertFailure $ show result
+
+-- we should not elide the outer @let x = ...@ here
+unit_tryReduce_push_elide_3 :: Assertion
+unit_tryReduce_push_elide_3 = do
+  let (expr, i) =
+        create $ let_ "x" (con0 cTrue) $ let_ "x" (lvar "x") $ lam "z" $ lvar "x"
+  result <- runTryReduce tydefs mempty mempty (expr, i)
+  case result of
+    Right (expr', _) -> expr' ~= create' (lam "z" $ let_ "x" (con0 cTrue) $ let_ "x" (lvar "x") $ lvar "x")
+    _ -> assertFailure $ show result
+
 runStep :: ID -> TypeDefMap -> DefMap -> (Expr, ID) -> IO (Either EvalError (Expr, EvalDetail))
 runStep i' tys globals (e, i) = do
   let (r, logs) = evalTestM i' $ runPureLogT $ step @EvalLog tys globals e Syn i
@@ -794,16 +798,6 @@ unit_step_non_redex =
 
 -- * 'findNodeByID' tests
 
-lookupNonCaptured :: LocalName k -> Cxt -> Maybe (ID, LetBinding)
-lookupNonCaptured = runReader . runMaybeT . getNonCapturedLocal
-
-lookupCaptured :: LocalName k -> Cxt -> Maybe (ID, LetBinding)
-lookupCaptured n c@(Cxt c')
-  | Nothing <- lookupNonCaptured n c
-  , Just (Just r, i, _) <- Map.lookup (unLocalName n) c' =
-      pure (i, r)
-  | otherwise = Nothing
-
 unit_findNodeByID_letrec :: Assertion
 unit_findNodeByID_letrec = do
   let expr = create' $ letrec "x" (lvar "x") (tcon' ["M"] "T") (lvar "x")
@@ -811,27 +805,25 @@ unit_findNodeByID_letrec = do
       t = create' $ tcon' ["M"] "T"
   case findNodeByID 0 Syn expr of
     Just (Cxt locals, Left (_, z)) -> do
-      assertBool "no locals in scope at node 0" $ Map.null locals
+      assertBool "no enclosing lets at node 0" $ null locals
       target z ~= expr
     _ -> assertFailure "node 0 not found"
   case findNodeByID 1 Syn expr of
-    Just (locals, Left (_, z)) -> do
+    Just (Cxt locals, Left (_, z)) -> do
       target z ~= x
-      case lookupNonCaptured "x" locals of
-        Just (0, LetrecBind _ e _) -> e ~= x
-        r -> assertFailure $ "expected to find 'x' bound at id 0, with rhs = 'x', but found " <> show r
+      assertBool "no enclosing lets at node 1" $ null locals
     _ -> assertFailure "node 1 not found"
   case findNodeByID 2 Syn expr of
     Just (Cxt locals, Right z) -> do
       target z ~~= t
-      assertBool "no locals in scope at node 2" $ Map.null locals
+      assertBool "no enclosing lets at node 2" $ null locals
     _ -> assertFailure "node 2 not found"
   case findNodeByID 3 Syn expr of
     Just (locals, Left (_, z)) -> do
       target z ~= x
-      case lookupNonCaptured "x" locals of
-        Just (0, LetrecBind _ e _) -> e ~= x
-        r -> assertFailure $ "expected to find 'x' bound at id 0, with rhs = 'x', but found " <> show r
+      case lookupEnclosingLet "x" locals of
+        Just (LetrecBind _ e _) -> e ~= x
+        r -> assertFailure $ "expected to find 'x' let-bound, with rhs = 'x', but found " <> show r
     _ -> assertFailure "node 3 not found"
 
 unit_findNodeByID_1 :: Assertion
@@ -846,9 +838,8 @@ unit_findNodeByID_1 = do
         pure (x_, c_, e)
   case findNodeByID 0 Syn expr of
     Just (locals, Left (_, z)) -> do
-      case lookupNonCaptured "x" locals of
-        Just (i, LetBind _ e) -> do
-          i @?= 2
+      case lookupEnclosingLet "x" locals of
+        Just (LetBind _ e) -> do
           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"
@@ -857,19 +848,19 @@ unit_findNodeByID_1 = do
 
   case findNodeByID 1 Syn expr of
     Just (Cxt locals, Left (_, z)) -> do
-      assertBool "expected nothing in scope" $ Map.null locals
+      assertBool "expected nothing in scope" $ null locals
       target z ~= c
     _ -> assertFailure "node 1 not found"
 
   case findNodeByID 2 Syn expr of
     Just (Cxt locals, Left (_, z)) -> do
-      assertBool "expected nothing in scope" $ Map.null locals
+      assertBool "expected nothing in scope" $ null locals
       target z ~= expr
     _ -> assertFailure "node 2 not found"
 
 unit_findNodeByID_2 :: Assertion
 unit_findNodeByID_2 = do
-  let (x, t, expr) = create' $ do
+  let (x, _, expr) = create' $ do
         -- id 0
         x_ <- tvar "x"
         -- id 1
@@ -879,12 +870,9 @@ unit_findNodeByID_2 = do
         pure (x_, t_, e)
   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"
+      case lookupEnclosingLet "x" locals of
+        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"
 
@@ -900,9 +888,8 @@ unit_findNodeByID_tlet = do
         pure (x_, t_, e)
   case findNodeByID 0 Syn expr of
     Just (locals, Right z) -> do
-      case lookupNonCaptured "x" locals of
-        Just (i, LetTyBind (LetTypeBind _ e)) -> do
-          i @?= 4
+      case lookupEnclosingLet "x" locals of
+        Just (LetTyBind (LetTypeBind _ e)) -> do
           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"
@@ -913,10 +900,10 @@ unit_findNodeByID_scoping_1 :: Assertion
 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 ->
+    Just (locals, Left _)
+      | Nothing <- lookupEnclosingLet "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
@@ -927,8 +914,8 @@ unit_findNodeByID_scoping_2 = do
         pure (b, e)
   case findNodeByID 4 Syn expr of
     Just (locals@(Cxt locals'), Left _)
-      | Map.size locals' == 1
-      , lookupNonCaptured "x" locals == Just (3, LetBind "x" bind) ->
+      | length locals' == 2
+      , lookupEnclosingLet "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 +933,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 ->
+            | null locals'
+            , Nothing <- lookupEnclosingLet "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 +952,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 ->
+            | null locals'
+            , Nothing <- lookupEnclosingLet "x" locals
+            , Nothing <- lookupEnclosingLet "z" locals ->
                 pure ()
-          Just (_, Right _) -> assertFailure "Expected lettype binding of 'x' and the tlet binding of 'z' 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
@@ -1140,59 +1127,55 @@ unit_redexes_LAM_4 =
               )
           )
    in do
-        redexesOf (e noAnn) <@?=> Set.singleton 5
-        redexesOf (e withAnn) <@?=> Set.fromList [3, 6]
+        redexesOf (e noAnn) <@?=> Set.singleton 0
+        redexesOf (e withAnn) <@?=> Set.fromList [0, 3]
 
 unit_redexes_let_1 :: Assertion
 unit_redexes_let_1 =
   redexesOf (let_ "x" (con0' ["M"] "C") (app (lvar "x") (lvar "y")))
-    <@?=> Set.singleton 3
+    <@?=> Set.singleton 0
 
 unit_redexes_let_2 :: Assertion
 unit_redexes_let_2 =
   redexesOf (let_ "x" (con0' ["M"] "C") (lam "x" (app (lvar "x") (lvar "y"))))
-    <@?=> Set.singleton 0
+    <@?=> Set.fromList [0, 2]
 
--- We cannot substitute one occurrence of a let-bound variable if it
--- would result in capture of a free variable in the bound term by the
--- let binder itself.
 unit_redexes_let_3 :: Assertion
 unit_redexes_let_3 = do
-  -- NB we must not say node 3 (the occurrence of the variable) is a redex
   redexesOf (lam "x" $ let_ "x" (lvar "x") (lvar "x")) <@?=> Set.fromList [1]
 
--- We cannot substitute one occurrence of a let-bound variable if it
--- would result in capture of a free variable in the bound term by the
--- some intervening binder.
+-- We cannot push a let under a binder if it would result in capture of a free
+-- variable in the bound term.
 unit_redexes_let_capture :: Assertion
 unit_redexes_let_capture =
   -- We should rename the lambda, and not inline the variable
   redexesOf (let_ "x" (lvar "y") $ lam "y" $ lvar "x") <@?=> Set.singleton 2
 
 unit_redexes_lettype_capture :: Assertion
-unit_redexes_lettype_capture =
-  -- We should rename the forall and not inline the variable
-  redexesOf (letType "x" (tvar "y") (emptyHole `ann` tforall "y" (KType ()) (tvar "x"))) <@?=> Set.singleton 4
+unit_redexes_lettype_capture = do
+  -- We can push the letType down once
+  redexesOf (letType "x" (tvar "y") (emptyHole `ann` tforall "y" (KType ()) (tvar "x"))) <@?=> Set.singleton 0
+  -- 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
 
 unit_redexes_letrec_1 :: Assertion
 unit_redexes_letrec_1 =
   redexesOf (letrec "x" (con1' ["M"] "C" $ lvar "x") (tcon' ["M"] "T") (app (lvar "x") (lvar "y")))
-    <@?=> Set.fromList [2, 5]
+    <@?=> Set.fromList [0]
 
 unit_redexes_letrec_2 :: Assertion
 unit_redexes_letrec_2 =
   redexesOf (letrec "x" (con1' ["M"] "C" $ lvar "x") (tcon' ["M"] "T") (lvar "y"))
-    <@?=> Set.fromList [0, 2]
+    <@?=> Set.fromList [0]
 
--- Test that our self-capture logic does not apply to letrec.
 unit_redexes_letrec_3 :: Assertion
 unit_redexes_letrec_3 =
-  -- If this were a let, we would not be able to substitute, but it is possible for letrec
-  redexesOf (lAM "a" $ lam "x" $ letrec "x" (lvar "x") (tvar "a") (lvar "x")) <@?=> Set.fromList [3, 5]
+  redexesOf (lAM "a" $ lam "x" $ letrec "x" (lvar "x") (tvar "a") (lvar "x")) <@?=> Set.fromList [2]
+
+unit_redexes_letrec_4 :: Assertion
+unit_redexes_letrec_4 =
+  redexesOf (let_ "x" ((lam "x" (lvar "x") `ann` (tcon tBool `tfun` tcon tBool)) `app` con0 cTrue) $ letrec "xs" (con cCons [lvar "x", lvar "xs"]) (tcon tList `tapp` tEmptyHole) (lvar "xs")) <@?=> Set.fromList [1, 9]
 
--- The application could potentially be reduced by pushing the
--- argument inside the letrec, but that is not a reduction rule. Once
--- we inline the letrec enough we would be able to see the beta.
 unit_redexes_letrec_app_1 :: Assertion
 unit_redexes_letrec_app_1 =
   let e mkAnn =
@@ -1205,12 +1188,9 @@ unit_redexes_letrec_app_1 =
           )
           (con0' ["M"] "D")
    in do
-        redexesOf (e noAnn) <@?=> Set.fromList [5]
-        redexesOf (e withAnn) <@?=> Set.fromList [6]
+        redexesOf (e noAnn) <@?=> Set.fromList [1]
+        redexesOf (e withAnn) <@?=> Set.fromList [1]
 
--- The application could potentially be reduced by pushing the
--- argument inside the letrec, but that is not a reduction rule. Once
--- we inline the letrec enough we would be able to see the beta.
 unit_redexes_letrec_APP_1 :: Assertion
 unit_redexes_letrec_APP_1 =
   let e mkAnn =
@@ -1223,8 +1203,8 @@ unit_redexes_letrec_APP_1 =
           )
           (tcon' ["M"] "D")
    in do
-        redexesOf (e noAnn) <@?=> Set.fromList [5]
-        redexesOf (e withAnn) <@?=> Set.fromList [6]
+        redexesOf (e noAnn) <@?=> Set.fromList [1]
+        redexesOf (e withAnn) <@?=> Set.fromList [1]
 
 unit_redexes_lettype_1 :: Assertion
 unit_redexes_lettype_1 =
@@ -1232,18 +1212,14 @@ unit_redexes_lettype_1 =
 
 unit_redexes_lettype_2 :: Assertion
 unit_redexes_lettype_2 =
-  redexesOf (letType "x" (tcon' ["M"] "T") (con0' ["M"] "C" `ann` tvar "x")) <@?=> Set.fromList [4]
+  redexesOf (letType "x" (tcon' ["M"] "T") (con0' ["M"] "C" `ann` tvar "x")) <@?=> Set.fromList [0]
 
 unit_redexes_lettype_3 :: Assertion
 unit_redexes_lettype_3 =
-  redexesOf (letType "x" (tcon' ["M"] "T") (letrec "y" (con0' ["M"] "C") (tvar "x") (lvar "y"))) <@?=> Set.fromList [4, 5]
+  redexesOf (letType "x" (tcon' ["M"] "T") (letrec "y" (con0' ["M"] "C") (tvar "x") (lvar "y"))) <@?=> Set.fromList [2]
 
--- We cannot substitute one occurrence of a let-bound variable if it
--- would result in capture of a free variable in the bound term by the
--- let binder itself.
 unit_redexes_lettype_4 :: Assertion
 unit_redexes_lettype_4 = do
-  -- NB we must not say node 5 (the occurrence of the variable) is a redex
   redexesOf (lAM "x" $ letType "x" (tvar "x") (emptyHole `ann` tvar "x")) <@?=> Set.fromList [1]
 
 unit_redexes_tlet_1 :: Assertion
@@ -1252,18 +1228,14 @@ unit_redexes_tlet_1 =
 
 unit_redexes_tlet_2 :: Assertion
 unit_redexes_tlet_2 =
-  redexesOf (emptyHole `ann` tlet "x" (tcon' ["M"] "T") (tapp (tcon' ["M"] "S") (tvar "x"))) <@?=> Set.fromList [6]
+  redexesOf (emptyHole `ann` tlet "x" (tcon' ["M"] "T") (tapp (tcon' ["M"] "S") (tvar "x"))) <@?=> Set.fromList [2]
 
 unit_redexes_tlet_3 :: Assertion
 unit_redexes_tlet_3 =
-  redexesOf (emptyHole `ann` tlet "x" (tcon' ["M"] "T") (tlet "y" (tcon' ["M"] "S") (tapp (tvar "x") (tvar "y")))) <@?=> Set.fromList [7, 8]
+  redexesOf (emptyHole `ann` tlet "x" (tcon' ["M"] "T") (tlet "y" (tcon' ["M"] "S") (tapp (tvar "x") (tvar "y")))) <@?=> Set.fromList [2, 4]
 
--- We cannot substitute one occurrence of a let-bound variable if it
--- would result in capture of a free variable in the bound term by the
--- let binder itself.
 unit_redexes_tlet_4 :: Assertion
 unit_redexes_tlet_4 = do
-  -- NB we must not say node 5 (the occurrence of the variable) is a redex
   redexesOf (lAM "x" $ emptyHole `ann` tlet "x" (tvar "x") (tvar "x")) <@?=> Set.fromList [3]
 
 -- case-of-constructor does not reduce if the constructor is not annotated
@@ -1288,7 +1260,7 @@ unit_redexes_case_2 =
     )
     <@?=> mempty
 
--- The case expression can be reduced, as can the variable x in the branch rhs.
+-- The case expression can be reduced, and the @let x@ can be pushed down
 unit_redexes_case_3 :: Assertion
 unit_redexes_case_3 =
   redexesOf
@@ -1300,10 +1272,11 @@ unit_redexes_case_3 =
             [branch' (["M"], "C") [] (lvar "x")]
         )
     )
-    <@?=> Set.fromList [2, 6]
+    <@?=> Set.fromList [0, 2]
 
--- The variable x in the rhs is bound to the branch pattern, so is no longer reducible.
--- However this means the let is redundant, and can be reduced.
+-- The variable x in the rhs is bound to the branch pattern, so is no longer refering to the @let@.
+-- This means the let is redundant, and we can either elide it or rename the inner "x" binder
+--(to prepare to push).
 unit_redexes_case_4 :: Assertion
 unit_redexes_case_4 =
   redexesOf
@@ -1317,10 +1290,28 @@ unit_redexes_case_4 =
     )
     <@?=> Set.fromList [0, 2]
 
--- If scrutinee of a case is a redex itself, we recognise that
 unit_redexes_case_5 :: Assertion
 unit_redexes_case_5 =
-  redexesOf (let_ "x" (con0' ["M"] "C") (case_ (lvar "x") [])) <@?=> Set.fromList [3]
+  redexesOf (let_ "x" (con0' ["M"] "C") (case_ (lvar "x") [])) <@?=> Set.fromList [0]
+
+-- The @let@ cannot be pushed into the @case_@, as the 'y' would be captured.
+unit_redexes_case_6 :: Assertion
+unit_redexes_case_6 =
+  redexesOf
+    ( let_
+        "x"
+        (lvar "y")
+        ( case_
+            (con0' ["M"] "C" `ann` tcon' ["M"] "C")
+            [branch' (["M"], "C") [("y", Nothing)] (lvar "x")]
+        )
+    )
+    <@?=> Set.fromList [2]
+
+-- If scrutinee of a case is a redex itself, we recognise that
+unit_redexes_case_7 :: Assertion
+unit_redexes_case_7 =
+  redexesOf (case_ (let_ "x" (con0' ["M"] "C") $ lvar "x") []) <@?=> Set.fromList [1]
 
 unit_redexes_case_fallback_1 :: Assertion
 unit_redexes_case_fallback_1 =
@@ -1355,6 +1346,13 @@ unit_redexes_let_upsilon = do
   redexesOf (letrec "x" (lam "x" emptyHole `ann` t) t $ lam "x" emptyHole `ann` t) <@?=> Set.fromList [0, 1]
   redexesOf (lam "x" $ letrec "x" (lam "x" emptyHole `ann` t) t $ emptyHole `ann` t) <@?=> Set.fromList [1, 2, 9]
 
+unit_redexes_push_let :: Assertion
+unit_redexes_push_let = do
+  redexesOf (letrec "x" (lam "x" emptyHole) tEmptyHole $ lam "x" emptyHole) <@?=> Set.fromList [0, 4]
+  redexesOf (letType "x" tEmptyHole $ let_ "y" (lam "x" emptyHole) $ lam "x" emptyHole) <@?=> Set.fromList [0, 2, 5]
+  redexesOf (letType "x" tEmptyHole $ letrec "y" (lam "x" emptyHole) tEmptyHole $ lam "x" emptyHole) <@?=> Set.fromList [0, 2, 6]
+  redexesOf (letType "x" tEmptyHole $ letType "y" (tforall "x" (KType ()) tEmptyHole) $ lam "x" emptyHole) <@?=> Set.fromList [0, 2, 5]
+
 unit_redexes_prim_1 :: Assertion
 unit_redexes_prim_1 =
   redexesOfWithPrims (pfun EqChar `app` char 'a' `app` char 'b') <@?=> Set.fromList [0]
@@ -1453,7 +1451,14 @@ tasty_type_preservation =
 -- | Reductions do not interfere with each other
 -- if @i,j ∈ redexes e@  (and @i /= j@), and @e@ reduces to @e'@ via redex @i@
 -- then @j ∈ redexes e'@,
--- unless @j@ no longer exists in @e'@ or @j@ was a rename-binding which is no longer required
+-- unless one of the following is true
+-- - @j@ no longer exists in @e'@
+-- - @j@ was a rename-binding which is no longer required
+--       (e.g. because @i@ was eliding a let, or reducing inside the binding of
+--       a let removing a variable reference)
+-- - @i@ was a PushLet, which can intersperse itself inside the parts of @j@'s redex, blocking it
+-- - @j@ was a PushLet surrounding @i@, and @i@ either reduced to a leaf or
+--       removed a variable reference, causing us to not PushLet, but ElideLet
 tasty_redex_independent :: Property
 tasty_redex_independent =
   let testModules = [builtinModule, primitiveModule]
@@ -1472,12 +1477,19 @@ tasty_redex_independent =
             s <- failWhenSevereLogs $ step @EvalLog tds globs t dir i
             case s of
               Left err -> annotateShow err >> failure
-              Right (s', _) -> do
+              Right (s', siDetails) -> do
                 annotateShow s'
                 if elemOf exprIDs j s'
                   then do
                     sj <- failWhenSevereLogs $ step @EvalLog tds globs t dir j
-                    case sj of
-                      Right (_, BindRename{}) -> success
+                    case (sj, siDetails) of
+                      (Right (_, BindRename{}), _) -> success
+                      (_, PushLetDown{}) -> success
+                      (_, PushLetDownTy{}) -> success
+                      (Right (_, PushLetDown{}), CaseReduction{}) -> success
+                      (Right (_, PushLetDown{}), CaseReductionTrivial{}) -> success
+                      (Right (_, PushLetDown{}), RemoveAnn{}) -> success
+                      (Right (_, PushLetDown{}), LetRemoval{}) -> success
+                      (Right (_, PushLetDownTy{}), TLetRemoval{}) -> success
                       _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog tds globs dir s')
                   else success
diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs
index c98878049..820e21ab0 100644
--- a/primer/test/Tests/EvalFull.hs
+++ b/primer/test/Tests/EvalFull.hs
@@ -2,6 +2,7 @@ module Tests.EvalFull where
 
 import Foreword hiding (unlines)
 
+import Primer.Pretty
 import Data.List ((\\))
 import Data.List.NonEmpty qualified as NE
 import Data.Map qualified as M
@@ -22,6 +23,7 @@ import Primer.App (
  )
 import Primer.Builtins (
   boolDef,
+  cCons,
   cFalse,
   cJust,
   cMakePair,
@@ -43,6 +45,7 @@ import Primer.Core.Utils (
   forgetMetadata,
  )
 import Primer.Def (DefMap)
+import Primer.Eval
 import Primer.EvalFull
 import Primer.Examples qualified as Examples (
   even,
@@ -141,41 +144,37 @@ unit_3 :: Assertion
 unit_3 =
   let ((expr, expected), maxID) = create $ do
         e <- letType "a" (tvar "b") $ emptyHole `ann` (tcon' ["M"] "T" `tapp` tvar "a" `tapp` tforall "a" (KType ()) (tvar "a") `tapp` tforall "b" (KType ()) (tcon' ["M"] "S" `tapp` tvar "a" `tapp` tvar "b"))
-        let b' = "a33" -- NB: fragile name a33
+        let b' = "a42" -- NB: fragile name
         expect <- emptyHole `ann` (tcon' ["M"] "T" `tapp` tvar "b" `tapp` tforall "a" (KType ()) (tvar "a") `tapp` tforall b' (KType ()) (tcon' ["M"] "S" `tapp` tvar "b" `tapp` tvar b'))
         pure (e, expect)
    in do
-        s <- evalFullTest maxID mempty mempty 7 Syn expr
-        s <~==> Right expected
+        s <- evalFullTestExactSteps maxID mempty mempty 12 Syn expr
+        s ~== expected
 
 -- Check we don't have shadowing issues in terms
 unit_4 :: Assertion
 unit_4 =
   let ((expr, expected), maxID) = create $ do
         e <- let_ "a" (lvar "b") $ con' ["M"] "C" [lvar "a", lam "a" (lvar "a"), lam "b" (con' ["M"] "D" [lvar "a", lvar "b"])]
-        let b' = "a19" -- NB: fragile name
+        let b' = "a22" -- NB: fragile name
         expect <- con' ["M"] "C" [lvar "b", lam "a" (lvar "a"), lam b' (con' ["M"] "D" [lvar "b", lvar b'])]
         pure (e, expect)
    in do
-        s <- evalFullTest maxID mempty mempty 7 Syn expr
-        s <~==> Right expected
+        s <- evalFullTestExactSteps maxID mempty mempty 8 Syn expr
+        s ~== expected
 
--- This test is slightly unfortunate for two reasons
--- First, maybe we should do upsilon redexes more aggressively, to avoid the
--- inner annotation in the output; alternatively tweak the reduction rule for
--- letrec so that when inlining, the newly-created letrec does not scope over
--- the newly-created annotation
--- Second, writing [_] for embeddings we don't reduce [ e ] : T (and I'm not
--- sure if we should). This leads to the outer annotation in the output.
+-- This test is slightly unfortunate.
+-- Writing [_] for embeddings we don't reduce [ e ] : T (and I'm not
+-- sure if we should). This leads to the annotation in the output.
 -- See https://github.com/hackworthltd/primer/issues/12
 unit_5 :: Assertion
 unit_5 =
   let ((e, expt), maxID) = create $ do
         a <- letrec "x" (lvar "x") (tcon tBool) (lvar "x")
-        b <- letrec "x" (lvar "x") (tcon tBool) (lvar "x" `ann` tcon tBool) `ann` tcon tBool
+        b <- letrec "x" (lvar "x") (tcon tBool) (lvar "x") `ann` tcon tBool
         pure (a, b)
    in do
-        s <- evalFullTest maxID mempty mempty 100 Syn e
+        s <- evalFullTest maxID mempty mempty 101 Syn e
         s <~==> Left (TimedOut expt)
 
 unit_6 :: Assertion
@@ -215,7 +214,7 @@ unit_8 =
         evalFullTest (maxID e) builtinTypes (defMap e) 500 Syn (expr e) >>= \case
           Left (TimedOut _) -> pure ()
           x -> assertFailure $ show x
-        s <- evalFullTest (maxID e) builtinTypes (defMap e) 1000 Syn (expr e)
+        s <- evalFullTest (maxID e) builtinTypes (defMap e) 2000 Syn (expr e)
         s <~==> Right (expectedResult e)
 
 -- A worker/wrapper'd map
@@ -236,7 +235,7 @@ unit_9 =
         evalFullTest maxID builtinTypes (M.fromList globals) 500 Syn e >>= \case
           Left (TimedOut _) -> pure ()
           x -> assertFailure $ show x
-        s <- evalFullTest maxID builtinTypes (M.fromList globals) 1000 Syn e
+        s <- evalFullTest maxID builtinTypes (M.fromList globals) 2000 Syn e
         s <~==> Right expected
 
 -- A case redex must have an scrutinee which is an annotated constructor.
@@ -265,8 +264,6 @@ unit_10 =
         t' <- evalFullTest maxID builtinTypes mempty 1 Syn t
         t' <~==> Right t
 
--- This example shows that when we are under even a 'let' all we can do is
--- substitute, otherwise we may go down a rabbit hole!
 unit_11 :: Assertion
 unit_11 =
   let modName = mkSimpleModuleName "TestModule"
@@ -285,15 +282,9 @@ unit_11 =
             `ann` (tcon tPair `tapp` tcon tBool `tapp` tcon tNat)
         pure (globs, expr, expect)
    in do
-        evalFullTest maxID builtinTypes (M.fromList globals) 10 Syn e >>= \case
-          Left (TimedOut _) -> pure ()
-          x -> assertFailure $ show x
-        s <- evalFullTest maxID builtinTypes (M.fromList globals) 20 Syn e
-        s <~==> Right expected
+        s <- evalFullTestExactSteps maxID builtinTypes (M.fromList globals) 15 Syn e
+        s ~== expected
 
--- This example shows that we may only substitute the top-most let otherwise we
--- may go down a rabbit hole unrolling a letrec and not doing enough
--- computation to see the recursion should terminate
 unit_12 :: Assertion
 unit_12 =
   let ((e, expected), maxID) = create $ do
@@ -309,8 +300,8 @@ unit_12 =
         expect <- con0 cTrue `ann` tcon tBool
         pure (expr, expect)
    in do
-        s <- evalFullTest maxID builtinTypes mempty 15 Syn e
-        s <~==> Right expected
+        s <- evalFullTestExactSteps maxID builtinTypes mempty 10 Syn e
+        s ~== expected
 
 unit_13 :: Assertion
 unit_13 =
@@ -332,27 +323,26 @@ unit_14 =
         s <- evalFullTest maxID builtinTypes mempty 15 Syn e
         s <~==> Right expected
 
--- Need to swap to substituting an inner let, when it (could have) arises from
--- a renaming to unblock the outer let.
--- i.e. when trying to reduce the let x:
+-- Sometimes we need to rename a binder in order to push a let past it
 --   let x = y in λy.C x y
 --   let x = y in λz. let y = z in C x y
---   let x = y in λz. let y = z in C x z
---   let x = y in λz. C x z
---   let x = y in λz. C y z
---                λz. C y z
+--   λz. let x = y in let y = z in C x y
+--   λz. C (let x = y in x) (let y = z in y)
+--   λz. C y (let y = z in y)
+--   λz. C y z
 unit_15 :: Assertion
 unit_15 =
   let ((expr, steps, expected), maxID) = create $ do
         let l = let_ "x" (lvar "y")
-        let c a b = con' ["M"] "C" [lvar a, lvar b]
-        e0 <- l $ lam "y" $ c "x" "y"
-        let y' = "a38"
-        e1 <- l $ lam y' $ let_ "y" (lvar y') $ c "x" "y"
-        e2 <- l $ lam y' $ let_ "y" (lvar y') $ c "x" y'
-        e3 <- l $ lam y' $ c "x" y'
-        e4 <- l $ lam y' $ c "y" y'
-        e5 <- lam y' $ c "y" y'
+        let c a b = con' ["M"] "C" [a, b]
+        e0 <- l $ lam "y" $ c (lvar "x") (lvar "y")
+        let y' = "a40"
+        let rny = let_ "y" (lvar y')
+        e1 <- l $ lam y' $ rny $ c (lvar "x") (lvar "y")
+        e2 <- lam y' $ l $ rny $ c (lvar "x") (lvar "y")
+        e3 <- lam y' $ c (l $ lvar "x") (rny $ lvar "y")
+        e4 <- lam y' $ c (lvar "y") (rny $ lvar "y")
+        e5 <- lam y' $ c (lvar "y") (lvar y')
         pure (e0, [e0, e1, e2, e3, e4, e5], e5)
    in do
         si <- traverse (\i -> evalFullTest maxID builtinTypes mempty i Syn expr) [0 .. fromIntegral $ length steps - 1]
@@ -367,21 +357,110 @@ unit_hole_ann_case =
         t <- evalFullTest maxID builtinTypes mempty 1 Chk tm
         t @?= Right tm
 
+-- Check we don't have variable capture in
+-- let x = y in case ? of C x -> x ; D y -> x
+unit_case_let_capture :: Assertion
+unit_case_let_capture =
+  let ((expr, steps, expected), maxID) = create $ do
+        let l = let_ "x" (lvar "y")
+        let w = "a66"
+        let z = "a69"
+        let rnx = let_ "x" (lvar w)
+        let rny = let_ "y" (lvar z)
+        e0 <-
+          l $
+            case_
+              emptyHole
+              [ branch' (["M"], "C") [("x", Nothing)] (lvar "x")
+              , branch' (["M"], "D") [("y", Nothing)] (lvar "x")
+              ]
+        e1 <-
+          l $
+            case_
+              emptyHole
+              [ branch' (["M"], "C") [(w, Nothing)] (rnx $ lvar "x")
+              , branch' (["M"], "D") [("y", Nothing)] (lvar "x")
+              ]
+        e2 <-
+          l $
+            case_
+              emptyHole
+              [ branch' (["M"], "C") [(w, Nothing)] (rnx $ lvar "x")
+              , branch' (["M"], "D") [(z, Nothing)] (rny $ lvar "x")
+              ]
+        e3 <-
+          case_
+            emptyHole
+            [ branch' (["M"], "C") [(w, Nothing)] (rnx $ lvar "x")
+            , branch' (["M"], "D") [(z, Nothing)] (l $ rny $ lvar "x")
+            ]
+        e4 <-
+          case_
+            emptyHole
+            [ branch' (["M"], "C") [(w, Nothing)] (lvar w)
+            , branch' (["M"], "D") [(z, Nothing)] (l $ rny $ lvar "x")
+            ]
+        e5 <-
+          case_
+            emptyHole
+            [ branch' (["M"], "C") [(w, Nothing)] (lvar w)
+            , branch' (["M"], "D") [(z, Nothing)] (l $ lvar "x")
+            ]
+        e6 <-
+          case_
+            emptyHole
+            [ branch' (["M"], "C") [(w, Nothing)] (lvar w)
+            , branch' (["M"], "D") [(z, Nothing)] (lvar "y")
+            ]
+        pure (e0, [e0, e1, e2, e3, e4, e5, e6], e6)
+   in do
+        si <- traverse (\i -> evalFullTest maxID builtinTypes mempty i Syn expr) [0 .. fromIntegral $ length steps - 1]
+        zipWithM_ (\s e -> s <~==> Left (TimedOut e)) si steps
+        s <- evalFullTest maxID builtinTypes mempty (fromIntegral $ length steps) Syn expr
+        s <~==> Right expected
+
+-- We must evaluate inside the body of a let before the binding:
+-- consider @let x = ((λy.t : A -> B) r) in letrec xs = s[x] : S in xs@
+-- the two possible reductions are to inline the @letrec@s or to reduce the beta.
+-- We should do the @letrec@ first.
+unit_letrec_body_first :: Assertion
+unit_letrec_body_first =
+  let lx = let_ "x" ((lam "x" (lvar "x") `ann` (tcon tBool `tfun` tcon tBool)) `app` con0 cTrue)
+      lxs =
+        letrec
+          "xs"
+          (con cCons [lvar "x", lvar "xs"])
+          (tcon tList `tapp` tEmptyHole)
+      (expr, maxID) = create $ lx $ lxs (lvar "xs")
+      expected1 = create' $ lx $ lxs $ con cCons [lvar "x", lvar "xs"] `ann` (tcon tList `tapp` tEmptyHole)
+      expected2 = create' $ (lx $ lxs $ con cCons [lvar "x", lvar "xs"]) `ann` (tcon tList `tapp` tEmptyHole)
+      expected3 = create' $ con cCons [lx $ lvar "x", lx $ lxs $ lvar "xs"] `ann` (tcon tList `tapp` tEmptyHole)
+   in do
+        e1 <- evalFullTest maxID builtinTypes mempty 1 Syn expr
+        e1 <~==> Left (TimedOut expected1)
+        e2 <- evalFullTest maxID builtinTypes mempty 2 Syn expr
+        e2 <~==> Left (TimedOut expected2)
+        e3 <- evalFullTest maxID builtinTypes mempty 3 Syn expr
+        e3 <~==> Left (TimedOut expected3)
+
 -- tlet x = C in D x x
 --   ==>
--- tlet x = C in D C x
+-- (tlet x = C in D x) (tlet x = C in x)
+--   ==>
+-- D (tlet x = C in x) (tlet x = C in x)
 --   ==>
--- tlet x = C in D C C
+-- D C (tlet x = C in x)
 --   ==>
 -- D C C
 unit_tlet :: Assertion
 unit_tlet =
   let ((expr, expected), maxID) = create $ do
         e0 <- ann emptyHole $ tlet "x" (tcon' ["M"] "C") (tcon' ["M"] "D" `tapp` tvar "x" `tapp` tvar "x")
-        e1 <- ann emptyHole $ tlet "x" (tcon' ["M"] "C") (tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tvar "x")
-        e2 <- ann emptyHole $ tlet "x" (tcon' ["M"] "C") (tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tcon' ["M"] "C")
-        e3 <- ann emptyHole $ tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tcon' ["M"] "C"
-        pure (e0, map (Left . TimedOut) [e0, e1, e2, e3] ++ [Right e3])
+        e1 <- ann emptyHole $ tlet "x" (tcon' ["M"] "C") (tcon' ["M"] "D" `tapp` tvar "x") `tapp` tlet "x" (tcon' ["M"] "C") (tvar "x")
+        e2 <- ann emptyHole $ tcon' ["M"] "D" `tapp` tlet "x" (tcon' ["M"] "C") (tvar "x") `tapp` tlet "x" (tcon' ["M"] "C") (tvar "x")
+        e3 <- ann emptyHole $ tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tlet "x" (tcon' ["M"] "C") (tvar "x")
+        e4 <- ann emptyHole $ tcon' ["M"] "D" `tapp` tcon' ["M"] "C" `tapp` tcon' ["M"] "C"
+        pure (e0, map (Left . TimedOut) [e0, e1, e2, e3, e4] ++ [Right e4])
       test (n, expect) = do
         r <- evalFullTest maxID mempty mempty n Syn expr
         r <~==> expect
@@ -400,27 +479,13 @@ unit_tlet_elide = do
    in mapM_ test (zip [0 ..] expected)
 
 -- tlet x = x in x
---   ==>
--- tlet y = x in let x = y in x
---   ==>
--- tlet y = x in let x = y in y
---   ==>
--- tlet y = x in y
---   ==>
--- tlet y = x in x
---   ==>
 -- x
 unit_tlet_self_capture :: Assertion
 unit_tlet_self_capture = do
-  let y = "a32"
-      ((expr, expected), maxID) = create $ do
+  let ((expr, expected), maxID) = create $ do
         e0 <- ann emptyHole $ tlet "x" (tvar "x") $ tvar "x"
-        e1 <- ann emptyHole $ tlet y (tvar "x") $ tlet "x" (tvar y) $ tvar "x"
-        e2 <- ann emptyHole $ tlet y (tvar "x") $ tlet "x" (tvar y) $ tvar y
-        e3 <- ann emptyHole $ tlet y (tvar "x") $ tvar y
-        e4 <- ann emptyHole $ tlet y (tvar "x") $ tvar "x"
-        e5 <- ann emptyHole $ tvar "x"
-        pure (e0, map (Left . TimedOut) [e0, e1, e2, e3, e4, e5] ++ [Right e5])
+        e1 <- ann emptyHole $ tvar "x"
+        pure (e0, map (Left . TimedOut) [e0, e1] ++ [Right e1])
       test (n, expect) = do
         r <- evalFullTest maxID mempty mempty n Syn expr
         r <~==> expect
@@ -443,6 +508,8 @@ tasty_resume = withDiscards 2000 $
 -- A helper for tasty_resume, and tasty_resume_regression
 resumeTest :: [Module] -> Dir -> Expr -> PropertyT WT ()
 resumeTest mods dir t = do
+  let optsV = ViewRedexOptions { pushMulti = True , aggressiveElision = True }
+  let optsR = RunRedexOptions { pushAndElide = True }
   let globs = foldMap' moduleDefsQualified mods
   tds <- asks typeDefs
   n <- forAllT $ Gen.integral $ Range.linear 2 1000 -- Arbitrary limit here
@@ -453,19 +520,19 @@ resumeTest mods dir t = do
   -- exactly the same as "reducing n steps and then further reducing m
   -- steps" (including generated names). (A happy consequence of this is that
   -- it is precisely the same including ids in metadata.)
-  ((stepsFinal', sFinal), logs) <- lift $ isolateWT $ runPureLogT $ evalFullStepCount @EvalLog tds globs n dir t
+  ((stepsFinal', sFinal), logs) <- lift $ isolateWT $ runPureLogT $ evalFullStepCount @EvalLog optsV optsR tds globs n dir t
   testNoSevereLogs logs
   when (stepsFinal' < 2) discard
   let stepsFinal = case sFinal of Left _ -> stepsFinal'; Right _ -> 1 + stepsFinal'
   m <- forAllT $ Gen.integral $ Range.constant 1 (stepsFinal - 1)
-  (stepsMid, sMid') <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs m dir t
+  (stepsMid, sMid') <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs m dir t
   stepsMid === m
   sMid <- case sMid' of
     Left (TimedOut e) -> pure e
     -- This should never happen: we know we are not taking enough steps to
     -- hit a normal form (as m < stepsFinal)
     Right e -> assert False >> pure e
-  (stepsTotal, sTotal) <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs (stepsFinal - m) dir sMid
+  (stepsTotal, sTotal) <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs (stepsFinal - m) dir sMid
   stepsMid + stepsTotal === stepsFinal'
   sFinal === sTotal
 
@@ -594,34 +661,63 @@ unit_type_preservation_BETA_regression =
                 `app` lvar "x"
         -- NB: the point of the ... `app` lvar x is to make the annotated term be in SYN position
         -- so we reduce the type, rather than taking an upsilon step
-        -- Rename the let b
-        -- Λb. λx. ((lettype a = b Bool in λc (? : a)) : (let c = b Bool in let b = c in Nat -> b)) x
-        let b' = "a132"
+        -- Push the let b
+        -- Λb. λx. ((lettype a = b Bool in λc (? : a)) : (Nat -> (let b = b Bool in b))) x
         expectA2 <-
           lAM "b" $
             lam "x" $
               ( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a")
-                  `ann` tlet b' (tvar "b" `tapp` tcon tBool) (tlet "b" (tvar b') $ tcon tNat `tfun` tvar "b")
+                  `ann` (tcon tNat `tfun` tlet "b" (tvar "b" `tapp` tcon tBool) (tvar "b"))
               )
                 `app` lvar "x"
-        -- Resolve the renaming
-        -- Λb. λx. ((lettype a = b Bool in λc (? : a)) : (let c = b Bool in Nat -> c)) x
-        expectA4 <-
+        -- Inline the let
+        -- Λb. λx. ((lettype a = b Bool in λc (? : a)) : (Nat -> b Bool)) x
+        expectA3 <-
           lAM "b" $
             lam "x" $
               ( letType "a" (tvar "b" `tapp` tcon tBool) (lam "c" $ emptyHole `ann` tvar "a")
-                  `ann` tlet b' (tvar "b" `tapp` tcon tBool) (tcon tNat `tfun` tvar b')
+                  `ann` (tcon tNat `tfun` (tvar "b" `tapp` tcon tBool))
               )
                 `app` lvar "x"
-        -- Resolve all the letTypes
-        -- Λb. λx. ((λc (? : b Bool)) : (Nat -> b Bool)) x
-        expectA8 <-
+        -- Push the let
+        -- Λb. λx. (λc (lettype a = b Bool in (? : a)) : (Nat -> b Bool)) x
+        expectA4 <-
           lAM "b" $
             lam "x" $
-              ( lam "c" (emptyHole `ann` (tvar "b" `tapp` tcon tBool))
+              ( lam "c" (letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a"))
                   `ann` (tcon tNat `tfun` (tvar "b" `tapp` tcon tBool))
               )
                 `app` lvar "x"
+        -- Do the beta step
+        -- Λb. λx. (let c = (x : Nat) in (lettype a = b Bool in (? : a)) : (b Bool))
+        expectA5 <-
+          lAM "b" $
+            lam "x" $
+              let_ "c" (lvar "x" `ann` tcon tNat) (letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a"))
+                `ann` (tvar "b" `tapp` tcon tBool)
+        -- Elide a pointless let
+        -- Λb. λx. ((lettype a = b Bool in (? : a)) : (b Bool))
+        expectA6 <-
+          lAM "b" $
+            lam "x" $
+              letType "a" (tvar "b" `tapp` tcon tBool) (emptyHole `ann` tvar "a")
+                `ann` (tvar "b" `tapp` tcon tBool)
+        -- Push the lets, eliding those that are redundant
+        -- Λb. λx. ((? : lettype a = b Bool in a) : (b Bool))
+        expectA7 <-
+          lAM "b" $
+            lam "x" $
+              emptyHole
+                `ann` tlet "a" (tvar "b" `tapp` tcon tBool) (tvar "a")
+                `ann` (tvar "b" `tapp` tcon tBool)
+        -- Inline a let
+        -- Λb. λx. ((? : b Bool) : (b Bool))
+        expectA8 <-
+          lAM "b" $
+            lam "x" $
+              emptyHole
+                `ann` (tvar "b" `tapp` tcon tBool)
+                `ann` (tvar "b" `tapp` tcon tBool)
         -- The 'B' sequence previously captured in the term "t" above
         -- Λb. (Λa (foo @(b Bool) : ∀b.Nat) @Char
         eB <-
@@ -636,7 +732,7 @@ unit_type_preservation_BETA_regression =
           lAM "b" $
             letType "a" (tcon tChar) (gvar foo `aPP` (tvar "b" `tapp` tcon tBool))
               `ann` tlet "b" (tcon tChar) (tcon tNat)
-        -- Drop annotation and elide lettype
+        -- Drop annotation, elide lettype
         -- Λb. foo @(b Bool)
         expectB3 <- lAM "b" $ gvar foo `aPP` (tvar "b" `tapp` tcon tBool)
         -- Note that the reduction of eA and eB take slightly
@@ -644,7 +740,19 @@ unit_type_preservation_BETA_regression =
         -- because it has an occurrence of a type variable and is thus
         -- not "concrete"
         pure
-          ( (eA, [(1, expectA1), (2, expectA2), (4, expectA4), (8, expectA8)])
+          (
+            ( eA
+            ,
+              [ (1, expectA1)
+              , (2, expectA2)
+              , (3, expectA3)
+              , (4, expectA4)
+              , (5, expectA5)
+              , (6, expectA6)
+              , (7, expectA7)
+              , (8, expectA8)
+              ]
+            )
           , (eB, [(1, expectB1), (3, expectB3)])
           )
       sA n = evalFullTest maxID builtinTypes mempty n Chk exprA
@@ -672,29 +780,29 @@ unit_type_preservation_BETA_regression =
 -- 'let x' has captured the reference to the x in the bound term.
 -- This causes the term to become ill-sorted.
 -- Similarly, we reduce 'λx. let x = x in x' to itself, due to the same capture.
+-- (This was before we changed to "pushing down lets")
 unit_let_self_capture :: Assertion
 unit_let_self_capture =
   let ( ( expr1
           , ty1
           , expr2
-          , expected2a
-          , expected2b
+          , expected2
           , expr3
           , expected3a
           , expected3b
           , expr4
           , expected4a
           , expected4b
+          , expected4c
           )
         , maxID
         ) = create $ do
           e1 <- lAM "x" $ let_ "x" (emptyHole `ann` tvar "x") (lvar "x")
           let t1 = TForall () "a" (KType ()) $ TVar () "a"
           e2 <- lam "x" $ let_ "x" (lvar "x") (lvar "x")
-          expect2a <- lam "x" $ let_ "a76" (lvar "x") (let_ "x" (lvar "a76") (lvar "x"))
-          expect2b <- lam "x" $ lvar "x"
+          expect2 <- lam "x" $ lvar "x"
           e3 <- lAM "x" $ letType "x" (tvar "x") (emptyHole `ann` tvar "x")
-          expect3a <- lAM "x" $ letType "a76" (tvar "x") (letType "x" (tvar "a76") (emptyHole `ann` tvar "x"))
+          expect3a <- lAM "x" $ emptyHole `ann` tlet "x" (tvar "x") (tvar "x")
           expect3b <- lAM "x" $ emptyHole `ann` tvar "x"
           -- We do not need to do anything special for letrec
           e4 <- lAM "a" $ lam "f" $ lam "x" $ letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "x")
@@ -703,28 +811,29 @@ unit_let_self_capture =
               lam "f" $
                 lam "x" $
                   letrec "x" (lvar "f" `app` lvar "x") (tvar "a") $
-                    letrec "x" (lvar "f" `app` lvar "x") (tvar "a") ((lvar "f" `app` lvar "x") `ann` tvar "a")
+                    (lvar "f" `app` lvar "x") `ann` tvar "a"
           expect4b <-
             lAM "a" $
               lam "f" $
                 lam "x" $
-                  letrec
-                    "x"
-                    (lvar "f" `app` lvar "x")
-                    (tvar "a")
-                    ((lvar "f" `app` lvar "x") `ann` tvar "a")
+                  letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "f" `app` lvar "x") `ann` tvar "a"
+          expect4c <-
+            lAM "a" $
+              lam "f" $
+                lam "x" $
+                  (lvar "f" `app` letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "x")) `ann` tvar "a"
           pure
             ( e1
             , t1
             , e2
-            , expect2a
-            , expect2b
+            , expect2
             , e3
             , expect3a
             , expect3b
             , e4
             , expect4a
             , expect4b
+            , expect4c
             )
       s1 n = evalFullTest maxID mempty mempty n Chk expr1
       s2 n = evalFullTest maxID mempty mempty n Chk expr2
@@ -741,14 +850,14 @@ unit_let_self_capture =
                 Right _ -> pure ()
    in do
         typePres ty1 s1
-        s2 1 >>= (<~==> Left (TimedOut expected2a))
-        s2 5 >>= (<~==> Left (TimedOut expected2b))
-        s2 6 >>= (<~==> Right expected2b)
+        s2 1 >>= (<~==> Left (TimedOut expected2))
+        s2 2 >>= (<~==> Right expected2)
         s3 1 >>= (<~==> Left (TimedOut expected3a))
-        s3 5 >>= (<~==> Left (TimedOut expected3b))
-        s3 6 >>= (<~==> Right expected3b)
+        s3 2 >>= (<~==> Left (TimedOut expected3b))
+        s3 3 >>= (<~==> Right expected3b)
         s4 1 >>= (<~==> Left (TimedOut expected4a))
         s4 2 >>= (<~==> Left (TimedOut expected4b))
+        s4 3 >>= (<~==> Left (TimedOut expected4c))
 
 -- | @spanM p mxs@ returns a tuple where the first component is the
 -- values coming from the longest prefix of @mxs@ all of which satisfy
@@ -777,6 +886,7 @@ spanM f (x : xs) = do
 -- Λy. let x = ?:y in let y = _:y in y x
 -- reducing it to
 -- Λy. let x = ?:y in let y = _:y in (_:y) x
+-- (This was before we changed to "pushing down lets")
 unit_regression_self_capture_let_let :: Assertion
 unit_regression_self_capture_let_let = do
   let e =
@@ -784,18 +894,27 @@ unit_regression_self_capture_let_let = do
           let_ "x" (emptyHole `ann` tvar "y") $
             let_ "y" (emptyHole `ann` tvar "y") $
               lvar "y" `app` lvar "x"
-      z = "a12"
       f =
         lAM "y" $
-          let_ "x" (emptyHole `ann` tvar "y") $
-            let_ z (emptyHole `ann` tvar "y") $
-              let_ "y" (lvar z) $
-                lvar "y" `app` lvar "x"
+          (             let_ "y" (emptyHole `ann` tvar "y") $
+                lvar "y"
+            )
+            `app`  
+          (let_
+            "x"
+            (emptyHole `ann` tvar "y") $
+                  lvar "x"
+              )
+      g =
+        lAM "y" $
+          (emptyHole `ann` tvar "y")
+            `app` (emptyHole `ann` tvar "y") 
       (e', i) = create e
       ev n = evalFullTest i mempty mempty n Chk e'
       x ~ y = x >>= (<~==> Left (TimedOut (create' y)))
   ev 0 ~ e
   ev 1 ~ f
+  ev 3 ~ g
 
 -- | Evaluation preserves types
 -- (assuming we don't end with a 'LetType' in the term, as the typechecker
@@ -804,6 +923,8 @@ tasty_type_preservation :: Property
 tasty_type_preservation = withTests 1000 $
   withDiscards 2000 $
     propertyWT testModules $ do
+      let optsV = ViewRedexOptions { pushMulti = True , aggressiveElision = True }
+      let optsR = RunRedexOptions { pushAndElide = True }
       let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
       tds <- asks typeDefs
       (dir, t, ty) <- genDirTm
@@ -820,7 +941,7 @@ tasty_type_preservation = withTests 1000 $
                 s' <- checkTest ty s
                 forgetMetadata s === forgetMetadata s' -- check no smart holes happened
       maxSteps <- forAllT $ Gen.integral $ Range.linear 1 1000 -- Arbitrary limit here
-      (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs maxSteps dir t
+      (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs maxSteps dir t
       annotateShow steps
       annotateShow s
       -- s is often reduced to normal form
@@ -830,7 +951,7 @@ tasty_type_preservation = withTests 1000 $
         then label "generated a normal form"
         else do
           midSteps <- forAllT $ Gen.integral $ Range.linear 1 (steps - 1)
-          (_, s') <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs midSteps dir t
+          (_, s') <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsV optsR tds globs midSteps dir t
           test "mid " s'
 
 -- Unsaturated primitives are stuck terms
@@ -1270,8 +1391,17 @@ unit_prim_partial_map =
             <*> pure (M.singleton mapName mapDef)
             <*> primDefs
    in do
-        s <- evalFullTest maxID builtinTypes (gs <> prims) 67 Syn e
-        s <~==> Right r
+        s <- evalFullTestExactSteps maxID builtinTypes (gs <> prims) 91 Syn e
+        s ~== r
+
+-- TODO/REVIEW:
+-- I NEED TO WRITE A [note] about this!
+-- note that ww/map is somewhat pointless when push down lets -- maybe we should push lets inside letrecs (maybe just inside type?)?
+-- note that ww/map is somewhat pointless when push down lets -- maybe we should push lets inside letrecs (maybe just inside type?)?
+--     nb, get something like @let α=Char, β=Char, f=toUpper in (letrec go : List α -> List β; go = λxs.RHS in go)@
+--     and then in two steps (expand @go@, push stack of let+letrec)
+--        @λxs. let α=Char, β=Char, f=toUpper in (letrec go : List α -> List β; go = λxs.RHS in RHS : List α -> List β)@
+--     we carry around the subst for α,β and f, using α,β inside annotation and f in RHS each time expand the letrec
 
 -- Test that handleEvalFullRequest will reduce imported terms
 unit_eval_full_modules :: Assertion
@@ -1335,13 +1465,15 @@ tasty_unique_ids :: Property
 tasty_unique_ids = withTests 1000 $
   withDiscards 2000 $
     propertyWT testModules $ do
+      let optsV = ViewRedexOptions { pushMulti = True , aggressiveElision = True }
+      let optsR = RunRedexOptions { pushAndElide = True }
       let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
       tds <- asks typeDefs
       (dir, t1, _) <- genDirTm
       let go n t
             | n == (0 :: Int) = pure ()
             | otherwise = do
-                t' <- failWhenSevereLogs $ evalFull @EvalLog tds globs 1 dir t
+                t' <- failWhenSevereLogs $ evalFull @EvalLog optsV optsR tds globs 1 dir t
                 case t' of
                   Left (TimedOut e) -> uniqueIDs e >> go (n - 1) e
                   Right e -> uniqueIDs e
@@ -1357,11 +1489,10 @@ unit_wildcard =
       (eTerm, maxIDTerm) = create $ caseFB_ loop [] (con0 cTrue)
       expectTerm = create' $ con0 cTrue
       (eDiverge, maxIDDiverge) = create $ caseFB_ loop [branch cZero [] $ con0 cFalse] (con0 cTrue)
-      -- This has an annotation within the body of the letrec for the same reason as unit_5
       expectDiverge =
         create' $
           caseFB_
-            ( letrec "x" (lvar "x") (tcon tNat) (lvar "x" `ann` tcon tNat)
+            ( letrec "x" (lvar "x") (tcon tNat) (lvar "x")
                 `ann` tcon tNat
             )
             [branch cZero [] $ con0 cFalse]
@@ -1369,7 +1500,7 @@ unit_wildcard =
    in do
         s <- evalFullTest maxIDTerm mempty mempty 2 Syn eTerm
         s <~==> Right expectTerm
-        t <- evalFullTest maxIDDiverge mempty mempty 22 Syn eDiverge
+        t <- evalFullTest maxIDDiverge mempty mempty 5 Syn eDiverge
         t <~==> Left (TimedOut expectDiverge)
 
 unit_case_prim :: Assertion
@@ -1406,18 +1537,75 @@ unit_case_prim =
         s4 <- evalFullTest maxID4 mempty mempty 6 Syn e4
         s4 <~==> Right expect4
 
+-- TODO/REVIEW: remove me!
+tmp :: Bool -> Assertion
+tmp ae =
+  let modName = mkSimpleModuleName "TestModule"
+      ((e, r, gs, prims), maxID) =
+        create $ do
+          (mapName, mapDef) <- Examples.map' modName
+          (,,,)
+            <$> gvar mapName
+            `aPP` tcon tChar
+            `aPP` tcon tChar
+            `app` pfun ToUpper
+            `app` list_
+              [ char 'a'
+              , char 'b'
+              , char 'c'
+              ]
+            <*> list_
+              [ char 'A'
+              , char 'B'
+              , char 'C'
+              ]
+            `ann` (tcon tList `tapp` tcon tChar)
+            <*> pure (M.singleton mapName mapDef)
+            <*> primDefs
+      evalFullTest' :: ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr)
+      evalFullTest' id_ tydefs globals n d e = do
+        let optsV = ViewRedexOptions { pushMulti = True, aggressiveElision = ae}
+        let optsR = RunRedexOptions { }
+        let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsV optsR tydefs globals n d e
+        assertNoSevereLogs logs
+        distinctIDs r
+        pure r
+   in for_ @[] [0..] $ \n -> do
+        s <- evalFullTest' maxID builtinTypes (gs <> prims) n Syn e
+        case s of
+            Left (TimedOut t) -> prettyPrintExpr compact t
+            Right t -> putStrLn @Text "\n\n NORMAL FORM \n\n" >> prettyPrintExpr compact t
+        putStrLn @Text $ "\n\nn=" <> show n
+        putStrLn @Text "------------------\n\n"
+        getLine
+
 -- * Utilities
 
-evalFullTest :: ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr)
+evalFullTest :: HasCallStack => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr)
 evalFullTest id_ tydefs globals n d e = do
-  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog tydefs globals n d e
+  let optsV = ViewRedexOptions { pushMulti = True , aggressiveElision = True }
+  let optsR = RunRedexOptions { pushAndElide = True }
+  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsV optsR tydefs globals n d e
   assertNoSevereLogs logs
   distinctIDs r
   pure r
 
+evalFullTestExactSteps :: HasCallStack => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO Expr
+evalFullTestExactSteps id_ tydefs globals n d e = do
+    s <- evalFullTest id_ tydefs globals (n-1) d e
+    case s of
+        Right s' -> assertFailure $ "Unexpectedly reached normal form: " <> show s'
+        Left _ -> do
+          t <- evalFullTest id_ tydefs globals n d e
+          case t of
+              Left t' -> assertFailure $ "Unexpected timeout: " <> show t'
+              Right t' -> pure t'
+
 evalFullTasty :: MonadTest m => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr)
 evalFullTasty id_ tydefs globals n d e = do
-  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog tydefs globals n d e
+  let optsV = ViewRedexOptions { pushMulti = True , aggressiveElision = True }
+  let optsR = RunRedexOptions { pushAndElide = True }
+  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsV optsR tydefs globals n d e
   testNoSevereLogs logs
   let ids = r ^.. evalResultExpr % exprIDs
   ids === ordNub ids
@@ -1457,6 +1645,9 @@ evalResultExpr = _Left % timedOut `adjoin` _Right
 (<~==>) :: HasCallStack => Either EvalFullError Expr -> Either EvalFullError Expr -> Assertion
 x <~==> y = on (@?=) (over evalResultExpr zeroIDs) x y
 
+(~==) :: HasCallStack => Expr -> Expr -> Assertion
+x ~== y = on (@?=) zeroIDs x y
+
 distinctIDs :: Either EvalFullError Expr -> Assertion
 distinctIDs e =
   let ids = e ^.. evalResultExpr % exprIDs
diff --git a/primer/test/Tests/Prelude/Integer.hs b/primer/test/Tests/Prelude/Integer.hs
index bdffa9c0d..df975abf3 100644
--- a/primer/test/Tests/Prelude/Integer.hs
+++ b/primer/test/Tests/Prelude/Integer.hs
@@ -37,7 +37,7 @@ tasty_negate_prop = property $ do
 tasty_abs_prop :: Property
 tasty_abs_prop = property $ do
   n <- forAll $ G.integral_ (Range.constant (-10) 10)
-  functionOutput P.abs [int n] 40 <===> Right (create' $ int $ abs n)
+  functionOutput P.abs [int n] 45 <===> Right (create' $ int $ abs n)
 
 -- NOTE: Termination bound is experimental, do not know how it varies with n, m
 tasty_gcd_prop :: Property
@@ -61,7 +61,7 @@ tasty_even_prop = property $ do
 tasty_odd_prop :: Property
 tasty_odd_prop = property $ do
   n <- forAll $ G.integral_ (Range.constant (-10) 10)
-  functionOutput P.odd [int n] 20 <===> Right (create' $ bool_ $ odd n)
+  functionOutput P.odd [int n] 25 <===> Right (create' $ bool_ $ odd n)
 
 tasty_sum_prop :: Property
 tasty_sum_prop = property $ do
diff --git a/primer/test/Tests/Prelude/Polymorphism.hs b/primer/test/Tests/Prelude/Polymorphism.hs
index bf444e1c1..552c49048 100644
--- a/primer/test/Tests/Prelude/Polymorphism.hs
+++ b/primer/test/Tests/Prelude/Polymorphism.hs
@@ -63,7 +63,7 @@ tasty_const_prop = property $ do
     , Right $ tcon tBool
     , Left $ bool_ True
     ]
-    20
+    21
     <===> Right (create' $ int n)
   functionOutput' -- Bool Test
     P.const
@@ -72,7 +72,7 @@ tasty_const_prop = property $ do
     , Right $ tcon tInt
     , Left $ int n
     ]
-    20
+    21
     <===> Right (create' $ bool_ b)
   functionOutput' -- List of Int Test
     P.const
@@ -81,7 +81,7 @@ tasty_const_prop = property $ do
     , Right $ tcon tInt
     , Left $ int n
     ]
-    20
+    21
     <===> Right (create' $ list_ $ map int ns)
 
 tasty_map_prop :: Property
diff --git a/primer/test/Tests/Prelude/Utils.hs b/primer/test/Tests/Prelude/Utils.hs
index 752bd0d2f..01811477b 100644
--- a/primer/test/Tests/Prelude/Utils.hs
+++ b/primer/test/Tests/Prelude/Utils.hs
@@ -7,6 +7,8 @@ import Hedgehog.Internal.Property
 import Optics (over)
 import Primer.Core (Expr, GVarName, Type)
 import Primer.Core.DSL (apps', create', gvar)
+import Primer.Eval (RunRedexOptions (RunRedexOptions),
+    ViewRedexOptions(ViewRedexOptions,aggressiveElision, pushMulti))
 import Primer.EvalFull (Dir (Chk), EvalFullError, EvalLog, TerminationBound, evalFull)
 import Primer.Log (runPureLogT)
 import Primer.Module (builtinModule, moduleDefsQualified, moduleTypesQualified, primitiveModule)
@@ -49,9 +51,11 @@ functionOutput f args = functionOutput' f (map Left args)
 -- Tests a prelude function with a combination of Expr/Type arguments to be applied
 functionOutput' :: GVarName -> [Either (TestM Expr) (TestM Type)] -> TerminationBound -> Either EvalFullError Expr
 functionOutput' f args depth =
-  let (r, logs) = evalTestM 0 $ runPureLogT $ do
+  let optsV = ViewRedexOptions {pushMulti = True, aggressiveElision = True}
+      optsR = RunRedexOptions {}
+      (r, logs) = evalTestM 0 $ runPureLogT $ do
         e <- apps' (gvar f) $ bimap lift lift <$> args
-        evalFull @EvalLog ty def n d e
+        evalFull @EvalLog optsV optsR ty def n d e
       severe = Seq.filter isSevereLog logs
    in if null severe
         then r
diff --git a/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi b/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi
index a9d43dcc9..a88a3741b 100644
--- a/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi	
+++ b/primer/test/outputs/Pretty/comprehensive/Expr (Compact).ansi	
@@ -1,44 +1,27 @@
-let x = (True) :: (Bool) in
-  let rec y =
-    (
-      (
-        {?(Just (?)) :: ((Maybe) (?))?}
-      )
-      (
-        {?unboundName?}
-      )
-    ) ::
-    (
-      {?Maybe?}
-    )
-  in
-    (
-      λi.
-        Λβ.
-          (
-            (
-              let type b = Bool in
-                Left
-            ) @β
-          )
-          (
-            match i with
-              Zero   → False
-              Succ n → match n with
-                Zero → (
-                  (
-                    ?
-                  )
-                  (
-                    x
-                  )
-                )
-                (
-                  y
-                )
-                _    → ?
-          )
-    ) ::
-    (
-      Nat -> ∀ α. ((Either) (Bool)) (α)
-    )
+let x = True :: Bool in
+  (
+    let rec y = (({?(Just ?) :: (Maybe ?)?}) unboundName) :: Maybe in
+      (
+        (
+          λi.
+            Λβ.
+              (
+                (
+                  let type b = Bool in
+                    Left
+                ) @β
+              )
+              (
+                match i with
+                  Zero   → False
+                  Succ n → match n with
+                    Zero → (
+                      ?
+                      x
+                    )
+                    y
+                    _    → ?
+              )
+        ) :: (Nat -> ∀ α. (Either Bool) α)
+      )
+  )
diff --git a/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi b/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi
index 3dc91420d..bca91e299 100644
--- a/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi	
+++ b/primer/test/outputs/Pretty/comprehensive/Expr (Sparse).ansi	
@@ -1,83 +1,57 @@
 let x =
-  (
-    True
-  ) ::
-  (
-    Bool
-  )
+  True ::
+  Bool
 in
-  let rec y =
-    (
-      (
-        {?
-          (
-            Just
-            (
+  (
+    let rec y =
+      (
+        (
+          {?
+            (
+              Just
               ?
-            )
-          ) ::
-          (
-            (
+            ) ::
+            (
               Maybe
-            )
-            (
               ?
-            )
-          )
-        ?}
-      )
-      (
-        {?
-          unboundName
-        ?}
-      )
-    ) ::
-    (
-      {?
-        Maybe
-      ?}
-    )
-  in
-    (
-      λi.
-        Λβ.
-          (
-            (
-              let type b =
-                Bool
-              in
-                Left
-            ) @β
-          )
-          (
-            match i with
-              Zero   → False
-              Succ n → match n with
-                Zero → (
-                  (
-                    ?
-                  )
-                  (
-                    x
-                  )
-                )
-                (
-                  y
-                )
-                _    → ?
-          )
-    ) ::
-    (
-      Nat -> ∀ α.
-        (
-          (
-            Either
-          )
-          (
-            Bool
-          )
-        )
-        (
-          α
-        )
-    )
+            )
+          ?}
+        )
+        unboundName
+      ) ::
+      Maybe
+    in
+      (
+        (
+          λi.
+            Λβ.
+              (
+                (
+                  let type b =
+                    Bool
+                  in
+                    Left
+                ) @β
+              )
+              (
+                match i with
+                  Zero   → False
+                  Succ n → match n with
+                    Zero → (
+                      ?
+                      x
+                    )
+                    y
+                    _    → ?
+              )
+        ) ::
+        (
+          Nat -> ∀ α.
+            (
+              Either
+              Bool
+            )
+            α
+        )
+      )
+  )
diff --git a/primer/test/outputs/Pretty/comprehensive/Type (Compact).ansi b/primer/test/outputs/Pretty/comprehensive/Type (Compact).ansi
index 5c8a9cf03..9776b5749 100644
--- a/primer/test/outputs/Pretty/comprehensive/Type (Compact).ansi	
+++ b/primer/test/outputs/Pretty/comprehensive/Type (Compact).ansi	
@@ -1 +1 @@
-Nat -> ∀ a. ({?(List) (?)?}) (a)
+Nat -> ∀ a. ({?List ??}) a
diff --git a/primer/test/outputs/Pretty/comprehensive/Type (Sparse).ansi b/primer/test/outputs/Pretty/comprehensive/Type (Sparse).ansi
index 3b4f7ce2f..46a5db3e9 100644
--- a/primer/test/outputs/Pretty/comprehensive/Type (Sparse).ansi	
+++ b/primer/test/outputs/Pretty/comprehensive/Type (Sparse).ansi	
@@ -1,14 +1,8 @@
 Nat -> ∀ a.
-  (
+  (
     {?
-      (
-        List
-      )
-      (
-        ?
-      )
+      List
+      ?
     ?}
-  )
-  (
-    a
-  )
+  )
+  a