diff --git a/src/Lean/Compiler/LCNF.lean b/src/Lean/Compiler/LCNF.lean
index bf6a741f8f..6ea7070704 100644
--- a/src/Lean/Compiler/LCNF.lean
+++ b/src/Lean/Compiler/LCNF.lean
@@ -45,3 +45,4 @@ public import Lean.Compiler.LCNF.LambdaLifting
 public import Lean.Compiler.LCNF.ReduceArity
 public import Lean.Compiler.LCNF.Probing
 public import Lean.Compiler.LCNF.Irrelevant
+public import Lean.Compiler.LCNF.SplitSCC
diff --git a/src/Lean/Compiler/LCNF/Check.lean b/src/Lean/Compiler/LCNF/Check.lean
index 5997ad5638..cc17d990a5 100644
--- a/src/Lean/Compiler/LCNF/Check.lean
+++ b/src/Lean/Compiler/LCNF/Check.lean
@@ -258,45 +258,4 @@ end Check
 def Decl.check (decl : Decl) : CompilerM Unit := do
   Check.run do decl.value.forCodeM (Check.checkFunDeclCore decl.name decl.params decl.type)
 
-/--
-Check whether every local declaration in the local context is used in one of given `decls`.
--/
-partial def checkDeadLocalDecls (decls : Array Decl) : CompilerM Unit := do
-  let (_, s) := visitDecls decls |>.run {}
-  let usesFVar (binderName : Name) (fvarId : FVarId) :=
-    unless s.contains fvarId do
-      throwError "LCNF local context contains unused local variable declaration `{binderName}`"
-  let lctx := (← get).lctx
-  lctx.params.forM fun fvarId decl => usesFVar decl.binderName fvarId
-  lctx.letDecls.forM fun fvarId decl => usesFVar decl.binderName fvarId
-  lctx.funDecls.forM fun fvarId decl => usesFVar decl.binderName fvarId
-where
-  visitFVar (fvarId : FVarId) : StateM FVarIdHashSet Unit :=
-    modify (·.insert fvarId)
-
-  visitParam (param : Param) : StateM FVarIdHashSet Unit := do
-    visitFVar param.fvarId
-
-  visitParams (params : Array Param) : StateM FVarIdHashSet Unit := do
-    params.forM visitParam
-
-  visitCode (code : Code) : StateM FVarIdHashSet Unit := do
-    match code with
-    | .jmp .. | .return .. | .unreach .. => return ()
-    | .let decl k => visitFVar decl.fvarId; visitCode k
-    | .fun decl k | .jp decl k =>
-      visitFVar decl.fvarId; visitParams decl.params; visitCode decl.value
-      visitCode k
-    | .cases c => c.alts.forM fun alt => do
-      match alt with
-      | .default k => visitCode k
-      | .alt _ ps k => visitParams ps; visitCode k
-
-  visitDecl (decl : Decl) : StateM FVarIdHashSet Unit := do
-    visitParams decl.params
-    decl.value.forCodeM visitCode
-
-  visitDecls (decls : Array Decl) : StateM FVarIdHashSet Unit :=
-    decls.forM visitDecl
-
 end Lean.Compiler.LCNF
diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean
index 8c88c81ea2..52824870e1 100644
--- a/src/Lean/Compiler/LCNF/Main.lean
+++ b/src/Lean/Compiler/LCNF/Main.lean
@@ -11,6 +11,7 @@ public import Lean.Compiler.LCNF.Passes
 public import Lean.Compiler.LCNF.ToDecl
 public import Lean.Compiler.LCNF.Check
 import Lean.Meta.Match.MatcherInfo
+import Lean.Compiler.LCNF.SplitSCC
 public section
 namespace Lean.Compiler.LCNF
 /--
@@ -56,8 +57,6 @@ def checkpoint (stepName : Name) (decls : Array Decl) (shouldCheck : Bool) : Com
         Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl' decl}"
       if shouldCheck then
         decl.check
-  if shouldCheck then
-    checkDeadLocalDecls decls
 
 def isValidMainType (type : Expr) : Bool :=
   let isValidResultName (name : Name) : Bool :=
@@ -74,7 +73,7 @@ def isValidMainType (type : Expr) : Bool :=
 
 namespace PassManager
 
-def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRecDepth 8192 do
+def run (declNames : Array Name) : CompilerM (Array (Array IR.Decl)) := withAtLeastMaxRecDepth 8192 do
   /-
   Note: we need to increase the recursion depth because we currently do to save phase1
   declarations in .olean files. Then, we have to recursively compile all dependencies,
@@ -100,31 +99,33 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe
   let decls := markRecDecls decls
   let manager ← getPassManager
   let isCheckEnabled := compiler.check.get (← getOptions)
