diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 19f9b99aa1..76be4f57b1 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -1084,6 +1084,12 @@ theorem getLast?_tail {l : List α} : (tail l).getLast? = if l.length = 1 then n
     rw [if_neg]
     rintro ⟨⟩
 
+@[simp, grind =]
+theorem cons_head_tail (h : l ≠ []) : l.head h :: l.tail = l := by
+  induction l with
+  | nil => contradiction
+  | cons ih => simp_all
+
 /-! ## Basic operations -/
 
 /-! ### map -/
diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean
index bb41869407..f8e04b97fd 100644
--- a/src/Std/Do/Triple/SpecLemmas.lean
+++ b/src/Std/Do/Triple/SpecLemmas.lean
@@ -31,6 +31,35 @@ end Std.Range
 
 namespace List
 
+@[ext]
+structure Cursor {α : Type u} (l : List α) : Type u where
+  «prefix» : List α
+  suffix : List α
+  property : «prefix» ++ suffix = l
+
+def Cursor.at (l : List α) (n : Nat) : Cursor l := ⟨l.take n, l.drop n, by simp⟩
+abbrev Cursor.begin (l : List α) : Cursor l := .at l 0
+abbrev Cursor.end (l : List α) : Cursor l := .at l l.length
+
+def Cursor.current {α} {l : List α} (c : Cursor l) (h : 0 < c.suffix.length := by get_elem_tactic) : α :=
+  c.suffix[0]'(by simp [h])
+
+def Cursor.tail (s : Cursor l) (h : 0 < s.suffix.length := by get_elem_tactic) : Cursor l :=
+  { «prefix» := s.prefix ++ [s.current]
+  , suffix := s.suffix.tail
+  , property := by
+      have : s.suffix ≠ [] := by simp only [List.ne_nil_iff_length_pos, h]
+      simp [current, ←List.head_eq_getElem this, s.property] }
+
+@[simp, grind =] theorem Cursor.prefix_at (l : List α) : (Cursor.at l n).prefix = l.take n := rfl
+@[simp, grind =] theorem Cursor.suffix_at (l : List α) : (Cursor.at l n).suffix = l.drop n := rfl
+@[simp, grind =] theorem Cursor.current_at (l : List α) (h : n < l.length) :
+    (Cursor.at l n).current  (by simpa using Nat.sub_lt_sub_right (Nat.le_refl n) h) = l[n] := by
+  induction n with simp_all [Cursor.current]
+@[simp, grind =] theorem Cursor.tail_at (l : List α) (h : n < l.length) :
+    (Cursor.at l n).tail (by simpa using Nat.sub_lt_sub_right (Nat.le_refl n) h) = Cursor.at l (n + 1) := by
+  simp [Cursor.tail, Cursor.at, Cursor.current]
+
 @[grind →]
 theorem eq_of_range'_eq_append_cons (h : range' s n step = xs ++ cur :: ys) :
     cur = s + step * xs.length := by
