diff --git a/src/Lean/Compiler/LCNF/Closure.lean b/src/Lean/Compiler/LCNF/Closure.lean
index de77803a2c..e13b88d2af 100644
--- a/src/Lean/Compiler/LCNF/Closure.lean
+++ b/src/Lean/Compiler/LCNF/Closure.lean
@@ -33,10 +33,6 @@ structure Context where
   Remark: the lambda lifting pass abstracts all `let`/`fun`-declarations.
   -/
   abstract : FVarId → Bool
-  /--
-  Indicates whether we are processing terms beneath a binder.
-  -/
-  isUnderBinder : Bool
 
 /--
 State for the `ClosureM` monad.
@@ -103,8 +99,7 @@ mutual
     match c with
     | .let decl k =>
       collectType decl.type
-      withReader (fun ctx => { ctx with isUnderBinder := ctx.isUnderBinder || decl.type.isForall })
-        do collectLetValue decl.value
+      collectLetValue decl.value
       collectCode k
     | .fun decl k | .jp decl k => collectFunDecl decl; collectCode k
     | .cases c =>
@@ -122,8 +117,7 @@ mutual
   partial def collectFunDecl (decl : FunDecl) : ClosureM Unit := do
     collectType decl.type
     collectParams decl.params
-    withReader (fun ctx => { ctx with isUnderBinder := true }) do
-      collectCode decl.value
+    collectCode decl.value
 
   /--
   Process the given free variable.
@@ -146,7 +140,7 @@ mutual
           modify fun s => { s with params := s.params.push param }
         else if let some letDecl ← findLetDecl? fvarId then
           collectType letDecl.type
-          if ctx.isUnderBinder || ctx.abstract letDecl.fvarId then
+          if ctx.abstract letDecl.fvarId then
             modify fun s => { s with params := s.params.push <| { letDecl with borrow := false } }
           else
             collectLetValue letDecl.value
@@ -162,7 +156,7 @@ mutual
 end
 
 def run (x : ClosureM α) (inScope : FVarId → Bool) (abstract : FVarId → Bool := fun _ => true) : CompilerM (α × Array Param × Array CodeDecl) := do