-  let decls ← profileitM Exception "compilation (LCNF base)" (← getOptions) do
-    let mut decls := decls
-    for pass in manager.basePasses do
-      decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
-        withPhase pass.phase <| pass.run decls
-      withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
-    return decls
-  let decls ← profileitM Exception "compilation (LCNF mono)" (← getOptions) do
-    let mut decls := decls
-    for pass in manager.monoPasses do
-      decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
-        withPhase pass.phase <| pass.run decls
-      withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
-    return decls
-  if (← Lean.isTracingEnabledFor `Compiler.result) then
-    for decl in decls do
-      let decl ← normalizeFVarIds decl
-      Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}"
-  profileitM Exception "compilation (IR)" (← getOptions) do
-    let irDecls ← IR.toIR decls
-    IR.compile irDecls
+  let decls ← runPassManagerPart "compilation (LCNF base)" manager.basePasses decls isCheckEnabled
+  let decls ← runPassManagerPart "compilation (LCNF mono)" manager.monoPasses decls isCheckEnabled
+  let sccs ← withTraceNode `Compiler.splitSCC (fun _ => return m!"Splitting up SCC") do
+    splitScc decls
+  sccs.mapM fun decls => do
+    let decls ← runPassManagerPart "compilation (LCNF mono)" manager.monoPassesNoLambda decls isCheckEnabled
+    if (← Lean.isTracingEnabledFor `Compiler.result) then
+      for decl in decls do
+        let decl ← normalizeFVarIds decl
+        Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}"
+    profileitM Exception "compilation (IR)" (← getOptions) do
+      let irDecls ← IR.toIR decls
+      IR.compile irDecls
+where
+  runPassManagerPart (profilerName : String) (passes : Array Pass) (decls : Array Decl)
+      (isCheckEnabled : Bool) : CompilerM (Array Decl) := do
+    profileitM Exception profilerName (← getOptions) do
+      let mut decls := decls
+      for pass in passes do
+        decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
+          withPhase pass.phase <| pass.run decls
+        withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
+      return decls
 
 end PassManager
 
-def compile (declNames : Array Name) : CoreM (Array IR.Decl) :=
+def compile (declNames : Array Name) : CoreM (Array (Array IR.Decl)) :=
   CompilerM.run <| PassManager.run declNames
 
 def showDecl (phase : Phase) (declName : Name) : CoreM Format := do
diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean
index 3c19e48a79..1e1d025f52 100644
--- a/src/Lean/Compiler/LCNF/PassManager.lean
+++ b/src/Lean/Compiler/LCNF/PassManager.lean
@@ -87,6 +87,7 @@ pipeline.
 structure PassManager where
   basePasses : Array Pass
   monoPasses : Array Pass
+  monoPassesNoLambda : Array Pass
   deriving Inhabited
 
 instance : ToString Phase where
@@ -114,6 +115,7 @@ private def validatePasses (phase : Phase) (passes : Array Pass) : CoreM Unit :=
 def validate (manager : PassManager) : CoreM Unit := do
   validatePasses .base manager.basePasses
   validatePasses .mono manager.monoPasses
+  validatePasses .mono manager.monoPassesNoLambda
 
 def findOccurrenceBounds (targetName : Name) (passes : Array Pass) : CoreM (Nat × Nat) := do
   let mut lowest := none
diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean
index f72ef04318..8deeebfff1 100644
--- a/src/Lean/Compiler/LCNF/Passes.lean
+++ b/src/Lean/Compiler/LCNF/Passes.lean
@@ -115,6 +115,8 @@ def builtinPassManager : PassManager := {
     simp (occurrence := 4) (phase := .mono),
     floatLetIn (phase := .mono) (occurrence := 2),
     lambdaLifting,
+  ]
+  monoPassesNoLambda := #[
     extendJoinPointContext (phase := .mono) (occurrence := 1),
     simp (occurrence := 5) (phase := .mono),
     elimDeadBranches,
diff --git a/src/Lean/Compiler/LCNF/SplitSCC.lean b/src/Lean/Compiler/LCNF/SplitSCC.lean
new file mode 100644
index 0000000000..bcc222ab49
--- /dev/null
+++ b/src/Lean/Compiler/LCNF/SplitSCC.lean
@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+module
+
+prelude
+public import Lean.Compiler.LCNF.CompilerM
+import Lean.Util.SCC
+
+namespace Lean.Compiler.LCNF
+
+namespace SplitScc
+
+partial def findSccCalls (scc : Std.HashMap Name Decl) (decl : Decl) : BaseIO (Std.HashSet Name) := do
+  match decl.value with
+  | .code code =>
+    let (_, calls) ← goCode code |>.run {}
+    return calls
+  | .extern .. => return {}
+where
+  goCode (c : Code) : StateRefT (Std.HashSet Name) BaseIO Unit := do
+    match c with
+    | .let decl k =>
+      if let .const name .. := decl.value then
+        if scc.contains name then
+          modify fun s => s.insert name
+      goCode k
+    | .fun decl k | .jp decl k =>
+      goCode decl.value
+      goCode k
+    | .cases cases => cases.alts.forM (·.forCodeM goCode)
+    | .jmp .. | .return .. | .unreach .. => return ()
+
+end SplitScc
+
+public def splitScc (scc : Array Decl) : CompilerM (Array (Array Decl)) := do
+  let declMap := Std.HashMap.ofArray <| scc.map fun decl => (decl.name, decl)
+  let callers := Std.HashMap.ofArray <| ← scc.mapM fun decl => do
+    let calls ← SplitScc.findSccCalls declMap decl
+    return (decl.name, calls.toList)
+  let newSccs := Lean.SCC.scc (scc.toList.map (·.name)) (callers.getD · [])
+  trace[Compiler.splitSCC] m!"Split SCC into {newSccs}"
+  return newSccs.toArray.map (fun scc => scc.toArray.map declMap.get!)
+
+builtin_initialize
+  registerTraceClass `Compiler.splitSCC (inherited := true)
+
+end Lean.Compiler.LCNF
diff --git a/tests/lean/4089.lean.expected.out b/tests/lean/4089.lean.expected.out
index 94f27f05d3..56d3e001b0 100644
--- a/tests/lean/4089.lean.expected.out
+++ b/tests/lean/4089.lean.expected.out
@@ -8,9 +8,6 @@
         let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_3 x_2;
         ret x_4
 [Compiler.IR] [reset_reuse]
-    def Sigma.toProd (x_1 : ◾) (x_2 : ◾) (x_3 : obj) : obj :=
-      let x_4 : obj := Sigma.toProd._redArg x_3;
-      ret x_4
     def Sigma.toProd._redArg (x_1 : obj) : obj :=
       case x_1 : obj of
       Sigma.mk →
@@ -19,6 +16,10 @@
         let x_5 : tobj := reset[2] x_1;
         let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_2 x_3;
         ret x_4
+[Compiler.IR] [reset_reuse]
+    def Sigma.toProd (x_1 : ◾) (x_2 : ◾) (x_3 : obj) : obj :=
+      let x_4 : obj := Sigma.toProd._redArg x_3;
+      ret x_4
 [Compiler.IR] [reset_reuse]
     def foo (x_1 : tobj) : tobj :=
       case x_1 : tobj of
diff --git a/tests/lean/4240.lean.expected.out b/tests/lean/4240.lean.expected.out
index 24add9eb29..aa7e713870 100644
--- a/tests/lean/4240.lean.expected.out
+++ b/tests/lean/4240.lean.expected.out
@@ -1,10 +1,4 @@
 [Compiler.IR] [result]
-    def isSomeWithInstanceNat (x_1 : @& obj) : u8 :=
-      let x_2 : usize := 0;
-      let x_3 : tobj := Array.uget ◾ x_1 x_2 ◾;
-      let x_4 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_3;
-      dec x_3;
-      ret x_4
     def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 (x_1 : @& tobj) : u8 :=
       case x_1 : tobj of
       MyOption.none →
@@ -13,13 +7,20 @@
       MyOption.some →
         let x_3 : u8 := 1;
         ret x_3
-    def isSomeWithInstanceNat._boxed (x_1 : obj) : tagged :=
-      let x_2 : u8 := isSomeWithInstanceNat x_1;
-      dec x_1;
-      let x_3 : tagged := box x_2;
-      ret x_3
     def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0._boxed (x_1 : tobj) : tagged :=
       let x_2 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_1;
       dec x_1;
       let x_3 : tagged := box x_2;
       ret x_3
+[Compiler.IR] [result]
+    def isSomeWithInstanceNat (x_1 : @& obj) : u8 :=
+      let x_2 : usize := 0;
+      let x_3 : tobj := Array.uget ◾ x_1 x_2 ◾;
+      let x_4 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_3;
+      dec x_3;
+      ret x_4
+    def isSomeWithInstanceNat._boxed (x_1 : obj) : tagged :=
+      let x_2 : u8 := isSomeWithInstanceNat x_1;
+      dec x_1;
+      let x_3 : tagged := box x_2;
+      ret x_3
diff --git a/tests/lean/computedFieldsCode.lean.expected.out b/tests/lean/computedFieldsCode.lean.expected.out
index 55b538059e..54d3d38ce2 100644
--- a/tests/lean/computedFieldsCode.lean.expected.out
+++ b/tests/lean/computedFieldsCode.lean.expected.out
@@ -27,9 +27,6 @@
       dec x_1;
       ret x_2
 [Compiler.IR] [result]
-    def Exp.ctorElim (x_1 : ◾) (x_2 : @& tobj) (x_3 : tobj) (x_4 : ◾) (x_5 : tobj) : tobj :=
-      let x_6 : tobj := Exp.ctorElim._redArg x_3 x_5;
-      ret x_6
     def Exp.ctorElim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
       case x_1 : tobj of
       Exp.var →
@@ -49,59 +46,122 @@
       default →
         dec x_1;
         ret x_2
+[Compiler.IR] [result]
+    def Exp.ctorElim (x_1 : ◾) (x_2 : @& tobj) (x_3 : tobj) (x_4 : ◾) (x_5 : tobj) : tobj :=
+      let x_6 : tobj := Exp.ctorElim._redArg x_3 x_5;
+      ret x_6
     def Exp.ctorElim._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) : tobj :=
       let x_6 : tobj := Exp.ctorElim x_1 x_2 x_3 x_4 x_5;
       dec x_2;
       ret x_6
+[Compiler.IR] [result]
+    def Exp.var.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
+      let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
+      ret x_3
 [Compiler.IR] [result]
     def Exp.var.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
       let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
       ret x_5
-    def Exp.var.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
+[Compiler.IR] [result]
+    def Exp.app.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
       let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
       ret x_3
 [Compiler.IR] [result]
     def Exp.app.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
       let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
       ret x_5
-    def Exp.app.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
+[Compiler.IR] [result]
+    def Exp.a1.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
       let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
       ret x_3
 [Compiler.IR] [result]
     def Exp.a1.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
       let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
       ret x_5
-    def Exp.a1.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
+[Compiler.IR] [result]
+    def Exp.a2.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
       let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
       ret x_3
 [Compiler.IR] [result]
     def Exp.a2.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
       let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
       ret x_5
-    def Exp.a2.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
+[Compiler.IR] [result]
+    def Exp.a3.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
       let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
       ret x_3
 [Compiler.IR] [result]
     def Exp.a3.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
       let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
       ret x_5
-    def Exp.a3.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
+[Compiler.IR] [result]
+    def Exp.a4.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
       let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
       ret x_3
 [Compiler.IR] [result]
     def Exp.a4.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
       let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
       ret x_5
-    def Exp.a4.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
+[Compiler.IR] [result]
+    def Exp.a5.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
       let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
       ret x_3
 [Compiler.IR] [result]
     def Exp.a5.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
       let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
       ret x_5
-    def Exp.a5.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
-      let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
-      ret x_3
+[Compiler.IR] [result]
+    def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
+      case x_1 : tobj of
+      Exp.var._impl →
+        dec x_3;
+        let x_9 : u32 := sproj[0, 8] x_1;
+        dec x_1;
+        let x_10 : tobj := box x_9;
+        let x_11 : tobj := app x_2 x_10;
+        ret x_11
+      Exp.app._impl →
+        dec x_2;
+        let x_12 : tobj := proj[0] x_1;
+        inc x_12;
+        let x_13 : tobj := proj[1] x_1;
+        inc x_13;
+        dec x_1;
+        let x_14 : tobj := app x_3 x_12 x_13;
+        ret x_14
+      Exp.a1._impl →
+        dec x_3;
+        dec x_2;
+        inc x_4;
+        ret x_4
+      Exp.a2._impl →
+        dec x_3;
+        dec x_2;
+        inc x_5;
+        ret x_5
+      Exp.a3._impl →
+        dec x_3;
+        dec x_2;
+        inc x_6;
+        ret x_6
+      Exp.a4._impl →
+        dec x_3;
+        dec x_2;
+        inc x_7;
+        ret x_7
+      Exp.a5._impl →
+        dec x_3;
+        dec x_2;
+        inc x_8;
+        ret x_8
+    def Exp.casesOn._override._redArg._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) : tobj :=
+      let x_9 : tobj := Exp.casesOn._override._redArg x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8;
+      dec x_8;
+      dec x_7;
+      dec x_6;
+      dec x_5;
+      dec x_4;
+      ret x_9
 [Compiler.IR] [result]
     def Exp.casesOn._override (x_1 : ◾) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) (x_9 : @& tobj) : tobj :=
       case x_2 : tobj of