@@ -71,24 +100,6 @@ theorem lt_of_range'_eq_append_cons (h : range' s n step = xs ++ i :: ys) (hstep
 
 end List
 
-namespace Std.List
-
-@[ext]
-structure Zipper {α : Type u} (l : List α) : Type u where
-  rpref : List α
-  suff : List α
-  property : rpref.reverse ++ suff = l
-
-@[simp]
-abbrev Zipper.pref {α} {l : List α} (s : List.Zipper l) : List α := s.rpref.reverse
-
-abbrev Zipper.begin (l : List α) : Zipper l := ⟨[],l,rfl⟩
-abbrev Zipper.end (l : List α) : Zipper l := ⟨l.reverse,[],by simp⟩
-abbrev Zipper.tail (s : Zipper l) (h : s.suff = hd::tl) : Zipper l :=
-  { rpref := hd::s.rpref, suff := tl, property := by simp [s.property, ←h] }
-
-end Std.List
-
 namespace Std.Do
 
 -- We override the `Triple` notation in `Std.Do.Triple.Basic` just in this module.
@@ -339,7 +350,7 @@ theorem Spec.tryCatch_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q :
 The type of loop invariants used by the specifications of `for ... in ...` loops.
 A loop invariant is a `PostCond` that takes as parameters
 
-* A `List.Zipper xs` representing the iteration state of the loop. It is parameterized by the list
+* A `List.Cursor xs` representing the iteration state of the loop. It is parameterized by the list
   of elements `xs` that the `for` loop iterates over.
 * A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of
   `let mut` variables and early return.
@@ -351,7 +362,7 @@ During the induction step, the invariant holds for a suffix with head element `x
 After running the loop body, the invariant then holds after shifting `x` to the prefix.
 -/
 abbrev Invariant {α : Type u} (xs : List α) (β : Type u) (ps : PostShape) :=
-  PostCond (List.Zipper xs × β) ps
+  PostCond (List.Cursor xs × β) ps
 
 /--
 Helper definition for specifying loop invariants for loops with early return.
@@ -365,20 +376,20 @@ It is `none` as long as there was no early return and `some r` if the loop retur
 
 This function allows to specify different invariants for the loop body depending on whether the loop
 terminated early or not. When there was an early return, the loop has effectively finished, which is
-encoded by the additional `⌜xs.suff = []⌝` assertion in the invariant. This assertion is vital for
+encoded by the additional `⌜xs.suffix = []⌝` assertion in the invariant. This assertion is vital for
 successfully proving the induction step, as it contradicts with the assumption that
-`xs.suff = x::rest` of the inductive hypothesis at the start of the loop body, meaning that users
+`xs.suffix = x::rest` of the inductive hypothesis at the start of the loop body, meaning that users
 won't need to prove anything about the bogus case where the loop has returned early yet takes
 another iteration of the loop body.
 -/
 abbrev Invariant.withEarlyReturn
-  (onContinue : List.Zipper xs → β → Assertion ps)
+  (onContinue : List.Cursor xs → β → Assertion ps)
   (onReturn : γ → β → Assertion ps)
   (onExcept : ExceptConds ps := ExceptConds.false) :
     Invariant xs (MProd (Option γ) β) ps :=
   ⟨fun ⟨xs, x, b⟩ => spred(
         (⌜x = none⌝ ∧ onContinue xs b)
-      ∨ (∃ r, ⌜x = some r⌝ ∧ ⌜xs.suff = []⌝ ∧ onReturn r b)),
+      ∨ (∃ r, ⌜x = some r⌝ ∧ ⌜xs.suffix = []⌝ ∧ onReturn r b)),
    onExcept⟩
 
 @[spec]
@@ -386,32 +397,32 @@ theorem Spec.forIn'_list {α β : Type u}
     [Monad m] [WPMonad m ps]
     {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
     (inv : Invariant xs β ps)
-    (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
-        f x hx b
+    (step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b,
+        ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
+        f cur (by simp [h]) b
         ⦃(fun r => match r with
-                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
-                   | .done b' => inv.1 (⟨xs.reverse, [], by simp⟩, b'), inv.2)}) :
-    ⦃inv.1 (⟨[], xs, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp⟩, b), inv.2)} := by
-  suffices h : ∀ rpref suff (h : xs = rpref.reverse ++ suff),
-      ⦃inv.1 (⟨rpref, suff, by simp [h]⟩, init)}
-      forIn' (m:=m) suff init (fun a ha => f a (by simp[h,ha]))
-      ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp [h]⟩, b), inv.2)}
-    from h [] xs rfl
-  intro rpref suff h
-  induction suff generalizing rpref init
-  case nil => apply Triple.pure; simp [h]
+                   | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)} := by
+  suffices h : ∀ c,
+      ⦃inv.1 (c, init)}
+      forIn' (m:=m) c.suffix init (fun a ha => f a (by simp [←c.property, ha]))
+      ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)}
+    from h ⟨[], xs, rfl⟩
+  rintro ⟨pref, suff, h⟩
+  induction suff generalizing pref init
+  case nil => apply Triple.pure; simp [←h]
   case cons x suff ih =>
     simp only [List.forIn'_cons]
     apply Triple.bind
-    case hx => exact step init rpref x (by simp[h]) suff h
+    case hx => exact step _ _ _ h.symm init
     case hf =>
       intro r
       split
-      next => apply Triple.pure; simp [h]
+      next => apply Triple.pure; simp
       next b =>
         simp
-        have := @ih b (x::rpref) (by simp [h])
+        have := @ih b (pref ++ [x]) (by simp [h])
         simp at this
         exact this
 
@@ -425,22 +436,22 @@ theorem Spec.forIn'_list_const_inv {α β : Type u}
         f x hx b
         ⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)}) :
     ⦃inv.1 init} forIn' xs init f ⦃inv} :=
-  Spec.forIn'_list (fun p => inv.1 p.2, inv.2) (fun b _ x hx _ _ => step x hx b)
+  Spec.forIn'_list (fun p => inv.1 p.2, inv.2) (fun _p c _s h b => step c (by simp [h]) b)
 
 @[spec]
 theorem Spec.forIn_list {α β : Type u}
     [Monad m] [WPMonad m ps]
     {xs : List α} {init : β} {f : α → β → m (ForInStep β)}
     (inv : Invariant xs β ps)
-    (step : ∀ b rpref x suff (h : xs = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
-        f x b
+    (step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b,
+        ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
+        f cur b
         ⦃(fun r => match r with
-                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
-                   | .done b' => inv.1 (⟨xs.reverse, [], by simp⟩, b'), inv.2)}) :
-    ⦃inv.1 (⟨[], xs, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp⟩, b), inv.2)} := by
+                   | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)} := by
   simp only [← forIn'_eq_forIn]
-  exact Spec.forIn'_list inv (fun b rpref x _ suff h => step b rpref x suff h)
+  exact Spec.forIn'_list inv step
 
 -- using the postcondition as a constant invariant:
 theorem Spec.forIn_list_const_inv {α β : Type u}
@@ -452,18 +463,18 @@ theorem Spec.forIn_list_const_inv {α β : Type u}
         f hd b
         ⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)}) :
     ⦃inv.1 init} forIn xs init f ⦃inv} :=
-  Spec.forIn_list (fun p => inv.1 p.2, inv.2) (fun b _ hd _ _ => step hd b)
+  Spec.forIn_list (fun p => inv.1 p.2, inv.2) (fun _p c _s _h b => step c b)
 
 @[spec]
 theorem Spec.foldlM_list {α β : Type u}
     [Monad m] [WPMonad m ps]
     {xs : List α} {init : β} {f : β → α → m β}
     (inv : Invariant xs β ps)
-    (step : ∀ b rpref x suff (h : xs = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
-        f b x
-        ⦃(fun b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b'), inv.2)}) :
-    ⦃inv.1 (⟨[], xs, by simp⟩, init)} List.foldlM f init xs ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp⟩, b), inv.2)} := by
+    (step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b,
+        ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
+        f b cur
+        ⦃(fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs, rfl⟩, init)} List.foldlM f init xs ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)} := by
   have : xs.foldlM f init = forIn xs init (fun a b => .yield <$> f b a) := by
     simp only [List.forIn_yield_eq_foldlM, id_map']
   rw[this]
@@ -481,35 +492,35 @@ theorem Spec.foldlM_list_const_inv {α β : Type u}
         f b hd
         ⦃(fun b' => inv.1 b', inv.2)}) :
   ⦃inv.1 init} List.foldlM f init xs ⦃inv} :=
-    Spec.foldlM_list (fun p => inv.1 p.2, inv.2) (fun b _ hd _ _ => step hd b)
+    Spec.foldlM_list (fun p => inv.1 p.2, inv.2) (fun _p c _s _h b => step c b)
 
 @[spec]
 theorem Spec.forIn'_range {β : Type} {m : Type → Type v} {ps : PostShape}
     [Monad m] [WPMonad m ps]
     {xs : Std.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
     (inv : Invariant xs.toList β ps)
-    (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
-        f x hx b
+    (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
+        ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
+        f cur (by simp [Std.Range.mem_of_mem_range', h]) b
         ⦃(fun r => match r with
-                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
-                   | .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
-    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
+                   | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
   simp only [Std.Range.forIn'_eq_forIn'_range', Std.Range.size, Std.Range.size.eq_1]
-  apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (Std.Range.mem_of_mem_range' hx) suff h)
+  apply Spec.forIn'_list inv (fun c hcur b => step c hcur b)
 
 @[spec]
 theorem Spec.forIn_range {β : Type} {m : Type → Type v} {ps : PostShape}
     [Monad m] [WPMonad m ps]
     {xs : Std.Range} {init : β} {f : Nat → β → m (ForInStep β)}
     (inv : Invariant xs.toList β ps)
-    (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
-        f x b
+    (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
+        ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
+        f cur b
         ⦃(fun r => match r with
-                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
-                   | .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
-    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
+                   | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
   simp only [Std.Range.forIn_eq_forIn_range', Std.Range.size]
   apply Spec.forIn_list inv step
 
@@ -523,15 +534,15 @@ theorem Spec.forIn'_prange {α β : Type u}
     [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
     {xs : PRange ⟨sl, su⟩ α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
     (inv : Invariant xs.toList β ps)
-    (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
-        f x hx b
+    (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
+        ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
+        f cur (by simp [←mem_toList_iff_mem, h]) b
         ⦃(fun r => match r with
-                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
-                   | .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
-    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
+                   | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
   simp only [forIn'_eq_forIn'_toList]
-  apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (mem_toList_iff_mem.mp hx) suff h)
+  apply Spec.forIn'_list inv step
 
 open Std.PRange in
 @[spec]
@@ -543,44 +554,44 @@ theorem Spec.forIn_prange {α β : Type u}
     [LawfulUpwardEnumerableLowerBound sl α] [LawfulUpwardEnumerableUpperBound su α]
     {xs : PRange ⟨sl, su⟩ α} {init : β} {f : α → β → m (ForInStep β)}
     (inv : Invariant xs.toList β ps)
-    (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
-        f x b
+    (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
+        ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
+        f cur b
         ⦃(fun r => match r with
-                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
-                   | .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
-    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
+                   | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
   simp only [forIn]
-  apply Spec.forIn'_prange inv (fun b rpref x _hx suff h => step b rpref x suff h)
+  apply Spec.forIn'_prange inv step
 
 @[spec]
 theorem Spec.forIn'_array {α β : Type u}
     [Monad m] [WPMonad m ps]
     {xs : Array α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
     (inv : Invariant xs.toList β ps)
-    (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
-        f x hx b
+    (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
+        ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
+        f cur (by simp [←Array.mem_toList_iff, h]) b
         ⦃(fun r => match r with
-                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
-                   | .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
-    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
+                   | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
   cases xs
   simp
-  apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (by simp[hx]) suff h)
+  apply Spec.forIn'_list inv step
 
 @[spec]
 theorem Spec.forIn_array {α β : Type u}
     [Monad m] [WPMonad m ps]
     {xs : Array α} {init : β} {f : α → β → m (ForInStep β)}
     (inv : Invariant xs.toList β ps)
-    (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
-        f x b
+    (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
+        ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
+        f cur b
         ⦃(fun r => match r with
-                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
-                   | .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
-    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
+                   | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
   cases xs
   simp
   apply Spec.forIn_list inv step
@@ -590,11 +601,11 @@ theorem Spec.foldlM_array {α β : Type u}
     [Monad m] [WPMonad m ps]
     {xs : Array α} {init : β} {f : β → α → m β}
     (inv : Invariant xs.toList β ps)
-    (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
-        f b x
-        ⦃(fun b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b'), inv.2)}) :
-    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} Array.foldlM f init xs ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
+    (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b,
+        ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)}
+        f b cur
+          ⦃(fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} Array.foldlM f init xs ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by
   cases xs
   simp
   apply Spec.foldlM_list inv step
diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean
index fed4518f76..c0eb4c0e2a 100644
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@@ -160,7 +160,10 @@ macro (name := mleave) "mleave" : tactic =>
               $(mkIdent ``Std.Do.ExceptConds.entails_false):term,
               $(mkIdent ``ULift.down_ite):term,
               $(mkIdent ``ULift.down_dite):term,
-              $(mkIdent ``Std.List.Zipper.pref):term,
+              $(mkIdent ``List.Cursor.prefix_at):term,
+              $(mkIdent ``List.Cursor.suffix_at):term,
+              $(mkIdent ``List.Cursor.current_at):term,
+              $(mkIdent ``List.Cursor.tail_at):term,
               $(mkIdent ``and_imp):term,
               $(mkIdent ``and_true):term,
               $(mkIdent ``dite_eq_ite):term,
diff --git a/tests/lean/run/bhaviksSampler.lean b/tests/lean/run/bhaviksSampler.lean
index 89621f4fe7..9275995a1c 100644
--- a/tests/lean/run/bhaviksSampler.lean
+++ b/tests/lean/run/bhaviksSampler.lean
@@ -152,16 +152,16 @@ theorem sampler_correct {m : Type → Type u} {k h} [Monad m] [WPMonad m ps] :
   sampler (m:=m) n k h
   ⦃⇓ xs => ⌜xs.toList.Nodup⌝⦄ := by
   mvcgen -leave [sampler]
-  case inv1 => exact (⇓ (xs, midway) => ⌜Midway.valid midway xs.rpref.length⌝)
-  case vc1 rpref x _ _ _ _ _ _ r _ _ _ =>
+  case inv1 => exact (⇓ (xs, midway) => ⌜Midway.valid midway xs.prefix.length⌝)
+  case vc1 pref cur _ _ _ _ _ _ r _ _ _ =>
     dsimp
     mframe
     rename_i hinv
     mpure_intro
-    change Midway.valid (next _ x _ r.val) (rpref.length + 1)
-    have : x = rpref.length := sorry -- by grind -- wishful thinking :(
+    simp only [List.length_append, List.length_cons, List.length_nil, Nat.zero_add]
+    have : cur = pref.length := sorry -- by grind -- wishful thinking :(
     subst this
-    apply Midway.valid_next _ rpref.length _ r.val r.property.1 r.property.2 hinv
+    apply Midway.valid_next _ pref.length _ r.val r.property.1 r.property.2 hinv
   case vc2 =>
     mpure_intro
     exact valid_init
diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean
index bbf6045a29..b1ba3df437 100644
--- a/tests/lean/run/doLogicTests.lean
+++ b/tests/lean/run/doLogicTests.lean
@@ -87,7 +87,7 @@ theorem sum_loop_spec :
   mintro -
   unfold sum_loop
   mspec
-  case inv => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
+  case inv => exact (⇓ (xs, r) => ⌜(∀ x ∈ xs.suffix, x ≤ 5) ∧ r + xs.suffix.length * 5 ≤ 25⌝)
   all_goals simp_all +decide; try omega
   intros
   mintro _
@@ -136,11 +136,11 @@ theorem mkFreshPair_spec_no_eta :
   mspec
   intro _; simp_all
 
-example : PostCond (Nat × Std.List.Zipper (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
-  ⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝, ()⟩
+example : PostCond (Nat × List.Cursor (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
+  ⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝, ()⟩
 
-example : PostCond (Nat × Std.List.Zipper (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
-  post⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
+example : PostCond (Nat × List.Cursor (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
+  post⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
 
 theorem throwing_loop_spec :
   ⦃fun s => ⌜s = 4⌝⦄
@@ -152,7 +152,7 @@ theorem throwing_loop_spec :
   mspec
   mspec
   mspec
-  case inv => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
+  case inv => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
   case post.success =>
     mspec
     mspec
@@ -178,7 +178,7 @@ theorem beaking_loop_spec :
   dsimp only [breaking_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift]
   mspec
   mspec
-  case inv => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
+  case inv => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.prefix.sum ∨ r > 4) ∧ s = 42⌝)
   all_goals simp_all
   case post => grind
   case step =>
@@ -196,7 +196,7 @@ theorem returning_loop_spec :
   dsimp only [returning_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift]
   mspec
   mspec
-  case inv => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
+  case inv => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.prefix.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
   all_goals simp_all [-SPred.entails_1]
   case post =>
     split
@@ -235,8 +235,8 @@ theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n
   if h : n = 0 then simp [h] else
   simp only [h, reduceIte]
   mspec -- Spec.pure
-  mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) ?step
-  case step => dsimp; intros; mintro _; simp_all
+  mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝) ?step
+  case step => intros; mintro _; simp_all
   simp_all [Nat.sub_one_add_one]
 
 theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
@@ -246,8 +246,8 @@ theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_sp
   mintro -
   simp only [fib_impl, h, reduceIte]
   mspec
-  mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) ?step
-  case step => dsimp; intros; mintro _; mspec; mspec; simp_all
+  mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝) ?step
+  case step => intros; mintro _; mspec; mspec; simp_all
   simp_all [Nat.sub_one_add_one]
 
 theorem fib_impl_vcs
@@ -255,10 +255,10 @@ theorem fib_impl_vcs
     (I : (n : Nat) → (_ : ¬n = 0) →
       Invariant [1:n].toList (MProd Nat Nat) PostShape.pure)
     (ret : ⊢ₛ (Q 0).1 0)
-    (loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 ⟨Std.List.Zipper.begin _, 0, 1⟩)
-    (loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 ⟨Std.List.Zipper.end _, r⟩ ⊢ₛ (Q n).1 r.2)
-    (loop_step : ∀ n (hn : ¬n = 0) r rpref x suff (h : [1:n].toList = rpref.reverse ++ x :: suff),
-                  (I n hn).1 ⟨⟨rpref, x::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨x::rpref, suff, by simp[h]⟩, r.2, r.1+r.2⟩)
+    (loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 ⟨⟨[], [1:n].toList, rfl⟩, 0, 1⟩)
+    (loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 ⟨⟨[1:n].toList, [], by simp⟩, r⟩ ⊢ₛ (Q n).1 r.2)
+    (loop_step : ∀ n (hn : ¬n = 0) r pref cur suff (h : [1:n].toList = pref ++ cur :: suff),
+                  (I n hn).1 ⟨⟨pref, cur::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨pref ++ [cur], suff, by simp[h]⟩, r.2, r.1+r.2⟩)
     : ⊢ₛ wp⟦fib_impl n⟧ (Q n) := by
   apply fib_impl.fun_cases n _ ?case1 ?case2
   case case1 => intro h; simp only [fib_impl, h, ↓reduceIte]; mstart; mspec
@@ -279,7 +279,7 @@ theorem fib_impl_vcs
 
 theorem fib_triple_vcs : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
   apply fib_impl_vcs
-  case I => intro n hn; exact (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝)
+  case I => intro n hn; exact (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝)
   case ret => mpure_intro; rfl
   case loop_pre => intros; mpure_intro; trivial
   case loop_post => simp_all [Nat.sub_one_add_one]
@@ -394,14 +394,14 @@ theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n
   unfold fib_impl
   mvcgen
   case inv1 => exact ⇓ (xs, ⟨a, b⟩) =>
-    ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝
+    ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝
   all_goals simp_all +zetaDelta [Nat.sub_one_add_one]
 
 theorem fib_triple_step : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
   unfold fib_impl
   mvcgen (stepLimit := some 14) -- 13 still has a wp⟦·⟧
   case inv1 => exact ⇓ ⟨xs, a, b⟩ =>
-    ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝
+    ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝
   all_goals simp_all +zetaDelta [Nat.sub_one_add_one]
 
 attribute [local spec] fib_triple in
@@ -419,10 +419,10 @@ theorem fib_impl_vcs
     (I : (n : Nat) → (_ : ¬n = 0) →
       Invariant [1:n].toList (MProd Nat Nat) PostShape.pure)
     (ret : ⊢ₛ (Q 0).1 0)
-    (loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 ⟨Std.List.Zipper.begin _, 0, 1⟩)
-    (loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 ⟨Std.List.Zipper.end _, r⟩ ⊢ₛ (Q n).1 r.2)
-    (loop_step : ∀ n (hn : ¬n = 0) r rpref x suff (h : [1:n].toList = rpref.reverse ++ x :: suff),
-                  (I n hn).1 ⟨⟨rpref, x::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨x::rpref, suff, by simp[h]⟩, r.2, r.1+r.2⟩)
+    (loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 ⟨⟨[], [1:n].toList, rfl⟩, 0, 1⟩)
+    (loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 ⟨⟨[1:n].toList, [], by simp⟩, r⟩ ⊢ₛ (Q n).1 r.2)
+    (loop_step : ∀ n (hn : ¬n = 0) r pref cur suff (h : [1:n].toList = pref ++ cur :: suff),
+                  (I n hn).1 ⟨⟨pref, cur::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨pref ++ [cur], suff, by simp[h]⟩, r.2, r.1+r.2⟩)
     : ⊢ₛ wp⟦fib_impl n⟧ (Q n) := by
   unfold fib_impl
   mvcgen
@@ -467,7 +467,7 @@ theorem sum_loop_spec :
   -- cf. `ByHand.sum_loop_spec`
   mintro -
   mvcgen [sum_loop]
-  case inv1 => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
+  case inv1 => exact (⇓ (xs, r) => ⌜r + xs.suffix.length * 5 ≤ 25⌝)
   all_goals simp_all; try grind
 
 theorem throwing_loop_spec :
@@ -476,7 +476,7 @@ theorem throwing_loop_spec :
   ⦃post⟨fun _ _ => ⌜False⌝,
         fun e s => ⌜e = 42 ∧ s = 4⌝⟩⦄ := by
   mvcgen [throwing_loop]
-  case inv1 => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝,
+  case inv1 => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝,
                          fun e s => ⌜e = 42 ∧ s = 4⌝⟩
   all_goals mleave; try (subst_vars; grind)
 
@@ -485,7 +485,7 @@ theorem test_loop_break :
   breaking_loop
   ⦃⇓ r s => ⌜r > 4 ∧ s = 1⌝⦄ := by
   mvcgen [breaking_loop]
-  case inv1 => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
+  case inv1 => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.prefix.sum ∨ r > 4) ∧ s = 42⌝)
   all_goals mleave; try grind
 
 theorem test_loop_early_return :
@@ -493,7 +493,7 @@ theorem test_loop_early_return :
   returning_loop
   ⦃⇓ r s => ⌜r = 42 ∧ s = 4⌝⦄ := by
   mvcgen [returning_loop]
-  case inv1 => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
+  case inv1 => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.prefix.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
   all_goals simp_all; try grind
 
 theorem unfold_to_expose_match_spec :
@@ -521,7 +521,7 @@ theorem test_sum :
     pure (f := Id) x
   ⦃⇓r => ⌜r < 30⌝⦄ := by
   mvcgen
-  case inv1 => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
+  case inv1 => exact (⇓ (xs, r) => ⌜r + xs.suffix.length * 5 ≤ 25⌝)
   all_goals simp_all; try grind
 
 /--
@@ -555,7 +555,7 @@ example (p : Nat → Prop) [DecidablePred p] (n : Nat) :
   case inv1 =>
     exact Invariant.withEarlyReturn
       (onReturn := fun ret _ => ⌜ret = false ∧ ¬ ∀ i < n, p i⌝)
-      (onContinue := fun xs _ => ⌜∀ i, i ∈ xs.pref → p i⌝)
+      (onContinue := fun xs _ => ⌜∀ i, i ∈ xs.prefix → p i⌝)
   all_goals simp_all [-Classical.not_forall]; try grind
 
 end Automated
@@ -704,7 +704,7 @@ def max_and_sum (xs : Array Nat) : Id (Nat × Nat) := do
 theorem max_and_sum_spec (xs : Array Nat) :
     ⦃⌜∀ i, (h : i < xs.size) → xs[i] ≥ 0⌝⦄ max_and_sum xs ⦃⇓ (m, s) => ⌜s ≤ m * xs.size⌝⦄ := by
   mvcgen [max_and_sum]
-  case inv1 => exact (⇓ ⟨xs, m, s⟩ => ⌜s ≤ m * xs.rpref.length⌝)
+  case inv1 => exact (⇓ ⟨xs, m, s⟩ => ⌜s ≤ m * xs.prefix.length⌝)
   all_goals simp_all
   · rw [Nat.left_distrib]
     simp +zetaDelta only [Nat.mul_one, Nat.add_le_add_iff_right]
@@ -851,20 +851,20 @@ theorem naive_expo_correct (x n : Nat) : naive_expo x n = x^n := by
   generalize h : naive_expo x n = r
   apply Id.of_wp_run_eq h
   mvcgen
-  case inv1 => exact ⇓⟨xs, r⟩ => ⌜r = x^xs.rpref.length⌝
+  case inv1 => exact ⇓⟨xs, r⟩ => ⌜r = x^xs.prefix.length⌝
   all_goals simp_all [Nat.pow_add_one]
 
 theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
   generalize h : fast_expo x n = r
   apply Id.of_wp_run_eq h
   mvcgen
-  case inv1 => exact ⇓⟨xs, e, x', y⟩ => ⌜x' ^ e * y = x ^ n ∧ e ≤ n - xs.rpref.length⌝
+  case inv1 => exact ⇓⟨xs, e, x', y⟩ => ⌜x' ^ e * y = x ^ n ∧ e ≤ n - xs.prefix.length⌝
   all_goals simp_all
-  case vc1 b _ _ _ _ _ _ _ _ _ _ ih =>
+  case vc1 b _ _ _ _ _ _ ih =>
     obtain ⟨e, y, x'⟩ := b
     subst_vars
     grind
-  case vc2 b _ _ _ _ _ _ _ _ _ _ ih _ =>
+  case vc2 b _ _ _ _ _ _ ih _ =>
     obtain ⟨e, y, x'⟩ := b
     simp at *
     constructor
@@ -872,7 +872,7 @@ theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
       have : e - 1 + 1 = e := by grind
       rw [this]
     · grind
-  case vc3 b _ _ _ _ _ _ _ _ _ _ ih _ =>
+  case vc3 b _ _ _ _ _ _ ih _ =>
     obtain ⟨e, y, x'⟩ := b
     simp at *
     constructor
@@ -909,7 +909,7 @@ theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by
     exact Invariant.withEarlyReturn
       (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
       (onContinue := fun traversalState seen =>
-        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.pref) ∧ traversalState.pref.Nodup⌝)
+        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
   all_goals mleave; grind
 
 theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by
diff --git a/tests/lean/run/pairsSumToZero.lean b/tests/lean/run/pairsSumToZero.lean
index c996f94b46..810e7dd64d 100644
--- a/tests/lean/run/pairsSumToZero.lean
+++ b/tests/lean/run/pairsSumToZero.lean
@@ -75,7 +75,7 @@ theorem pairsSumToZero_correct (l : List Int) : pairsSumToZero l ↔ l.ExistsPai
     exact Invariant.withEarlyReturn
       (onReturn := fun r b => ⌜r = true ∧ l.ExistsPair (fun a b => a + b = 0)⌝)
       (onContinue := fun traversalState seen =>
-        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.rpref) ∧ ¬traversalState.pref.ExistsPair (fun a b => a + b = 0)⌝)
+        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ ¬traversalState.prefix.ExistsPair (fun a b => a + b = 0)⌝)
 
   all_goals simp_all <;> grind