-  let (a, s) ← x { inScope, abstract, isUnderBinder := false } |>.run {}
+  let (a, s) ← x { inScope, abstract } |>.run {}
   -- If we've abstracted an fvar into a param, exclude its definition. Note that this still allows
   -- for other decls the removed decl depends upon to be included, but they will be removed later
   -- for having no users.
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..6c6b3bee8f 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// update thy
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/do_for_loop_compiler_test.lean b/tests/lean/run/do_for_loop_compiler_test.lean
index 8b2117be83..08d4080e54 100644
--- a/tests/lean/run/do_for_loop_compiler_test.lean
+++ b/tests/lean/run/do_for_loop_compiler_test.lean
@@ -8,43 +8,43 @@ def List.newForIn (l : List α) (b : β) (kcons : α → (β → γ) → β →
 
 /--
 trace: [Compiler.saveMono] size: 7
-    def 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 l b : Nat :=
+    def List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i tail.1 l b : Nat :=
       cases l : Nat
       | List.nil =>
-        let _x.3 := List.newForIn._at_.testing.spec_1 _x.1 tail.2 b;
-        return _x.3
-      | List.cons head.4 tail.5 =>
-        let _x.6 := Nat.add b i;
-        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
+        let _x.2 := List.newForIn._at_.testing.spec_1 tail.1 b;
+        return _x.2
+      | List.cons head.3 tail.4 =>
+        let _x.5 := Nat.add b i;
+        let x := Nat.add _x.5 head.3;
+        let _x.6 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i tail.1 tail.4 x;
+        return _x.6
 [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 :=
+    def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 tail.1 i l b : Nat :=
       cases l : Nat
       | List.nil =>
-        let _x.3 := List.newForIn._at_.testing.spec_1 _x.1 tail.2 b;
-        return _x.3
-      | List.cons head.4 tail.5 =>
-        let _x.6 := Nat.add b i;
-        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
+        let _x.2 := List.newForIn._at_.testing.spec_1 tail.1 b;
+        return _x.2
+      | List.cons head.3 tail.4 =>
+        let _x.5 := Nat.add b i;
+        let x := Nat.add _x.5 head.3;
+        let _x.6 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i tail.1 tail.4 x;
+        return _x.6
 [Compiler.saveMono] size: 12
-    def List.newForIn._at_.testing.spec_1 _x.1 l b : Nat :=
+    def List.newForIn._at_.testing.spec_1 l b : Nat :=
       cases l : Nat
       | List.nil =>
         return b
-      | List.cons head.2 tail.3 =>
+      | List.cons head.1 tail.2 =>
+        let _x.3 := 1;
         let _x.4 := 10;
-        let _x.5 := Nat.sub _x.4 head.2;
-        let _x.6 := Nat.add _x.5 _x.1;
-        let _x.7 := 1;
-        let _x.8 := Nat.sub _x.6 _x.7;
-        let _x.9 := Nat.add head.2 _x.8;
-        let _x.10 := [] ◾;
-        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
+        let _x.5 := Nat.sub _x.4 head.1;
+        let _x.6 := Nat.add _x.5 _x.3;
+        let _x.7 := Nat.sub _x.6 _x.3;
+        let _x.8 := Nat.add head.1 _x.7;
+        let _x.9 := [] ◾;
+        let _x.10 := List.range'TR.go _x.3 _x.7 _x.8 _x.9;
+        let _x.11 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 tail.2 head.1 _x.10 b;
+        return _x.11
 [Compiler.saveMono] size: 9
     def testing : Nat :=
       let x := 42;
@@ -55,7 +55,7 @@ trace: [Compiler.saveMono] size: 7
       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;
+      let _x.8 := List.newForIn._at_.testing.spec_1 _x.7 x;
       return _x.8
 [Compiler.saveMono] size: 7
     def List.newForIn._at_.testing.spec_0 i kcontinue l b : Nat :=
@@ -90,34 +90,34 @@ def testing :=
 
 /--
 trace: [Compiler.saveMono] size: 7
-    def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 _x.1 tail.2 i l b : Nat :=
+    def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 tail.1 i l b : Nat :=
       cases l : Nat
       | List.nil =>
-        let _x.3 := List.newForIn._at_.testing2.spec_0 _x.1 tail.2 b;
-        return _x.3
-      | List.cons head.4 tail.5 =>
-        let _x.6 := Nat.add b i;
-        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
+        let _x.2 := List.newForIn._at_.testing2.spec_0 tail.1 b;
+        return _x.2
+      | List.cons head.3 tail.4 =>
+        let _x.5 := Nat.add b i;
+        let x := Nat.add _x.5 head.3;
+        let _x.6 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 tail.1 i tail.4 x;
+        return _x.6
 [Compiler.saveMono] size: 14
-    def List.newForIn._at_.testing2.spec_0 _x.1 l b : Nat :=
+    def List.newForIn._at_.testing2.spec_0 l b : Nat :=
       cases l : Nat
       | List.nil =>
         return b
-      | List.cons head.2 tail.3 =>
+      | List.cons head.1 tail.2 =>
+        let _x.3 := 1;
         let _x.4 := 37;
         let x := Nat.add b _x.4;
         let _x.5 := 10;
-        let _x.6 := Nat.sub _x.5 head.2;
-        let _x.7 := Nat.add _x.6 _x.1;
-        let _x.8 := 1;
-        let _x.9 := Nat.sub _x.7 _x.8;
-        let _x.10 := Nat.add head.2 _x.9;
-        let _x.11 := [] ◾;
-        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
+        let _x.6 := Nat.sub _x.5 head.1;
+        let _x.7 := Nat.add _x.6 _x.3;
+        let _x.8 := Nat.sub _x.7 _x.3;
+        let _x.9 := Nat.add head.1 _x.8;
+        let _x.10 := [] ◾;
+        let _x.11 := List.range'TR.go _x.3 _x.8 _x.9 _x.10;
+        let _x.12 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 tail.2 head.1 _x.11 x;
+        return _x.12
 [Compiler.saveMono] size: 9
     def testing2 : Nat :=
       let x := 42;
@@ -128,7 +128,7 @@ trace: [Compiler.saveMono] size: 7
       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;
+      let _x.8 := List.newForIn._at_.testing2.spec_0 _x.7 x;
       return _x.8
 -/
 #guard_msgs in
@@ -152,47 +152,47 @@ def testing2 :=
 
 /--
 trace: [Compiler.saveMono] size: 9
-    def 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 l b : Nat :=
+    def List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i tail.1 l b : Nat :=
       cases l : Nat
       | List.nil =>
-        let _x.3 := List.newForIn._at_.testing3.spec_1 _x.1 tail.2 b;
-        return _x.3
-      | List.cons head.4 tail.5 =>
-        let _x.6 := Nat.add b b;
-        let x := Nat.add _x.6 s;
-        let _x.7 := Nat.add x i;
-        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
+        let _x.2 := List.newForIn._at_.testing3.spec_1 tail.1 b;
+        return _x.2
+      | List.cons head.3 tail.4 =>
+        let _x.5 := Nat.add b b;
+        let x := Nat.add _x.5 s;
+        let _x.6 := Nat.add x i;
+        let x := Nat.add _x.6 head.3;
+        let _x.7 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i tail.1 tail.4 x;
+        return _x.7
 [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 :=
+    def List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 tail.1 s i l b : Nat :=
       cases l : Nat
       | List.nil =>
-        let _x.3 := List.newForIn._at_.testing3.spec_1 _x.1 tail.2 b;
-        return _x.3
-      | List.cons head.4 tail.5 =>
-        let _x.6 := Nat.add b b;
-        let x := Nat.add _x.6 s;
-        let _x.7 := Nat.add x i;
-        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
+        let _x.2 := List.newForIn._at_.testing3.spec_1 tail.1 b;
+        return _x.2
+      | List.cons head.3 tail.4 =>
+        let _x.5 := Nat.add b b;
+        let x := Nat.add _x.5 s;
+        let _x.6 := Nat.add x i;
+        let x := Nat.add _x.6 head.3;
+        let _x.7 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i tail.1 tail.4 x;
+        return _x.7
 [Compiler.saveMono] size: 12
-    def List.newForIn._at_.testing3.spec_1 _x.1 l b : Nat :=
+    def List.newForIn._at_.testing3.spec_1 l b : Nat :=
       cases l : Nat
       | List.nil =>
         return b
-      | List.cons head.2 tail.3 =>
+      | List.cons head.1 tail.2 =>
+        let _x.3 := 1;
         let _x.4 := 10;
-        let _x.5 := Nat.sub _x.4 head.2;
-        let _x.6 := Nat.add _x.5 _x.1;
-        let _x.7 := 1;
-        let _x.8 := Nat.sub _x.6 _x.7;
-        let _x.9 := Nat.add head.2 _x.8;
-        let _x.10 := [] ◾;
-        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
+        let _x.5 := Nat.sub _x.4 head.1;
+        let _x.6 := Nat.add _x.5 _x.3;
+        let _x.7 := Nat.sub _x.6 _x.3;
+        let _x.8 := Nat.add head.1 _x.7;
+        let _x.9 := [] ◾;
+        let _x.10 := List.range'TR.go _x.3 _x.7 _x.8 _x.9;
+        let _x.11 := List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 tail.2 b head.1 _x.10 b;
+        return _x.11
 [Compiler.saveMono] size: 9
     def testing3 : Nat :=
       let x := 42;
@@ -203,7 +203,7 @@ trace: [Compiler.saveMono] size: 9
       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;
+      let _x.8 := List.newForIn._at_.testing3.spec_1 _x.7 x;
       return _x.8
 [Compiler.saveMono] size: 9
     def List.newForIn._at_.testing3.spec_0 s i kcontinue l b : Nat :=
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 7be10d86e6..0cefd9f4ce 100644
--- a/tests/lean/run/do_for_loop_levenstein_compiler_test.lean
+++ b/tests/lean/run/do_for_loop_levenstein_compiler_test.lean
@@ -75,83 +75,87 @@ trace: [Compiler.saveMono] size: 13
           let _x.8 := String.length a;
           let _x.9 := 1;
           let _x.10 := Std.Legacy.Range.mk _x.4 _x.8 _x.9 ◾;
-          let _x.11 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.7 a _x.9 _x.5 _x.10 _x.4 s;
+          let _x.11 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.7 a _x.3 _x.10 _x.4 s;
           return _x.11
         | Bool.true =>
           let _x.12 := Array.reverse._redArg s;
           return _x.12
-[Compiler.saveMono] size: 29
-    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._redArg s' _x.1 _x.2 as sz _x.3 range i a.4 : Array
+[Compiler.saveMono] size: 31
+    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._redArg s' _x.1 as sz _x.2 range i a.3 : Array
       String :=
       cases range : Array String
       | Std.Legacy.Range.mk start stop step step_pos =>
-        let _x.5 := Nat.decLt i stop;
-        cases _x.5 : Array String
+        let _x.4 := Nat.decLt i stop;
+        cases _x.4 : Array String
         | Bool.false =>
-          let _x.6 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz _x.3 a.4;
-          return _x.6
+          let _x.5 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz _x.2 a.3;
+          return _x.5
         | Bool.true =>
-          let _x.7 := Nat.add i step;
-          let _x.8 := 0;
-          let _x.9 := String.utf8ByteSize s';
-          let _x.10 := String.Slice.mk s' _x.8 _x.9 ◾;
-          let _x.11 := @String.Slice.Pos.nextn _x.10 _x.8 i;
-          let _x.12 := @String.extract s' _x.8 _x.11;
-          let _x.13 := Nat.add i _x.1;
-          let _x.14 := @String.Slice.Pos.nextn _x.10 _x.8 _x.13;
-          let _x.15 := @String.extract s' _x.14 _x.9;
-          let d := String.append _x.12 _x.15;
-          jp _jp.16 : Array String :=
-            let out := Array.push ◾ a.4 d;
-            let _x.17 := 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 _x.7 out;
-            return _x.17;
-          let _x.18 := Array.contains._at_.deletions.spec_0 a.4 d;
-          cases _x.18 : Array String
+          let _x.6 := 1;
+          let _x.7 := 0;
+          let _x.8 := Nat.decEq _x.1 _x.7;
+          let _x.9 := Nat.add i step;
+          let _x.10 := String.utf8ByteSize s';
+          let _x.11 := String.Slice.mk s' _x.7 _x.10 ◾;
+          let _x.12 := @String.Slice.Pos.nextn _x.11 _x.7 i;
+          let _x.13 := @String.extract s' _x.7 _x.12;
+          let _x.14 := Nat.add i _x.6;
+          let _x.15 := @String.Slice.Pos.nextn _x.11 _x.7 _x.14;
+          let _x.16 := @String.extract s' _x.15 _x.10;
+          let d := String.append _x.13 _x.16;
+          jp _jp.17 : Array String :=
+            let out := Array.push ◾ a.3 d;
+            let _x.18 := 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 as sz _x.2 range _x.9 out;
+            return _x.18;
+          let _x.19 := Array.contains._at_.deletions.spec_0 a.3 d;
+          cases _x.19 : Array String
           | Bool.false =>
-            goto _jp.16
+            goto _jp.17
           | Bool.true =>
-            cases _x.2 : Array String
+            cases _x.8 : Array String
             | Bool.false =>
-              let _x.19 := 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 _x.7 a.4;
-              return _x.19
+              let _x.20 := 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 as sz _x.2 range _x.9 a.3;
+              return _x.20
             | Bool.true =>
-              goto _jp.16
-[Compiler.saveMono] size: 29
-    def 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 : Array
+              goto _jp.17
+[Compiler.saveMono] size: 31
+    def 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 range i a.3 : Array
       String :=
       cases range : Array String
       | Std.Legacy.Range.mk start stop step step_pos =>
-        let _x.5 := Nat.decLt i stop;
-        cases _x.5 : Array String
+        let _x.4 := Nat.decLt i stop;
+        cases _x.4 : Array String
         | Bool.false =>
-          let _x.6 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz _x.1 a.4;
-          return _x.6
+          let _x.5 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz _x.1 a.3;
+          return _x.5
         | Bool.true =>
-          let _x.7 := Nat.add i step;
-          let _x.8 := 0;
-          let _x.9 := String.utf8ByteSize s';
-          let _x.10 := String.Slice.mk s' _x.8 _x.9 ◾;
-          let _x.11 := @String.Slice.Pos.nextn _x.10 _x.8 i;
-          let _x.12 := @String.extract s' _x.8 _x.11;
-          let _x.13 := Nat.add i _x.2;
-          let _x.14 := @String.Slice.Pos.nextn _x.10 _x.8 _x.13;
-          let _x.15 := @String.extract s' _x.14 _x.9;
-          let d := String.append _x.12 _x.15;
-          jp _jp.16 : Array String :=
-            let out := Array.push ◾ a.4 d;
-            let _x.17 := 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.2 _x.3 as sz _x.1 range _x.7 out;
-            return _x.17;
-          let _x.18 := Array.contains._at_.deletions.spec_0 a.4 d;
-          cases _x.18 : Array String
+          let _x.6 := 1;
+          let _x.7 := 0;
+          let _x.8 := Nat.decEq _x.2 _x.7;
+          let _x.9 := Nat.add i step;
+          let _x.10 := String.utf8ByteSize s';
+          let _x.11 := String.Slice.mk s' _x.7 _x.10 ◾;
+          let _x.12 := @String.Slice.Pos.nextn _x.11 _x.7 i;
+          let _x.13 := @String.extract s' _x.7 _x.12;
+          let _x.14 := Nat.add i _x.6;
+          let _x.15 := @String.Slice.Pos.nextn _x.11 _x.7 _x.14;
+          let _x.16 := @String.extract s' _x.15 _x.10;
+          let d := String.append _x.13 _x.16;
+          jp _jp.17 : Array String :=
+            let out := Array.push ◾ a.3 d;
+            let _x.18 := 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.2 as sz _x.1 range _x.9 out;
+            return _x.18;
+          let _x.19 := Array.contains._at_.deletions.spec_0 a.3 d;
+          cases _x.19 : Array String
           | Bool.false =>
-            goto _jp.16
+            goto _jp.17
           | Bool.true =>
-            cases _x.3 : Array String
+            cases _x.8 : Array String
             | Bool.false =>
-              let _x.19 := 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.2 _x.3 as sz _x.1 range _x.7 a.4;
-              return _x.19
+              let _x.20 := 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.2 as sz _x.1 range _x.9 a.3;
+              return _x.20
             | Bool.true =>
-              goto _jp.16
+              goto _jp.17
 [Compiler.saveMono] size: 15
     def deletions n s : Array String :=
       let zero := 0;
@@ -171,57 +175,57 @@ trace: [Compiler.saveMono] size: 13
         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 :=
+[Compiler.saveMono] size: 31
+    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 kcontinue range i a.2 : Array String :=
       cases range : Array String
       | Std.Legacy.Range.mk start stop step step_pos =>
-        let _x.4 := Nat.decLt i stop;
-        cases _x.4 : Array String
+        let _x.3 := Nat.decLt i stop;
+        cases _x.3 : Array String
         | Bool.false =>
-          let _x.5 := kcontinue a.3;
-          return _x.5
+          let _x.4 := kcontinue a.2;
+          return _x.4
         | Bool.true =>
-          let _x.6 := Nat.add i step;
-          let _x.7 := 0;
-          let _x.8 := String.utf8ByteSize s';
-          let _x.9 := String.Slice.mk s' _x.7 _x.8 ◾;
-          let _x.10 := @String.Slice.Pos.nextn _x.9 _x.7 i;
-          let _x.11 := @String.extract s' _x.7 _x.10;
-          let _x.12 := Nat.add i _x.1;
-          let _x.13 := @String.Slice.Pos.nextn _x.9 _x.7 _x.12;
-          let _x.14 := @String.extract s' _x.13 _x.8;
-          let d := String.append _x.11 _x.14;
-          jp _jp.15 : Array String :=
-            let out := Array.push ◾ a.3 d;
-            let _x.16 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range _x.6 out;
-            return _x.16;
-          let _x.17 := Array.contains._at_.deletions.spec_0 a.3 d;
-          cases _x.17 : Array String
+          let _x.5 := 1;
+          let _x.6 := 0;
+          let _x.7 := Nat.decEq _x.1 _x.6;
+          let _x.8 := Nat.add i step;
+          let _x.9 := String.utf8ByteSize s';
+          let _x.10 := String.Slice.mk s' _x.6 _x.9 ◾;
+          let _x.11 := @String.Slice.Pos.nextn _x.10 _x.6 i;
+          let _x.12 := @String.extract s' _x.6 _x.11;
+          let _x.13 := Nat.add i _x.5;
+          let _x.14 := @String.Slice.Pos.nextn _x.10 _x.6 _x.13;
+          let _x.15 := @String.extract s' _x.14 _x.9;
+          let d := String.append _x.12 _x.15;
+          jp _jp.16 : Array String :=
+            let out := Array.push ◾ a.2 d;
+            let _x.17 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 kcontinue range _x.8 out;
+            return _x.17;
+          let _x.18 := Array.contains._at_.deletions.spec_0 a.2 d;
+          cases _x.18 : Array String
           | Bool.false =>
-            goto _jp.15
+            goto _jp.16
           | Bool.true =>
-            cases _x.2 : Array String
+            cases _x.7 : Array String
             | Bool.false =>
-              let _x.18 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range _x.6 a.3;
-              return _x.18
+              let _x.19 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 kcontinue range _x.8 a.2;
+              return _x.19
             | Bool.true =>
-              goto _jp.15
+              goto _jp.16
 [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
+    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1 s' _x.1 kcontinue range this i hs hl a.2 : Array String :=
+      let _x.3 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 kcontinue range i a.2;
+      return _x.3
+[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 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;
+      let _x.4 := 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 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
+    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 as sz _x.2 range this i hs hl a.3 : 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
+      let _x.4 := 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 as sz _x.2 range i a.3;
+      return _x.4
 -/
 #guard_msgs in
 set_option trace.Compiler.saveMono true in