@@ -146,49 +206,6 @@
         dec x_3;
         inc x_9;
         ret x_9
-    def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
-      case x_1 : tobj of
-      Exp.var._impl →
-        dec x_3;
-        let x_9 : u32 := sproj[0, 8] x_1;
-        dec x_1;
-        let x_10 : tobj := box x_9;
-        let x_11 : tobj := app x_2 x_10;
-        ret x_11
-      Exp.app._impl →
-        dec x_2;
-        let x_12 : tobj := proj[0] x_1;
-        inc x_12;
-        let x_13 : tobj := proj[1] x_1;
-        inc x_13;
-        dec x_1;
-        let x_14 : tobj := app x_3 x_12 x_13;
-        ret x_14
-      Exp.a1._impl →
-        dec x_3;
-        dec x_2;
-        inc x_4;
-        ret x_4
-      Exp.a2._impl →
-        dec x_3;
-        dec x_2;
-        inc x_5;
-        ret x_5
-      Exp.a3._impl →
-        dec x_3;
-        dec x_2;
-        inc x_6;
-        ret x_6
-      Exp.a4._impl →
-        dec x_3;
-        dec x_2;
-        inc x_7;
-        ret x_7
-      Exp.a5._impl →
-        dec x_3;
-        dec x_2;
-        inc x_8;
-        ret x_8
     def Exp.casesOn._override._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) (x_9 : tobj) : tobj :=
       let x_10 : tobj := Exp.casesOn._override x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9;
       dec x_9;
@@ -197,37 +214,7 @@
       dec x_6;
       dec x_5;
       ret x_10
-    def Exp.casesOn._override._redArg._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) : tobj :=
-      let x_9 : tobj := Exp.casesOn._override._redArg x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8;
-      dec x_8;
-      dec x_7;
-      dec x_6;
-      dec x_5;
-      dec x_4;
-      ret x_9
 [Compiler.IR] [result]
-    def Exp.a1._override : tobj :=
-      let x_1 : tagged := ctor_2[Exp.a1._impl];
-      ret x_1
-    def Exp.a2._override : tobj :=
-      let x_1 : tagged := ctor_3[Exp.a2._impl];
-      ret x_1
-    def Exp.a3._override : tobj :=
-      let x_1 : tagged := ctor_4[Exp.a3._impl];
-      ret x_1
-    def Exp.a4._override : tobj :=
-      let x_1 : tagged := ctor_5[Exp.a4._impl];
-      ret x_1
-    def Exp.a5._override : tobj :=
-      let x_1 : tagged := ctor_6[Exp.a5._impl];
-      ret x_1
-    def Exp.app._override (x_1 : tobj) (x_2 : tobj) : tobj :=
-      let x_3 : u64 := Exp.hash._override x_1;
-      let x_4 : u64 := Exp.hash._override x_2;
-      let x_5 : u64 := mixHash x_3 x_4;
-      let x_6 : obj := ctor_1.0.8[Exp.app._impl] x_1 x_2;
-      sset x_6[2, 0] : u64 := x_5;
-      ret x_6
     def Exp.var._override (x_1 : u32) : tobj :=
       let x_2 : u64 := UInt32.toUInt64 x_1;
       let x_3 : u64 := 1000;
@@ -236,6 +223,12 @@
       sset x_5[0, 0] : u64 := x_4;
       sset x_5[0, 8] : u32 := x_1;
       ret x_5
+    def Exp.var._override._boxed (x_1 : tobj) : tobj :=
+      let x_2 : u32 := unbox x_1;
+      dec x_1;
+      let x_3 : tobj := Exp.var._override x_2;
+      ret x_3
+[Compiler.IR] [result]
     def Exp.hash._override (x_1 : @& tobj) : u64 :=
       case x_1 : tobj of
       Exp.var._impl →
@@ -247,16 +240,39 @@
       default →
         let x_4 : u64 := 42;
         ret x_4
-    def Exp.var._override._boxed (x_1 : tobj) : tobj :=
-      let x_2 : u32 := unbox x_1;
-      dec x_1;
-      let x_3 : tobj := Exp.var._override x_2;
-      ret x_3
     def Exp.hash._override._boxed (x_1 : tobj) : tobj :=
       let x_2 : u64 := Exp.hash._override x_1;
       dec x_1;
       let x_3 : tobj := box x_2;
       ret x_3
+[Compiler.IR] [result]
+    def Exp.app._override (x_1 : tobj) (x_2 : tobj) : tobj :=
+      let x_3 : u64 := Exp.hash._override x_1;
+      let x_4 : u64 := Exp.hash._override x_2;
+      let x_5 : u64 := mixHash x_3 x_4;
+      let x_6 : obj := ctor_1.0.8[Exp.app._impl] x_1 x_2;
+      sset x_6[2, 0] : u64 := x_5;
+      ret x_6
+[Compiler.IR] [result]
+    def Exp.a1._override : tobj :=
+      let x_1 : tagged := ctor_2[Exp.a1._impl];
+      ret x_1
+[Compiler.IR] [result]
+    def Exp.a2._override : tobj :=
+      let x_1 : tagged := ctor_3[Exp.a2._impl];
+      ret x_1
+[Compiler.IR] [result]
+    def Exp.a3._override : tobj :=
+      let x_1 : tagged := ctor_4[Exp.a3._impl];
+      ret x_1
+[Compiler.IR] [result]
+    def Exp.a4._override : tobj :=
+      let x_1 : tagged := ctor_5[Exp.a4._impl];
+      ret x_1
+[Compiler.IR] [result]
+    def Exp.a5._override : tobj :=
+      let x_1 : tagged := ctor_6[Exp.a5._impl];
+      ret x_1
 [Compiler.IR] [result]
     def f._closed_0 : tobj :=
       let x_1 : u32 := 10;
diff --git a/tests/lean/doubleReset.lean.expected.out b/tests/lean/doubleReset.lean.expected.out
index f6d2154c54..769653f97b 100644
--- a/tests/lean/doubleReset.lean.expected.out
+++ b/tests/lean/doubleReset.lean.expected.out
@@ -1,15 +1,4 @@
 [Compiler.IR] [reset_reuse]
-    def _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0 (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) (x_4 : tobj) (x_5 : usize) (x_6 : usize) (x_7 : obj) : obj :=
-      let x_8 : obj := _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_4 x_5 x_6 x_7;
-      ret x_8
-    def applyProjectionRules (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) (x_4 : obj) (x_5 : tobj) : obj :=
-      let x_6 : obj := applyProjectionRules._redArg x_4 x_5;
-      ret x_6
-    def applyProjectionRules._redArg (x_1 : obj) (x_2 : tobj) : obj :=
-      let x_3 : usize := Array.usize ◾ x_1;
-      let x_4 : usize := 0;
-      let x_5 : obj := _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_2 x_3 x_4 x_1;
-      ret x_5
     def _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg (x_1 : tobj) (x_2 : usize) (x_3 : usize) (x_4 : obj) : obj :=
       let x_5 : u8 := USize.decLt x_3 x_2;
       case x_5 : u8 of
@@ -35,3 +24,17 @@
             let x_16 : obj := Array.uset ◾ x_11 x_3 x_13 ◾;
             let x_17 : obj := _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_1 x_2 x_15 x_16;
             ret x_17
+[Compiler.IR] [reset_reuse]
+    def applyProjectionRules._redArg (x_1 : obj) (x_2 : tobj) : obj :=
+      let x_3 : usize := Array.usize ◾ x_1;
+      let x_4 : usize := 0;
+      let x_5 : obj := _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_2 x_3 x_4 x_1;
+      ret x_5
+[Compiler.IR] [reset_reuse]
+    def applyProjectionRules (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) (x_4 : obj) (x_5 : tobj) : obj :=
+      let x_6 : obj := applyProjectionRules._redArg x_4 x_5;
+      ret x_6
+[Compiler.IR] [reset_reuse]
+    def _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0 (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) (x_4 : tobj) (x_5 : usize) (x_6 : usize) (x_7 : obj) : obj :=
+      let x_8 : obj := _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_4 x_5 x_6 x_7;
+      ret x_8
diff --git a/tests/lean/reduceArity.lean.expected.out b/tests/lean/reduceArity.lean.expected.out
index acbe2c470e..e158d9598b 100644
--- a/tests/lean/reduceArity.lean.expected.out
+++ b/tests/lean/reduceArity.lean.expected.out
@@ -1,7 +1,3 @@
-[Compiler.result] size: 1
-    def g (α : ◾) (n : Nat) (a : lcAny) (b : lcAny) (f : lcAny → lcAny) : lcAny :=
-      let _x.1 := g._redArg n a f;
-      return _x.1
 [Compiler.result] size: 9
     def g._redArg (n : Nat) (a : lcAny) (f : lcAny → lcAny) : lcAny :=
       let zero := 0;
@@ -15,6 +11,10 @@
         let _x.2 := g._redArg n.1 a f;
         let _x.3 := f _x.2;
         return _x.3
+[Compiler.result] size: 1
+    def g (α : ◾) (n : Nat) (a : lcAny) (b : lcAny) (f : lcAny → lcAny) : lcAny :=
+      let _x.1 := g._redArg n a f;
+      return _x.1
 [Compiler.result] size: 1
     def h._closed_0 : Nat → Nat :=
       let _x.1 := double;
diff --git a/tests/lean/run/async_sleep.lean b/tests/lean/run/async_sleep.lean
index 8bdb42bde4..e26f200d77 100644
--- a/tests/lean/run/async_sleep.lean
+++ b/tests/lean/run/async_sleep.lean
@@ -13,7 +13,6 @@ def assertDuration (should : Nat) (eps : Nat) (x : IO α) : IO α := do
   assertElapsed t1 t2 should eps
   return res
 
-
 def BASE_DURATION : Nat := 1000
 
 -- generous tolerance for slow CI systems
diff --git a/tests/lean/run/boxing_bug.lean b/tests/lean/run/boxing_bug.lean
index bdbbf02a2e..a3b8046811 100644
--- a/tests/lean/run/boxing_bug.lean
+++ b/tests/lean/run/boxing_bug.lean
@@ -6,9 +6,6 @@ class Semiring (α : Type u) where
 
 /--
 trace: [Compiler.IR] [result]
-    def instSemiringUInt8 : obj :=
-      let x_1 : obj := pap instSemiringUInt8._lam_0._boxed;
-      ret x_1
     def instSemiringUInt8._lam_0 (x_1 : @& tobj) (x_2 : u8) : u8 :=
       let x_3 : u8 := UInt8.ofNat x_1;
       let x_4 : u8 := UInt8.mul x_3 x_2;
@@ -19,6 +16,13 @@ trace: [Compiler.IR] [result]
       dec x_1;
       let x_5 : tagged := box x_4;
       ret x_5
+[Compiler.IR] [result]
+    def instSemiringUInt8._closed_0 : obj :=
+      let x_1 : obj := pap instSemiringUInt8._lam_0._boxed;
+      ret x_1
+    def instSemiringUInt8 : obj :=
+      let x_1 : obj := instSemiringUInt8._closed_0;
+      ret x_1
 -/
 #guard_msgs in
 set_option trace.compiler.ir.result true in
diff --git a/tests/lean/run/do_for_loop_compiler_test.lean b/tests/lean/run/do_for_loop_compiler_test.lean
index 1cf37ec576..8b2117be83 100644
--- a/tests/lean/run/do_for_loop_compiler_test.lean
+++ b/tests/lean/run/do_for_loop_compiler_test.lean
@@ -18,17 +18,6 @@ trace: [Compiler.saveMono] size: 7
         let x := Nat.add _x.6 head.4;
         let _x.7 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i _x.1 tail.2 tail.5 x;
         return _x.7
-[Compiler.saveMono] size: 7
-    def List.newForIn._at_.testing.spec_0 i kcontinue l b : Nat :=
-      cases l : Nat
-      | List.nil =>
-        let _x.1 := kcontinue b;
-        return _x.1
-      | List.cons head.2 tail.3 =>
-        let _x.4 := Nat.add b i;
-        let x := Nat.add _x.4 head.2;
-        let _x.5 := List.newForIn._at_.testing.spec_0 i kcontinue tail.3 x;
-        return _x.5
 [Compiler.saveMono] size: 7
     def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 _x.1 tail.2 i l b : Nat :=
       cases l : Nat
@@ -40,18 +29,6 @@ trace: [Compiler.saveMono] size: 7
         let x := Nat.add _x.6 head.4;
         let _x.7 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i _x.1 tail.2 tail.5 x;
         return _x.7
-[Compiler.saveMono] size: 9
-    def testing : Nat :=
-      let x := 42;
-      let _x.1 := 1;
-      let _x.2 := 2;
-      let _x.3 := 3;
-      let _x.4 := [] ◾;
-      let _x.5 := List.cons ◾ _x.3 _x.4;
-      let _x.6 := List.cons ◾ _x.2 _x.5;
-      let _x.7 := List.cons ◾ _x.1 _x.6;
-      let _x.8 := List.newForIn._at_.testing.spec_1 _x.1 _x.7 x;
-      return _x.8
 [Compiler.saveMono] size: 12
     def List.newForIn._at_.testing.spec_1 _x.1 l b : Nat :=
       cases l : Nat
@@ -68,6 +45,29 @@ trace: [Compiler.saveMono] size: 7
         let _x.11 := List.range'TR.go _x.1 _x.8 _x.9 _x.10;
         let _x.12 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 _x.1 tail.3 head.2 _x.11 b;
         return _x.12
+[Compiler.saveMono] size: 9
+    def testing : Nat :=
+      let x := 42;
+      let _x.1 := 1;
+      let _x.2 := 2;
+      let _x.3 := 3;
+      let _x.4 := [] ◾;
+      let _x.5 := List.cons ◾ _x.3 _x.4;
+      let _x.6 := List.cons ◾ _x.2 _x.5;
+      let _x.7 := List.cons ◾ _x.1 _x.6;
+      let _x.8 := List.newForIn._at_.testing.spec_1 _x.1 _x.7 x;
+      return _x.8
+[Compiler.saveMono] size: 7
+    def List.newForIn._at_.testing.spec_0 i kcontinue l b : Nat :=
+      cases l : Nat
+      | List.nil =>
+        let _x.1 := kcontinue b;
+        return _x.1
+      | List.cons head.2 tail.3 =>
+        let _x.4 := Nat.add b i;
+        let x := Nat.add _x.4 head.2;
+        let _x.5 := List.newForIn._at_.testing.spec_0 i kcontinue tail.3 x;
+        return _x.5
 -/
 #guard_msgs in
 set_option trace.Compiler.saveMono true in
@@ -100,18 +100,6 @@ trace: [Compiler.saveMono] size: 7
         let x := Nat.add _x.6 head.4;
         let _x.7 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 _x.1 tail.2 i tail.5 x;
         return _x.7
-[Compiler.saveMono] size: 9
-    def testing2 : Nat :=
-      let x := 42;
-      let _x.1 := 1;
-      let _x.2 := 2;
-      let _x.3 := 3;
-      let _x.4 := [] ◾;
-      let _x.5 := List.cons ◾ _x.3 _x.4;
-      let _x.6 := List.cons ◾ _x.2 _x.5;
-      let _x.7 := List.cons ◾ _x.1 _x.6;
-      let _x.8 := List.newForIn._at_.testing2.spec_0 _x.1 _x.7 x;
-      return _x.8
 [Compiler.saveMono] size: 14
     def List.newForIn._at_.testing2.spec_0 _x.1 l b : Nat :=
       cases l : Nat
@@ -130,6 +118,18 @@ trace: [Compiler.saveMono] size: 7
         let _x.12 := List.range'TR.go _x.1 _x.9 _x.10 _x.11;
         let _x.13 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 _x.1 tail.3 head.2 _x.12 x;
         return _x.13
+[Compiler.saveMono] size: 9
+    def testing2 : Nat :=
+      let x := 42;
+      let _x.1 := 1;
+      let _x.2 := 2;
+      let _x.3 := 3;
+      let _x.4 := [] ◾;
+      let _x.5 := List.cons ◾ _x.3 _x.4;
+      let _x.6 := List.cons ◾ _x.2 _x.5;
+      let _x.7 := List.cons ◾ _x.1 _x.6;
+      let _x.8 := List.newForIn._at_.testing2.spec_0 _x.1 _x.7 x;
+      return _x.8
 -/
 #guard_msgs in
 set_option trace.Compiler.saveMono true in
@@ -164,19 +164,6 @@ trace: [Compiler.saveMono] size: 9
         let x := Nat.add _x.7 head.4;
         let _x.8 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i _x.1 tail.2 tail.5 x;
         return _x.8
-[Compiler.saveMono] size: 9
-    def List.newForIn._at_.testing3.spec_0 s i kcontinue l b : Nat :=
-      cases l : Nat
-      | List.nil =>
-        let _x.1 := kcontinue b;
-        return _x.1
-      | List.cons head.2 tail.3 =>
-        let _x.4 := Nat.add b b;
-        let x := Nat.add _x.4 s;
-        let _x.5 := Nat.add x i;
-        let x := Nat.add _x.5 head.2;
-        let _x.6 := List.newForIn._at_.testing3.spec_0 s i kcontinue tail.3 x;
-        return _x.6
 [Compiler.saveMono] size: 9
     def List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 _x.1 tail.2 s i l b : Nat :=
       cases l : Nat
@@ -190,18 +177,6 @@ trace: [Compiler.saveMono] size: 9
         let x := Nat.add _x.7 head.4;
         let _x.8 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i _x.1 tail.2 tail.5 x;
         return _x.8
-[Compiler.saveMono] size: 9
-    def testing3 : Nat :=
-      let x := 42;
-      let _x.1 := 1;
-      let _x.2 := 2;
-      let _x.3 := 3;
-      let _x.4 := [] ◾;
-      let _x.5 := List.cons ◾ _x.3 _x.4;
-      let _x.6 := List.cons ◾ _x.2 _x.5;
-      let _x.7 := List.cons ◾ _x.1 _x.6;
-      let _x.8 := List.newForIn._at_.testing3.spec_1 _x.1 _x.7 x;
-      return _x.8
 [Compiler.saveMono] size: 12
     def List.newForIn._at_.testing3.spec_1 _x.1 l b : Nat :=
       cases l : Nat
@@ -218,6 +193,31 @@ trace: [Compiler.saveMono] size: 9
         let _x.11 := List.range'TR.go _x.1 _x.8 _x.9 _x.10;
         let _x.12 := List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 _x.1 tail.3 b head.2 _x.11 b;
         return _x.12
+[Compiler.saveMono] size: 9
+    def testing3 : Nat :=
+      let x := 42;
+      let _x.1 := 1;
+      let _x.2 := 2;
+      let _x.3 := 3;
+      let _x.4 := [] ◾;
+      let _x.5 := List.cons ◾ _x.3 _x.4;
+      let _x.6 := List.cons ◾ _x.2 _x.5;
+      let _x.7 := List.cons ◾ _x.1 _x.6;
+      let _x.8 := List.newForIn._at_.testing3.spec_1 _x.1 _x.7 x;
+      return _x.8
+[Compiler.saveMono] size: 9
+    def List.newForIn._at_.testing3.spec_0 s i kcontinue l b : Nat :=
+      cases l : Nat
+      | List.nil =>
+        let _x.1 := kcontinue b;
+        return _x.1
+      | List.cons head.2 tail.3 =>
+        let _x.4 := Nat.add b b;
+        let x := Nat.add _x.4 s;
+        let _x.5 := Nat.add x i;
+        let x := Nat.add _x.5 head.2;
+        let _x.6 := List.newForIn._at_.testing3.spec_0 s i kcontinue tail.3 x;
+        return _x.6
 -/
 #guard_msgs in
 set_option trace.Compiler.saveMono true in
diff --git a/tests/lean/run/do_for_loop_levenstein_compiler_test.lean b/tests/lean/run/do_for_loop_levenstein_compiler_test.lean
index a500974651..7be10d86e6 100644
--- a/tests/lean/run/do_for_loop_levenstein_compiler_test.lean
+++ b/tests/lean/run/do_for_loop_levenstein_compiler_test.lean
@@ -21,39 +21,7 @@
   loop range.start (by simp) (by simp) init
 
 /--
-trace: [Compiler.saveMono] size: 1
-    def Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4 s' _x.1 _x.2 as sz _x.3 range this i hs hl a.4 : Array
-      String :=
-      let _x.5 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 _x.2 as sz _x.3 range i a.4;
-      return _x.5
-[Compiler.saveMono] size: 1
-    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1 s' _x.1 _x.2 kcontinue range this i hs hl a.3 : Array
-      String :=
-      let _x.4 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range i a.3;
-      return _x.4
-[Compiler.saveMono] size: 1
-    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4 as sz _x.1 s' _x.2 _x.3 range this i hs hl a.4 : Array
-      String :=
-      let _x.5 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.1 s' _x.2 _x.3 range i a.4;
-      return _x.5
-[Compiler.saveMono] size: 12
-    def Array.contains._at_.deletions.spec_0 as a : Bool :=
-      let _x.1 := 0;
-      let _x.2 := Array.size ◾ as;
-      let _x.3 := Nat.decLt _x.1 _x.2;
-      cases _x.3 : Bool
-      | Bool.false =>
-        return _x.3
-      | Bool.true =>
-        cases _x.3 : Bool
-        | Bool.false =>
-          return _x.3
-        | Bool.true =>
-          let _x.4 := 0;
-          let _x.5 := USize.ofNat _x.2;
-          let _x.6 := Array.anyMUnsafe.any._at_.Array.contains._at_.deletions.spec_0.spec_0.2 a as _x.4 _x.5;
-          return _x.6
-[Compiler.saveMono] size: 13
+trace: [Compiler.saveMono] size: 13
     def _private.Init.Data.Array.Basic.0.Array.anyMUnsafe.any._at_.Array.contains._at_.deletions.spec_0.spec_0 a as i stop : Bool :=
       let _x.1 := USize.decEq i stop;
       cases _x.1 : Bool
@@ -71,25 +39,23 @@ trace: [Compiler.saveMono] size: 1
       | Bool.true =>
         let _x.7 := false;
         return _x.7
-[Compiler.saveMono] size: 15
-    def deletions n s : Array String :=
-      let zero := 0;
-      let isZero := Nat.decEq n zero;
-      cases isZero : Array String
-      | Bool.true =>
-        let _x.1 := 1;
-        let _x.2 := Array.mkEmpty ◾ _x.1;
-        let _x.3 := Array.push ◾ _x.2 s;
-        return _x.3
+[Compiler.saveMono] size: 12
+    def Array.contains._at_.deletions.spec_0 as a : Bool :=
+      let _x.1 := 0;
+      let _x.2 := Array.size ◾ as;
+      let _x.3 := Nat.decLt _x.1 _x.2;
+      cases _x.3 : Bool
       | Bool.false =>
-        let one := 1;
-        let n.4 := Nat.sub n one;
-        let out := Array.mkEmpty ◾ zero;
-        let _x.5 := deletions n.4 s;
-        let sz := Array.usize ◾ _x.5;
-        let _x.6 := 0;
-        let _x.7 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 _x.5 sz _x.6 out;
-        return _x.7
+        return _x.3
+      | Bool.true =>
+        cases _x.3 : Bool
+        | Bool.false =>
+          return _x.3
+        | Bool.true =>
+          let _x.4 := 0;
+          let _x.5 := USize.ofNat _x.2;
+          let _x.6 := Array.anyMUnsafe.any._at_.Array.contains._at_.deletions.spec_0.spec_0.2 a as _x.4 _x.5;
+          return _x.6
 [Compiler.saveMono] size: 19
     def Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz i s : Array String :=
       let _x.1 := USize.decLt i sz;
@@ -186,6 +152,25 @@ trace: [Compiler.saveMono] size: 1
               return _x.19
             | Bool.true =>
               goto _jp.16
+[Compiler.saveMono] size: 15
+    def deletions n s : Array String :=
+      let zero := 0;
+      let isZero := Nat.decEq n zero;
+      cases isZero : Array String
+      | Bool.true =>
+        let _x.1 := 1;
+        let _x.2 := Array.mkEmpty ◾ _x.1;
+        let _x.3 := Array.push ◾ _x.2 s;
+        return _x.3
+      | Bool.false =>
+        let one := 1;
+        let n.4 := Nat.sub n one;
+        let out := Array.mkEmpty ◾ zero;
+        let _x.5 := deletions n.4 s;
+        let sz := Array.usize ◾ _x.5;
+        let _x.6 := 0;
+        let _x.7 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 _x.5 sz _x.6 out;
+        return _x.7
 [Compiler.saveMono] size: 29
     def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range i a.3 : Array
       String :=
@@ -222,6 +207,21 @@ trace: [Compiler.saveMono] size: 1
               return _x.18
             | Bool.true =>
               goto _jp.15
+[Compiler.saveMono] size: 1
+    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1 s' _x.1 _x.2 kcontinue range this i hs hl a.3 : Array
+      String :=
+      let _x.4 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range i a.3;
+      return _x.4
+[Compiler.saveMono] size: 1
+    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4 as sz _x.1 s' _x.2 _x.3 range this i hs hl a.4 : Array
+      String :=
+      let _x.5 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.1 s' _x.2 _x.3 range i a.4;
+      return _x.5
+[Compiler.saveMono] size: 1
+    def Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4 s' _x.1 _x.2 as sz _x.3 range this i hs hl a.4 : Array
+      String :=
+      let _x.5 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 _x.2 as sz _x.3 range i a.4;
+      return _x.5
 -/
 #guard_msgs in
 set_option trace.Compiler.saveMono true in
diff --git a/tests/lean/run/emptyLcnf.lean b/tests/lean/run/emptyLcnf.lean
index 3e74cdd6f7..9ee6e7744d 100644
--- a/tests/lean/run/emptyLcnf.lean
+++ b/tests/lean/run/emptyLcnf.lean
@@ -41,6 +41,13 @@ trace: [Compiler.result] size: 5
       let _x.2 := _eval._closed_2.2;
       let _x.3 := Array.push ◾ _x.2 _x.1;
       return _x.3
+[Compiler.result] size: 3
+    def _private.lean.run.emptyLcnf.0._eval._closed_4 : Lean.Elab.Term.Context →
+      lcAny → Lean.Meta.Context → lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit :=
+      let _x.1 := PUnit.unit;
+      let _x.2 := _eval._closed_3.2;
+      let _f.3 := _eval._lam_0.2 _x.2 _x.1;
+      return _f.3
 [Compiler.result] size: 8
     def _private.lean.run.emptyLcnf.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
       let _x.4 := _eval._closed_0.2;
@@ -49,7 +56,7 @@ trace: [Compiler.result] size: 5
       let _x.7 := _eval._closed_2.2;
       let _x.8 := _eval._closed_3.2;
       let _x.9 := PUnit.unit;
-      let _f.10 := _eval._lam_0.2 _x.8 _x.9;
+      let _f.10 := _eval._closed_4.2;
       let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
       return _x.11
 -/
diff --git a/tests/lean/run/erased.lean b/tests/lean/run/erased.lean
index 6cccf2ac6e..ec6befe0e4 100644
--- a/tests/lean/run/erased.lean
+++ b/tests/lean/run/erased.lean
@@ -61,6 +61,16 @@ trace: [Compiler.result] size: 5
       let _x.2 : Array Lean.Name := _eval._closed_3.2;
       let _x.3 : Array Lean.Name := Array.push ◾ _x.2 _x.1;
       return _x.3
+[Compiler.result] size: 3
+    def _private.lean.run.erased.0._eval._closed_5 : Lean.Elab.Term.Context →
+      lcAny → Lean.Meta.Context → lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit :=
+      let _x.1 : PUnit := PUnit.unit;
+      let _x.2 : Array Lean.Name := _eval._closed_4.2;
+      let _f.3 : Lean.Elab.Term.Context →
+        lcAny →
+          Lean.Meta.Context →
+            lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0.2 _x.2 _x.1;
+      return _f.3
 [Compiler.result] size: 9
     def _private.lean.run.erased.0._eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcVoid) : EST.Out
       Lean.Exception lcAny PUnit :=
@@ -74,8 +84,7 @@ trace: [Compiler.result] size: 5
       let _f.11 : Lean.Elab.Term.Context →
         lcAny →
           Lean.Meta.Context →
-            lcAny →
-              Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0.2 _x.9 _x.10;
+            lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._closed_5.2;
       let _x.12 : EST.Out Lean.Exception lcAny PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
       return _x.12
 -/