From d6efe5bd2878135bf1fc3fc31fec66322c5b8a86 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Mar 2024 04:52:36 +0100
Subject: Update the demo

---
 tests/coq/demo/Demo.v           | 48 ++++++++++++++++++++++++++++++++---------
 tests/fstar/demo/Demo.fst       | 45 +++++++++++++++++++++++++++++---------
 tests/lean/Demo/Demo.lean       | 47 +++++++++++++++++++++++++++++++---------
 tests/lean/Demo/Properties.lean | 16 ++++++++++++++
 4 files changed, 126 insertions(+), 30 deletions(-)

(limited to 'tests')

diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index ec7ca29d..48067c02 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -34,8 +34,14 @@ Definition use_mul2_add1 (x : u32) (y : u32) : result u32 :=
 Definition incr (x : u32) : result u32 :=
   u32_add x 1%u32.
 
+(** [demo::use_incr]:
+    Source: 'src/demo.rs', lines 25:0-25:17 *)
+Definition use_incr : result unit :=
+  i <- incr 0%u32; i1 <- incr i; _ <- incr i1; Return tt
+.
+
 (** [demo::CList]
-    Source: 'src/demo.rs', lines 27:0-27:17 *)
+    Source: 'src/demo.rs', lines 34:0-34:17 *)
 Inductive CList_t (T : Type) :=
 | CList_CCons : T -> CList_t T -> CList_t T
 | CList_CNil : CList_t T
@@ -45,7 +51,7 @@ Arguments CList_CCons { _ }.
 Arguments CList_CNil { _ }.
 
 (** [demo::list_nth]:
-    Source: 'src/demo.rs', lines 32:0-32:56 *)
+    Source: 'src/demo.rs', lines 39:0-39:56 *)
 Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
   match n with
   | O => Fail_ OutOfFuel
@@ -61,7 +67,7 @@ Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
 .
 
 (** [demo::list_nth_mut]:
-    Source: 'src/demo.rs', lines 47:0-47:68 *)
+    Source: 'src/demo.rs', lines 54:0-54:68 *)
 Fixpoint list_nth_mut
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -89,7 +95,7 @@ Fixpoint list_nth_mut
 .
 
 (** [demo::list_nth_mut1]: loop 0:
-    Source: 'src/demo.rs', lines 62:0-71:1 *)
+    Source: 'src/demo.rs', lines 69:0-78:1 *)
 Fixpoint list_nth_mut1_loop
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -116,7 +122,7 @@ Fixpoint list_nth_mut1_loop
 .
 
 (** [demo::list_nth_mut1]:
-    Source: 'src/demo.rs', lines 62:0-62:77 *)
+    Source: 'src/demo.rs', lines 69:0-69:77 *)
 Definition list_nth_mut1
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -125,7 +131,7 @@ Definition list_nth_mut1
 .
 
 (** [demo::i32_id]:
-    Source: 'src/demo.rs', lines 73:0-73:28 *)
+    Source: 'src/demo.rs', lines 80:0-80:28 *)
 Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -136,8 +142,30 @@ Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
   end
 .
 
+(** [demo::list_tail]:
+    Source: 'src/demo.rs', lines 88:0-88:64 *)
+Fixpoint list_tail
+  (T : Type) (n : nat) (l : CList_t T) :
+  result ((CList_t T) * (CList_t T -> result (CList_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons t tl =>
+      p <- list_tail T n1 tl;
+      let (c, list_tail_back) := p in
+      let back_'a :=
+        fun (ret : CList_t T) =>
+          tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in
+      Return (c, back_'a)
+    | CList_CNil => Return (CList_CNil, Return)
+    end
+  end
+.
+
 (** Trait declaration: [demo::Counter]
-    Source: 'src/demo.rs', lines 83:0-83:17 *)
+    Source: 'src/demo.rs', lines 97:0-97:17 *)
 Record Counter_t (Self : Type) := mkCounter_t {
   Counter_t_incr : Self -> result (usize * Self);
 }.
@@ -146,19 +174,19 @@ Arguments mkCounter_t { _ }.
 Arguments Counter_t_incr { _ }.
 
 (** [demo::{(demo::Counter for usize)}::incr]:
-    Source: 'src/demo.rs', lines 88:4-88:31 *)
+    Source: 'src/demo.rs', lines 102:4-102:31 *)
 Definition counterUsize_incr (self : usize) : result (usize * usize) :=
   self1 <- usize_add self 1%usize; Return (self, self1)
 .
 
 (** Trait implementation: [demo::{(demo::Counter for usize)}]
-    Source: 'src/demo.rs', lines 87:0-87:22 *)
+    Source: 'src/demo.rs', lines 101:0-101:22 *)
 Definition CounterUsize : Counter_t usize := {|
   Counter_t_incr := counterUsize_incr;
 |}.
 
 (** [demo::use_counter]:
-    Source: 'src/demo.rs', lines 95:0-95:59 *)
+    Source: 'src/demo.rs', lines 109:0-109:59 *)
 Definition use_counter
   (T : Type) (counterInst : Counter_t T) (cnt : T) : result (usize * T) :=
   counterInst.(Counter_t_incr) cnt
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index d13d2ba3..5651b80f 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -28,14 +28,19 @@ let use_mul2_add1 (x : u32) (y : u32) : result u32 =
 let incr (x : u32) : result u32 =
   u32_add x 1
 
+(** [demo::use_incr]:
+    Source: 'src/demo.rs', lines 25:0-25:17 *)
+let use_incr : result unit =
+  let* i = incr 0 in let* i1 = incr i in let* _ = incr i1 in Return ()
+
 (** [demo::CList]
-    Source: 'src/demo.rs', lines 27:0-27:17 *)
+    Source: 'src/demo.rs', lines 34:0-34:17 *)
 type cList_t (t : Type0) =
 | CList_CCons : t -> cList_t t -> cList_t t
 | CList_CNil : cList_t t
 
 (** [demo::list_nth]:
-    Source: 'src/demo.rs', lines 32:0-32:56 *)
+    Source: 'src/demo.rs', lines 39:0-39:56 *)
 let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
   if is_zero n
   then Fail OutOfFuel
@@ -48,7 +53,7 @@ let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
     end
 
 (** [demo::list_nth_mut]:
-    Source: 'src/demo.rs', lines 47:0-47:68 *)
+    Source: 'src/demo.rs', lines 54:0-54:68 *)
 let rec list_nth_mut
   (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
   result (t & (t -> result (cList_t t)))
@@ -74,7 +79,7 @@ let rec list_nth_mut
     end
 
 (** [demo::list_nth_mut1]: loop 0:
-    Source: 'src/demo.rs', lines 62:0-71:1 *)
+    Source: 'src/demo.rs', lines 69:0-78:1 *)
 let rec list_nth_mut1_loop
   (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
   result (t & (t -> result (cList_t t)))
@@ -99,7 +104,7 @@ let rec list_nth_mut1_loop
     end
 
 (** [demo::list_nth_mut1]:
-    Source: 'src/demo.rs', lines 62:0-62:77 *)
+    Source: 'src/demo.rs', lines 69:0-69:77 *)
 let list_nth_mut1
   (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
   result (t & (t -> result (cList_t t)))
@@ -107,7 +112,7 @@ let list_nth_mut1
   let* (x, back_'a) = list_nth_mut1_loop t n l i in Return (x, back_'a)
 
 (** [demo::i32_id]:
-    Source: 'src/demo.rs', lines 73:0-73:28 *)
+    Source: 'src/demo.rs', lines 80:0-80:28 *)
 let rec i32_id (n : nat) (i : i32) : result i32 =
   if is_zero n
   then Fail OutOfFuel
@@ -117,21 +122,41 @@ let rec i32_id (n : nat) (i : i32) : result i32 =
     then Return 0
     else let* i1 = i32_sub i 1 in let* i2 = i32_id n1 i1 in i32_add i2 1
 
+(** [demo::list_tail]:
+    Source: 'src/demo.rs', lines 88:0-88:64 *)
+let rec list_tail
+  (t : Type0) (n : nat) (l : cList_t t) :
+  result ((cList_t t) & (cList_t t -> result (cList_t t)))
+  =
+  if is_zero n
+  then Fail OutOfFuel
+  else
+    let n1 = decrease n in
+    begin match l with
+    | CList_CCons x tl ->
+      let* (c, list_tail_back) = list_tail t n1 tl in
+      let back_'a =
+        fun ret -> let* tl1 = list_tail_back ret in Return (CList_CCons x tl1)
+        in
+      Return (c, back_'a)
+    | CList_CNil -> Return (CList_CNil, Return)
+    end
+
 (** Trait declaration: [demo::Counter]
-    Source: 'src/demo.rs', lines 83:0-83:17 *)
+    Source: 'src/demo.rs', lines 97:0-97:17 *)
 noeq type counter_t (self : Type0) = { incr : self -> result (usize & self); }
 
 (** [demo::{(demo::Counter for usize)}::incr]:
-    Source: 'src/demo.rs', lines 88:4-88:31 *)
+    Source: 'src/demo.rs', lines 102:4-102:31 *)
 let counterUsize_incr (self : usize) : result (usize & usize) =
   let* self1 = usize_add self 1 in Return (self, self1)
 
 (** Trait implementation: [demo::{(demo::Counter for usize)}]
-    Source: 'src/demo.rs', lines 87:0-87:22 *)
+    Source: 'src/demo.rs', lines 101:0-101:22 *)
 let counterUsize : counter_t usize = { incr = counterUsize_incr; }
 
 (** [demo::use_counter]:
-    Source: 'src/demo.rs', lines 95:0-95:59 *)
+    Source: 'src/demo.rs', lines 109:0-109:59 *)
 let use_counter
   (t : Type0) (counterInst : counter_t t) (cnt : t) : result (usize & t) =
   counterInst.incr cnt
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 854b4853..f38b5cd3 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -36,14 +36,23 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 :=
 def incr (x : U32) : Result U32 :=
   x + 1#u32
 
+/- [demo::use_incr]:
+   Source: 'src/demo.rs', lines 25:0-25:17 -/
+def use_incr : Result Unit :=
+  do
+  let i ← incr 0#u32
+  let i1 ← incr i
+  let _ ← incr i1
+  Result.ret ()
+
 /- [demo::CList]
-   Source: 'src/demo.rs', lines 27:0-27:17 -/
+   Source: 'src/demo.rs', lines 34:0-34:17 -/
 inductive CList (T : Type) :=
 | CCons : T → CList T → CList T
 | CNil : CList T
 
 /- [demo::list_nth]:
-   Source: 'src/demo.rs', lines 32:0-32:56 -/
+   Source: 'src/demo.rs', lines 39:0-39:56 -/
 divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CList.CCons x tl =>
@@ -55,7 +64,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut]:
-   Source: 'src/demo.rs', lines 47:0-47:68 -/
+   Source: 'src/demo.rs', lines 54:0-54:68 -/
 divergent def list_nth_mut
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -79,7 +88,7 @@ divergent def list_nth_mut
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]: loop 0:
-   Source: 'src/demo.rs', lines 62:0-71:1 -/
+   Source: 'src/demo.rs', lines 69:0-78:1 -/
 divergent def list_nth_mut1_loop
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -102,7 +111,7 @@ divergent def list_nth_mut1_loop
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]:
-   Source: 'src/demo.rs', lines 62:0-62:77 -/
+   Source: 'src/demo.rs', lines 69:0-69:77 -/
 def list_nth_mut1
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -112,7 +121,7 @@ def list_nth_mut1
   Result.ret (t, back_'a)
 
 /- [demo::i32_id]:
-   Source: 'src/demo.rs', lines 73:0-73:28 -/
+   Source: 'src/demo.rs', lines 80:0-80:28 -/
 divergent def i32_id (i : I32) : Result I32 :=
   if i = 0#i32
   then Result.ret 0#i32
@@ -121,26 +130,44 @@ divergent def i32_id (i : I32) : Result I32 :=
        let i2 ← i32_id i1
        i2 + 1#i32
 
+/- [demo::list_tail]:
+   Source: 'src/demo.rs', lines 88:0-88:64 -/
+divergent def list_tail
+  (T : Type) (l : CList T) :
+  Result ((CList T) × (CList T → Result (CList T)))
+  :=
+  match l with
+  | CList.CCons t tl =>
+    do
+    let (c, list_tail_back) ← list_tail T tl
+    let back_'a :=
+      fun ret =>
+        do
+        let tl1 ← list_tail_back ret
+        Result.ret (CList.CCons t tl1)
+    Result.ret (c, back_'a)
+  | CList.CNil => Result.ret (CList.CNil, Result.ret)
+
 /- Trait declaration: [demo::Counter]
-   Source: 'src/demo.rs', lines 83:0-83:17 -/
+   Source: 'src/demo.rs', lines 97:0-97:17 -/
 structure Counter (Self : Type) where
   incr : Self → Result (Usize × Self)
 
 /- [demo::{(demo::Counter for usize)}::incr]:
-   Source: 'src/demo.rs', lines 88:4-88:31 -/
+   Source: 'src/demo.rs', lines 102:4-102:31 -/
 def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
   do
   let self1 ← self + 1#usize
   Result.ret (self, self1)
 
 /- Trait implementation: [demo::{(demo::Counter for usize)}]
-   Source: 'src/demo.rs', lines 87:0-87:22 -/
+   Source: 'src/demo.rs', lines 101:0-101:22 -/
 def CounterUsize : Counter Usize := {
   incr := CounterUsize.incr
 }
 
 /- [demo::use_counter]:
-   Source: 'src/demo.rs', lines 95:0-95:59 -/
+   Source: 'src/demo.rs', lines 109:0-109:59 -/
 def use_counter
   (T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
   CounterInst.incr cnt
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
index cdec7332..e514ac3e 100644
--- a/tests/lean/Demo/Properties.lean
+++ b/tests/lean/Demo/Properties.lean
@@ -65,4 +65,20 @@ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
 termination_by x.val.toNat
 decreasing_by scalar_decr_tac
 
+theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) :
+  ∃ back, list_tail T l = ret (CList.CNil, back) ∧
+  ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by
+  rw [list_tail]
+  match l with
+  | CNil =>
+    simp_all
+  | CCons hd tl =>
+    simp_all
+    progress as ⟨ back ⟩
+    simp
+    -- Proving the backward function
+    intro tl'
+    progress
+    simp_all
+
 end demo
-- 
cgit v1.2.3


From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Mar 2024 05:29:29 +0100
Subject: Regenerate the tests

---
 tests/coq/arrays/Arrays.v                          | 21 +++------
 tests/coq/betree/BetreeMain_Funs.v                 |  8 +---
 tests/coq/betree/_CoqProject                       |  2 +-
 tests/coq/demo/Demo.v                              |  2 +-
 tests/coq/hashmap/Hashmap_Funs.v                   |  4 +-
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v       |  8 +---
 tests/coq/hashmap_on_disk/_CoqProject              |  2 +-
 tests/coq/misc/Loops.v                             | 39 +++++-----------
 tests/coq/misc/_CoqProject                         |  4 +-
 tests/fstar/arrays/Arrays.Funs.fst                 | 17 +++----
 tests/fstar/betree/BetreeMain.Funs.fst             |  6 +--
 .../fstar/betree_back_stateful/BetreeMain.Funs.fst |  6 +--
 tests/fstar/demo/Demo.fst                          |  2 +-
 tests/fstar/hashmap/Hashmap.Funs.fst               |  3 +-
 tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst   |  6 +--
 tests/fstar/misc/Loops.Funs.fst                    | 35 +++++----------
 tests/lean/Arrays.lean                             | 28 ++++--------
 tests/lean/BetreeMain/Funs.lean                    |  8 +---
 tests/lean/Demo/Demo.lean                          |  4 +-
 tests/lean/Hashmap/Funs.lean                       |  4 +-
 tests/lean/HashmapMain/Funs.lean                   |  7 +--
 tests/lean/Loops.lean                              | 52 +++++++---------------
 22 files changed, 80 insertions(+), 188 deletions(-)

(limited to 'tests')

diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 34d163b7..580e72f0 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -30,9 +30,7 @@ Definition array_to_mut_slice_
   (T : Type) (s : array T 32%usize) :
   result ((slice T) * (slice T -> result (array T 32%usize)))
   :=
-  p <- array_to_slice_mut T 32%usize s;
-  let (s1, to_slice_mut_back) := p in
-  Return (s1, to_slice_mut_back)
+  array_to_slice_mut T 32%usize s
 .
 
 (** [arrays::array_len]:
@@ -78,9 +76,7 @@ Definition index_mut_array
   (T : Type) (s : array T 32%usize) (i : usize) :
   result (T * (T -> result (array T 32%usize)))
   :=
-  p <- array_index_mut_usize T 32%usize s i;
-  let (t, index_mut_back) := p in
-  Return (t, index_mut_back)
+  array_index_mut_usize T 32%usize s i
 .
 
 (** [arrays::index_slice]:
@@ -95,9 +91,7 @@ Definition index_mut_slice
   (T : Type) (s : slice T) (i : usize) :
   result (T * (T -> result (slice T)))
   :=
-  p <- slice_index_mut_usize T s i;
-  let (t, index_mut_back) := p in
-  Return (t, index_mut_back)
+  slice_index_mut_usize T s i
 .
 
 (** [arrays::slice_subslice_shared_]:
@@ -136,9 +130,7 @@ Definition array_to_slice_mut_
   (x : array u32 32%usize) :
   result ((slice u32) * (slice u32 -> result (array u32 32%usize)))
   :=
-  p <- array_to_slice_mut u32 32%usize x;
-  let (s, to_slice_mut_back) := p in
-  Return (s, to_slice_mut_back)
+  array_to_slice_mut u32 32%usize x
 .
 
 (** [arrays::array_subslice_shared_]:
@@ -381,7 +373,7 @@ Definition take_array_t (a : array AB_t 2%usize) : result unit :=
 (** [arrays::non_copyable_array]:
     Source: 'src/arrays.rs', lines 229:0-229:27 *)
 Definition non_copyable_array : result unit :=
-  _ <- take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]); Return tt
+  take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ])
 .
 
 (** [arrays::sum]: loop 0:
@@ -548,8 +540,7 @@ Fixpoint iter_mut_slice_loop
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s< len
-    then (
-      i1 <- usize_add i 1%usize; _ <- iter_mut_slice_loop n1 len i1; Return tt)
+    then (i1 <- usize_add i 1%usize; iter_mut_slice_loop n1 len i1)
     else Return tt
   end
 .
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 3863a90f..a0338557 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -27,9 +27,7 @@ Definition betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) :
   result (state * unit)
   :=
-  p <- betree_utils_store_internal_node id content st;
-  let (st1, _) := p in
-  Return (st1, tt)
+  betree_utils_store_internal_node id content st
 .
 
 (** [betree_main::betree::load_leaf_node]:
@@ -45,9 +43,7 @@ Definition betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 * u64)) (st : state) :
   result (state * unit)
   :=
-  p <- betree_utils_store_leaf_node id content st;
-  let (st1, _) := p in
-  Return (st1, tt)
+  betree_utils_store_leaf_node id content st
 .
 
 (** [betree_main::betree::fresh_node_id]:
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 13e4b9c1..b14bed66 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -3,8 +3,8 @@
 -arg -w
 -arg all
 
-BetreeMain_Types.v
 BetreeMain_TypesExternal_Template.v
+BetreeMain_Types.v
 Primitives.v
 BetreeMain_FunsExternal_Template.v
 BetreeMain_Funs.v
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 48067c02..2fccf6c0 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -127,7 +127,7 @@ Definition list_nth_mut1
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
   :=
-  p <- list_nth_mut1_loop T n l i; let (t, back_'a) := p in Return (t, back_'a)
+  list_nth_mut1_loop T n l i
 .
 
 (** [demo::i32_id]:
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 0478edbe..ab424e42 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -398,9 +398,7 @@ Definition hashMap_get_mut_in_list
   (T : Type) (n : nat) (ls : List_t T) (key : usize) :
   result (T * (T -> result (List_t T)))
   :=
-  p <- hashMap_get_mut_in_list_loop T n ls key;
-  let (t, back_'a) := p in
-  Return (t, back_'a)
+  hashMap_get_mut_in_list_loop T n ls key
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::get_mut]:
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 6a7eeb2d..aff4995f 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -423,9 +423,7 @@ Definition hashmap_HashMap_get_mut_in_list
   (T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) :
   result (T * (T -> result (hashmap_List_t T)))
   :=
-  p <- hashmap_HashMap_get_mut_in_list_loop T n ls key;
-  let (t, back_'a) := p in
-  Return (t, back_'a)
+  hashmap_HashMap_get_mut_in_list_loop T n ls key
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
@@ -585,9 +583,7 @@ Definition insert_on_disk
   p <- hashmap_utils_deserialize st;
   let (st1, hm) := p in
   hm1 <- hashmap_HashMap_insert u64 n hm key value;
-  p1 <- hashmap_utils_serialize hm1 st1;
-  let (st2, _) := p1 in
-  Return (st2, tt)
+  hashmap_utils_serialize hm1 st1
 .
 
 (** [hashmap_main::main]:
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject
index 41945494..d73541d9 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -4,9 +4,9 @@
 -arg all
 
 HashmapMain_Types.v
+HashmapMain_FunsExternal_Template.v
 Primitives.v
 HashmapMain_Funs.v
 HashmapMain_TypesExternal.v
-HashmapMain_FunsExternal_Template.v
 HashmapMain_FunsExternal.v
 HashmapMain_TypesExternal_Template.v
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index e235b60d..85b54510 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -183,7 +183,7 @@ Definition list_nth_mut_loop
   (T : Type) (n : nat) (ls : List_t T) (i : u32) :
   result (T * (T -> result (List_t T)))
   :=
-  p <- list_nth_mut_loop_loop T n ls i; let (t, back) := p in Return (t, back)
+  list_nth_mut_loop_loop T n ls i
 .
 
 (** [loops::list_nth_shared_loop]: loop 0:
@@ -400,9 +400,7 @@ Definition list_nth_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
   :=
-  t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i;
-  let '(p, back_'a, back_'b) := t in
-  Return (p, back_'a, back_'b)
+  list_nth_mut_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_loop_pair]: loop 0:
@@ -481,9 +479,7 @@ Definition list_nth_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
   :=
-  p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_loop_pair_merge]: loop 0:
@@ -557,9 +553,7 @@ Definition list_nth_mut_shared_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
@@ -599,9 +593,7 @@ Definition list_nth_mut_shared_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0:
@@ -641,9 +633,7 @@ Definition list_nth_shared_mut_loop_pair
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i;
-  let (p1, back_'b) := p in
-  Return (p1, back_'b)
+  list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i
 .
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
@@ -683,9 +673,7 @@ Definition list_nth_shared_mut_loop_pair_merge
   (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
   :=
-  p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i;
-  let (p1, back_'a) := p in
-  Return (p1, back_'a)
+  list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i
 .
 
 (** [loops::ignore_input_mut_borrow]: loop 0:
@@ -695,8 +683,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s> 0%u32
-    then (
-      i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt)
+    then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1)
     else Return tt
   end
 .
@@ -715,10 +702,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s> 0%u32
-    then (
-      i1 <- u32_sub i 1%u32;
-      _ <- incr_ignore_input_mut_borrow_loop n1 i1;
-      Return tt)
+    then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1)
     else Return tt
   end
 .
@@ -737,10 +721,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
   | O => Fail_ OutOfFuel
   | S n1 =>
     if i s> 0%u32
-    then (
-      i1 <- u32_sub i 1%u32;
-      _ <- ignore_input_shared_borrow_loop n1 i1;
-      Return tt)
+    then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1)
     else Return tt
   end
 .
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 869cdb4d..308de4f4 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,6 +3,7 @@
 -arg -w
 -arg all
 
+External_FunsExternal_Template.v
 Loops.v
 External_Types.v
 Primitives.v
@@ -10,9 +11,8 @@ External_Funs.v
 External_TypesExternal.v
 Constants.v
 PoloniusList.v
-Paper.v
 NoNestedBorrows.v
 External_FunsExternal.v
 Bitwise.v
 External_TypesExternal_Template.v
-External_FunsExternal_Template.v
+Paper.v
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index cf0f4f8b..15c82e93 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -23,8 +23,7 @@ let array_to_mut_slice_
   (t : Type0) (s : array t 32) :
   result ((slice t) & (slice t -> result (array t 32)))
   =
-  let* (s1, to_slice_mut_back) = array_to_slice_mut t 32 s in
-  Return (s1, to_slice_mut_back)
+  array_to_slice_mut t 32 s
 
 (** [arrays::array_len]:
     Source: 'src/arrays.rs', lines 25:0-25:40 *)
@@ -62,8 +61,7 @@ let index_mut_array
   (t : Type0) (s : array t 32) (i : usize) :
   result (t & (t -> result (array t 32)))
   =
-  let* (x, index_mut_back) = array_index_mut_usize t 32 s i in
-  Return (x, index_mut_back)
+  array_index_mut_usize t 32 s i
 
 (** [arrays::index_slice]:
     Source: 'src/arrays.rs', lines 56:0-56:46 *)
@@ -76,8 +74,7 @@ let index_mut_slice
   (t : Type0) (s : slice t) (i : usize) :
   result (t & (t -> result (slice t)))
   =
-  let* (x, index_mut_back) = slice_index_mut_usize t s i in
-  Return (x, index_mut_back)
+  slice_index_mut_usize t s i
 
 (** [arrays::slice_subslice_shared_]:
     Source: 'src/arrays.rs', lines 64:0-64:70 *)
@@ -110,8 +107,7 @@ let array_to_slice_mut_
   (x : array u32 32) :
   result ((slice u32) & (slice u32 -> result (array u32 32)))
   =
-  let* (s, to_slice_mut_back) = array_to_slice_mut u32 32 x in
-  Return (s, to_slice_mut_back)
+  array_to_slice_mut u32 32 x
 
 (** [arrays::array_subslice_shared_]:
     Source: 'src/arrays.rs', lines 80:0-80:74 *)
@@ -308,7 +304,7 @@ let take_array_t (a : array aB_t 2) : result unit =
 (** [arrays::non_copyable_array]:
     Source: 'src/arrays.rs', lines 229:0-229:27 *)
 let non_copyable_array : result unit =
-  let* _ = take_array_t (mk_array aB_t 2 [ AB_A; AB_B ]) in Return ()
+  take_array_t (mk_array aB_t 2 [ AB_A; AB_B ])
 
 (** [arrays::sum]: loop 0:
     Source: 'src/arrays.rs', lines 242:0-250:1 *)
@@ -444,8 +440,7 @@ let rec iter_mut_slice_loop
   Tot (result unit) (decreases (iter_mut_slice_loop_decreases len i))
   =
   if i < len
-  then
-    let* i1 = usize_add i 1 in let* _ = iter_mut_slice_loop len i1 in Return ()
+  then let* i1 = usize_add i 1 in iter_mut_slice_loop len i1
   else Return ()
 
 (** [arrays::iter_mut_slice]:
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index ec042fb3..74044961 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -22,8 +22,7 @@ let betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) :
   result (state & unit)
   =
-  let* (st1, _) = betree_utils_store_internal_node id content st in
-  Return (st1, ())
+  betree_utils_store_internal_node id content st
 
 (** [betree_main::betree::load_leaf_node]:
     Source: 'src/betree.rs', lines 46:0-46:44 *)
@@ -37,8 +36,7 @@ let betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 & u64)) (st : state) :
   result (state & unit)
   =
-  let* (st1, _) = betree_utils_store_leaf_node id content st in
-  Return (st1, ())
+  betree_utils_store_leaf_node id content st
 
 (** [betree_main::betree::fresh_node_id]:
     Source: 'src/betree.rs', lines 55:0-55:48 *)
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index ec042fb3..74044961 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -22,8 +22,7 @@ let betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) :
   result (state & unit)
   =
-  let* (st1, _) = betree_utils_store_internal_node id content st in
-  Return (st1, ())
+  betree_utils_store_internal_node id content st
 
 (** [betree_main::betree::load_leaf_node]:
     Source: 'src/betree.rs', lines 46:0-46:44 *)
@@ -37,8 +36,7 @@ let betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 & u64)) (st : state) :
   result (state & unit)
   =
-  let* (st1, _) = betree_utils_store_leaf_node id content st in
-  Return (st1, ())
+  betree_utils_store_leaf_node id content st
 
 (** [betree_main::betree::fresh_node_id]:
     Source: 'src/betree.rs', lines 55:0-55:48 *)
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index 5651b80f..4ad7cb65 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -109,7 +109,7 @@ let list_nth_mut1
   (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
   result (t & (t -> result (cList_t t)))
   =
-  let* (x, back_'a) = list_nth_mut1_loop t n l i in Return (x, back_'a)
+  list_nth_mut1_loop t n l i
 
 (** [demo::i32_id]:
     Source: 'src/demo.rs', lines 80:0-80:28 *)
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 447f9b49..7ca8b9c1 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -308,8 +308,7 @@ let hashMap_get_mut_in_list
   (t : Type0) (ls : list_t t) (key : usize) :
   result (t & (t -> result (list_t t)))
   =
-  let* (x, back_'a) = hashMap_get_mut_in_list_loop t ls key in
-  Return (x, back_'a)
+  hashMap_get_mut_in_list_loop t ls key
 
 (** [hashmap::{hashmap::HashMap<T>}::get_mut]:
     Source: 'src/hashmap.rs', lines 257:4-257:67 *)
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index b16dcada..9b5baaeb 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -324,8 +324,7 @@ let hashmap_HashMap_get_mut_in_list
   (t : Type0) (ls : hashmap_List_t t) (key : usize) :
   result (t & (t -> result (hashmap_List_t t)))
   =
-  let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t ls key in
-  Return (x, back_'a)
+  hashmap_HashMap_get_mut_in_list_loop t ls key
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
     Source: 'src/hashmap.rs', lines 257:4-257:67 *)
@@ -446,8 +445,7 @@ let insert_on_disk
   (key : usize) (value : u64) (st : state) : result (state & unit) =
   let* (st1, hm) = hashmap_utils_deserialize st in
   let* hm1 = hashmap_HashMap_insert u64 hm key value in
-  let* (st2, _) = hashmap_utils_serialize hm1 st1 in
-  Return (st2, ())
+  hashmap_utils_serialize hm1 st1
 
 (** [hashmap_main::main]:
     Source: 'src/hashmap_main.rs', lines 16:0-16:13 *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 5f24fe7a..c87f693b 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -140,7 +140,7 @@ let list_nth_mut_loop
   (t : Type0) (ls : list_t t) (i : u32) :
   result (t & (t -> result (list_t t)))
   =
-  let* (x, back) = list_nth_mut_loop_loop t ls i in Return (x, back)
+  list_nth_mut_loop_loop t ls i
 
 (** [loops::list_nth_shared_loop]: loop 0:
     Source: 'src/loops.rs', lines 101:0-111:1 *)
@@ -312,8 +312,7 @@ let list_nth_mut_loop_pair
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t)))
   =
-  let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t ls0 ls1 i in
-  Return (p, back_'a, back_'b)
+  list_nth_mut_loop_pair_loop t ls0 ls1 i
 
 (** [loops::list_nth_shared_loop_pair]: loop 0:
     Source: 'src/loops.rs', lines 208:0-229:1 *)
@@ -376,8 +375,7 @@ let list_nth_mut_loop_pair_merge
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t))))
   =
-  let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t ls0 ls1 i in
-  Return (p, back_'a)
+  list_nth_mut_loop_pair_merge_loop t ls0 ls1 i
 
 (** [loops::list_nth_shared_loop_pair_merge]: loop 0:
     Source: 'src/loops.rs', lines 251:0-266:1 *)
@@ -438,8 +436,7 @@ let list_nth_mut_shared_loop_pair
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   result ((t & t) & (t -> result (list_t t)))
   =
-  let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t ls0 ls1 i in
-  Return (p, back_'a)
+  list_nth_mut_shared_loop_pair_loop t ls0 ls1 i
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
     Source: 'src/loops.rs', lines 288:0-303:1 *)
@@ -474,8 +471,7 @@ let list_nth_mut_shared_loop_pair_merge
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   result ((t & t) & (t -> result (list_t t)))
   =
-  let* (p, back_'a) = list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i in
-  Return (p, back_'a)
+  list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0:
     Source: 'src/loops.rs', lines 307:0-322:1 *)
@@ -509,8 +505,7 @@ let list_nth_shared_mut_loop_pair
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   result ((t & t) & (t -> result (list_t t)))
   =
-  let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t ls0 ls1 i in
-  Return (p, back_'b)
+  list_nth_shared_mut_loop_pair_loop t ls0 ls1 i
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
     Source: 'src/loops.rs', lines 326:0-341:1 *)
@@ -545,8 +540,7 @@ let list_nth_shared_mut_loop_pair_merge
   (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   result ((t & t) & (t -> result (list_t t)))
   =
-  let* (p, back_'a) = list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i in
-  Return (p, back_'a)
+  list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i
 
 (** [loops::ignore_input_mut_borrow]: loop 0:
     Source: 'src/loops.rs', lines 345:0-349:1 *)
@@ -555,10 +549,7 @@ let rec ignore_input_mut_borrow_loop
   Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i))
   =
   if i > 0
-  then
-    let* i1 = u32_sub i 1 in
-    let* _ = ignore_input_mut_borrow_loop i1 in
-    Return ()
+  then let* i1 = u32_sub i 1 in ignore_input_mut_borrow_loop i1
   else Return ()
 
 (** [loops::ignore_input_mut_borrow]:
@@ -573,10 +564,7 @@ let rec incr_ignore_input_mut_borrow_loop
   Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i))
   =
   if i > 0
-  then
-    let* i1 = u32_sub i 1 in
-    let* _ = incr_ignore_input_mut_borrow_loop i1 in
-    Return ()
+  then let* i1 = u32_sub i 1 in incr_ignore_input_mut_borrow_loop i1
   else Return ()
 
 (** [loops::incr_ignore_input_mut_borrow]:
@@ -593,10 +581,7 @@ let rec ignore_input_shared_borrow_loop
   Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i))
   =
   if i > 0
-  then
-    let* i1 = u32_sub i 1 in
-    let* _ = ignore_input_shared_borrow_loop i1 in
-    Return ()
+  then let* i1 = u32_sub i 1 in ignore_input_shared_borrow_loop i1
   else Return ()
 
 (** [loops::ignore_input_shared_borrow]:
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index d637ee13..cd1b6544 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -28,9 +28,7 @@ def array_to_mut_slice_
   (T : Type) (s : Array T 32#usize) :
   Result ((Slice T) × (Slice T → Result (Array T 32#usize)))
   :=
-  do
-  let (s1, to_slice_mut_back) ← Array.to_slice_mut T 32#usize s
-  Result.ret (s1, to_slice_mut_back)
+  Array.to_slice_mut T 32#usize s
 
 /- [arrays::array_len]:
    Source: 'src/arrays.rs', lines 25:0-25:40 -/
@@ -76,9 +74,7 @@ def index_mut_array
   (T : Type) (s : Array T 32#usize) (i : Usize) :
   Result (T × (T → Result (Array T 32#usize)))
   :=
-  do
-  let (t, index_mut_back) ← Array.index_mut_usize T 32#usize s i
-  Result.ret (t, index_mut_back)
+  Array.index_mut_usize T 32#usize s i
 
 /- [arrays::index_slice]:
    Source: 'src/arrays.rs', lines 56:0-56:46 -/
@@ -91,9 +87,7 @@ def index_mut_slice
   (T : Type) (s : Slice T) (i : Usize) :
   Result (T × (T → Result (Slice T)))
   :=
-  do
-  let (t, index_mut_back) ← Slice.index_mut_usize T s i
-  Result.ret (t, index_mut_back)
+  Slice.index_mut_usize T s i
 
 /- [arrays::slice_subslice_shared_]:
    Source: 'src/arrays.rs', lines 64:0-64:70 -/
@@ -127,9 +121,7 @@ def array_to_slice_mut_
   (x : Array U32 32#usize) :
   Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
   :=
-  do
-  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 32#usize x
-  Result.ret (s, to_slice_mut_back)
+  Array.to_slice_mut U32 32#usize x
 
 /- [arrays::array_subslice_shared_]:
    Source: 'src/arrays.rs', lines 80:0-80:74 -/
@@ -354,9 +346,7 @@ def take_array_t (a : Array AB 2#usize) : Result Unit :=
 /- [arrays::non_copyable_array]:
    Source: 'src/arrays.rs', lines 229:0-229:27 -/
 def non_copyable_array : Result Unit :=
-  do
-  let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
-  Result.ret ()
+  take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
 
 /- [arrays::sum]: loop 0:
    Source: 'src/arrays.rs', lines 242:0-250:1 -/
@@ -496,11 +486,9 @@ def zero_slice (a : Slice U8) : Result (Slice U8) :=
    Source: 'src/arrays.rs', lines 312:0-318:1 -/
 divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
   if i < len
-  then
-    do
-    let i1 ← i + 1#usize
-    let _ ← iter_mut_slice_loop len i1
-    Result.ret ()
+  then do
+       let i1 ← i + 1#usize
+       iter_mut_slice_loop len i1
   else Result.ret ()
 
 /- [arrays::iter_mut_slice]:
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index d6449b37..bd5921a8 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -21,9 +21,7 @@ def betree.store_internal_node
   (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) :
   Result (State × Unit)
   :=
-  do
-  let (st1, _) ← betree_utils.store_internal_node id content st
-  Result.ret (st1, ())
+  betree_utils.store_internal_node id content st
 
 /- [betree_main::betree::load_leaf_node]:
    Source: 'src/betree.rs', lines 46:0-46:44 -/
@@ -37,9 +35,7 @@ def betree.store_leaf_node
   (id : U64) (content : betree.List (U64 × U64)) (st : State) :
   Result (State × Unit)
   :=
-  do
-  let (st1, _) ← betree_utils.store_leaf_node id content st
-  Result.ret (st1, ())
+  betree_utils.store_leaf_node id content st
 
 /- [betree_main::betree::fresh_node_id]:
    Source: 'src/betree.rs', lines 55:0-55:48 -/
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index f38b5cd3..09032820 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -116,9 +116,7 @@ def list_nth_mut1
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
   :=
-  do
-  let (t, back_'a) ← list_nth_mut1_loop T l i
-  Result.ret (t, back_'a)
+  list_nth_mut1_loop T l i
 
 /- [demo::i32_id]:
    Source: 'src/demo.rs', lines 80:0-80:28 -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index f0706725..d33b6571 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -311,9 +311,7 @@ def HashMap.get_mut_in_list
   (T : Type) (ls : List T) (key : Usize) :
   Result (T × (T → Result (List T)))
   :=
-  do
-  let (t, back_'a) ← HashMap.get_mut_in_list_loop T ls key
-  Result.ret (t, back_'a)
+  HashMap.get_mut_in_list_loop T ls key
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut]:
    Source: 'src/hashmap.rs', lines 257:4-257:67 -/
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 31441b4a..8a277700 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -326,9 +326,7 @@ def hashmap.HashMap.get_mut_in_list
   (T : Type) (ls : hashmap.List T) (key : Usize) :
   Result (T × (T → Result (hashmap.List T)))
   :=
-  do
-  let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T ls key
-  Result.ret (t, back_'a)
+  hashmap.HashMap.get_mut_in_list_loop T ls key
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
    Source: 'src/hashmap.rs', lines 257:4-257:67 -/
@@ -460,8 +458,7 @@ def insert_on_disk
   do
   let (st1, hm) ← hashmap_utils.deserialize st
   let hm1 ← hashmap.HashMap.insert U64 hm key value
-  let (st2, _) ← hashmap_utils.serialize hm1 st1
-  Result.ret (st2, ())
+  hashmap_utils.serialize hm1 st1
 
 /- [hashmap_main::main]:
    Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 433ca8f0..3f075347 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -138,9 +138,7 @@ divergent def list_nth_mut_loop_loop
    Source: 'src/loops.rs', lines 88:0-88:71 -/
 def list_nth_mut_loop
   (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
-  do
-  let (t, back) ← list_nth_mut_loop_loop T ls i
-  Result.ret (t, back)
+  list_nth_mut_loop_loop T ls i
 
 /- [loops::list_nth_shared_loop]: loop 0:
    Source: 'src/loops.rs', lines 101:0-111:1 -/
@@ -322,9 +320,7 @@ def list_nth_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T ls0 ls1 i
-  Result.ret (p, back_'a, back_'b)
+  list_nth_mut_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair]: loop 0:
    Source: 'src/loops.rs', lines 208:0-229:1 -/
@@ -384,9 +380,7 @@ def list_nth_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
   :=
-  do
-  let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 251:0-266:1 -/
@@ -443,9 +437,7 @@ def list_nth_mut_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 288:0-303:1 -/
@@ -480,9 +472,7 @@ def list_nth_mut_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a) ← list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair]: loop 0:
    Source: 'src/loops.rs', lines 307:0-322:1 -/
@@ -516,9 +506,7 @@ def list_nth_shared_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
-  Result.ret (p, back_'b)
+  list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 326:0-341:1 -/
@@ -553,19 +541,15 @@ def list_nth_shared_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a) ← list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::ignore_input_mut_borrow]: loop 0:
    Source: 'src/loops.rs', lines 345:0-349:1 -/
 divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
-  then
-    do
-    let i1 ← i - 1#u32
-    let _ ← ignore_input_mut_borrow_loop i1
-    Result.ret ()
+  then do
+       let i1 ← i - 1#u32
+       ignore_input_mut_borrow_loop i1
   else Result.ret ()
 
 /- [loops::ignore_input_mut_borrow]:
@@ -579,11 +563,9 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
    Source: 'src/loops.rs', lines 353:0-358:1 -/
 divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
-  then
-    do
-    let i1 ← i - 1#u32
-    let _ ← incr_ignore_input_mut_borrow_loop i1
-    Result.ret ()
+  then do
+       let i1 ← i - 1#u32
+       incr_ignore_input_mut_borrow_loop i1
   else Result.ret ()
 
 /- [loops::incr_ignore_input_mut_borrow]:
@@ -598,11 +580,9 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
    Source: 'src/loops.rs', lines 362:0-366:1 -/
 divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
-  then
-    do
-    let i1 ← i - 1#u32
-    let _ ← ignore_input_shared_borrow_loop i1
-    Result.ret ()
+  then do
+       let i1 ← i - 1#u32
+       ignore_input_shared_borrow_loop i1
   else Result.ret ()
 
 /- [loops::ignore_input_shared_borrow]:
-- 
cgit v1.2.3


From 5e99d127e0a746f5779779756fccf79f15c19d10 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 20 Mar 2024 06:17:41 +0100
Subject: Regenerate the code

---
 tests/coq/arrays/Arrays.v                          |  10 +-
 tests/coq/betree/BetreeMain_Funs.v                 | 140 ++++++++++----------
 tests/coq/demo/Demo.v                              |   2 +-
 tests/coq/hashmap/Hashmap_Funs.v                   |  26 ++--
 tests/coq/hashmap_on_disk/HashmapMain_Funs.v       |  28 ++--
 tests/coq/misc/External_Funs.v                     |   6 +-
 tests/coq/misc/Loops.v                             |  22 ++--
 tests/coq/misc/NoNestedBorrows.v                   |   9 +-
 tests/coq/misc/Paper.v                             |   2 +-
 tests/fstar/arrays/Arrays.Funs.fst                 |  10 +-
 tests/fstar/betree/BetreeMain.Funs.fst             | 141 +++++++++++----------
 .../fstar/betree_back_stateful/BetreeMain.Funs.fst | 141 +++++++++++----------
 tests/fstar/demo/Demo.fst                          |   2 +-
 tests/fstar/hashmap/Hashmap.Funs.fst               |  24 ++--
 tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst   |  27 ++--
 tests/fstar/misc/External.Funs.fst                 |   4 +-
 tests/fstar/misc/Loops.Clauses.Template.fst        |   3 +-
 tests/fstar/misc/Loops.Funs.fst                    |  24 ++--
 tests/fstar/misc/NoNestedBorrows.fst               |   7 +-
 tests/fstar/misc/Paper.fst                         |   2 +-
 tests/lean/Arrays.lean                             |  13 +-
 tests/lean/BetreeMain/Funs.lean                    | 136 ++++++++++----------
 tests/lean/Demo/Demo.lean                          |   6 +-
 tests/lean/External/Funs.lean                      |   6 +-
 tests/lean/Hashmap/Funs.lean                       |  29 ++---
 tests/lean/HashmapMain/Funs.lean                   |  29 ++---
 tests/lean/Loops.lean                              |  24 ++--
 tests/lean/NoNestedBorrows.lean                    |   8 +-
 tests/lean/Paper.lean                              |   4 +-
 29 files changed, 431 insertions(+), 454 deletions(-)

(limited to 'tests')

diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 580e72f0..049d63cb 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -36,19 +36,19 @@ Definition array_to_mut_slice_
 (** [arrays::array_len]:
     Source: 'src/arrays.rs', lines 25:0-25:40 *)
 Definition array_len (T : Type) (s : array T 32%usize) : result usize :=
-  s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i
+  s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
 .
 
 (** [arrays::shared_array_len]:
     Source: 'src/arrays.rs', lines 29:0-29:48 *)
 Definition shared_array_len (T : Type) (s : array T 32%usize) : result usize :=
-  s1 <- array_to_slice T 32%usize s; let i := slice_len T s1 in Return i
+  s1 <- array_to_slice T 32%usize s; Return (slice_len T s1)
 .
 
 (** [arrays::shared_slice_len]:
     Source: 'src/arrays.rs', lines 33:0-33:44 *)
 Definition shared_slice_len (T : Type) (s : slice T) : result usize :=
-  let i := slice_len T s in Return i
+  Return (slice_len T s)
 .
 
 (** [arrays::index_array_shared]:
@@ -326,8 +326,8 @@ Definition update_mut_slice (x : slice u32) : result (slice u32) :=
 Definition update_all : result unit :=
   _ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
   _ <- update_array (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
-  a <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
-  p <- array_to_slice_mut u32 2%usize a;
+  x <- update_array_mut_borrow (mk_array u32 2%usize [ 0%u32; 0%u32 ]);
+  p <- array_to_slice_mut u32 2%usize x;
   let (s, to_slice_mut_back) := p in
   s1 <- update_mut_slice s;
   _ <- to_slice_mut_back s1;
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index a0338557..c2cca26d 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -201,9 +201,9 @@ Definition betree_Leaf_split
   p1 <- betree_List_hd (u64 * u64) content1;
   let (pivot, _) := p1 in
   p2 <- betree_NodeIdCounter_fresh_id node_id_cnt;
-  let (id0, nic) := p2 in
-  p3 <- betree_NodeIdCounter_fresh_id nic;
-  let (id1, nic1) := p3 in
+  let (id0, node_id_cnt1) := p2 in
+  p3 <- betree_NodeIdCounter_fresh_id node_id_cnt1;
+  let (id1, node_id_cnt2) := p3 in
   p4 <- betree_store_leaf_node id0 content0 st;
   let (st1, _) := p4 in
   p5 <- betree_store_leaf_node id1 content1 st1;
@@ -218,7 +218,8 @@ Definition betree_Leaf_split
       betree_Leaf_id := id1;
       betree_Leaf_size := params.(betree_Params_split_size)
     |} in
-  Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, nic1))
+  Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2,
+    node_id_cnt2))
 .
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
@@ -286,22 +287,22 @@ Fixpoint betree_Node_apply_upserts
     if b
     then (
       p <- betree_List_pop_front (u64 * betree_Message_t) msgs;
-      let (msg, l) := p in
+      let (msg, msgs1) := p in
       let (_, m) := msg in
       match m with
       | Betree_Message_Insert _ => Fail_ Failure
       | Betree_Message_Delete => Fail_ Failure
       | Betree_Message_Upsert s =>
         v <- betree_upsert_update prev s;
-        betree_Node_apply_upserts n1 l (Some v) key st
+        betree_Node_apply_upserts n1 msgs1 (Some v) key st
       end)
     else (
       p <- core_option_Option_unwrap u64 prev st;
       let (st1, v) := p in
-      l <-
+      msgs1 <-
         betree_List_push_front (u64 * betree_Message_t) msgs (key,
           Betree_Message_Insert v);
-      Return (st1, (v, l)))
+      Return (st1, (v, msgs1)))
   end
 .
 
@@ -351,9 +352,9 @@ with betree_Node_lookup
         then (
           p3 <- betree_Internal_lookup_in_children n1 node key st1;
           let (st2, p4) := p3 in
-          let (o, i) := p4 in
+          let (o, node1) := p4 in
           _ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l);
-          Return (st2, (o, Betree_Node_Internal i)))
+          Return (st2, (o, Betree_Node_Internal node1)))
         else
           match msg with
           | Betree_Message_Insert v =>
@@ -369,23 +370,24 @@ with betree_Node_lookup
           | Betree_Message_Upsert ufs =>
             p3 <- betree_Internal_lookup_in_children n1 node key st1;
             let (st2, p4) := p3 in
-            let (v, i) := p4 in
+            let (v, node1) := p4 in
             p5 <-
               betree_Node_apply_upserts n1 (Betree_List_Cons (k,
                 Betree_Message_Upsert ufs) l) v key st2;
             let (st3, p6) := p5 in
-            let (v1, l1) := p6 in
-            msgs1 <- lookup_first_message_for_key_back l1;
-            p7 <- betree_store_internal_node i.(betree_Internal_id) msgs1 st3;
+            let (v1, pending1) := p6 in
+            msgs1 <- lookup_first_message_for_key_back pending1;
+            p7 <-
+              betree_store_internal_node node1.(betree_Internal_id) msgs1 st3;
             let (st4, _) := p7 in
-            Return (st4, (Some v1, Betree_Node_Internal i))
+            Return (st4, (Some v1, Betree_Node_Internal node1))
           end
       | Betree_List_Nil =>
         p2 <- betree_Internal_lookup_in_children n1 node key st1;
         let (st2, p3) := p2 in
-        let (o, i) := p3 in
+        let (o, node1) := p3 in
         _ <- lookup_first_message_for_key_back Betree_List_Nil;
-        Return (st2, (o, Betree_Node_Internal i))
+        Return (st2, (o, Betree_Node_Internal node1))
       end
     | Betree_Node_Leaf node =>
       p <- betree_load_leaf_node node.(betree_Leaf_id) st;
@@ -413,8 +415,8 @@ Fixpoint betree_Node_filter_messages_for_key
         p1 <-
           betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k,
             m) l);
-        let (_, l1) := p1 in
-        betree_Node_filter_messages_for_key n1 key l1)
+        let (_, msgs1) := p1 in
+        betree_Node_filter_messages_for_key n1 key msgs1)
       else Return (Betree_List_Cons (k, m) l)
     | Betree_List_Nil => Return Betree_List_Nil
     end
@@ -463,17 +465,17 @@ Definition betree_Node_apply_to_internal
   then
     match new_msg with
     | Betree_Message_Insert i =>
-      l <- betree_Node_filter_messages_for_key n key msgs1;
-      l1 <-
-        betree_List_push_front (u64 * betree_Message_t) l (key,
+      msgs2 <- betree_Node_filter_messages_for_key n key msgs1;
+      msgs3 <-
+        betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
           Betree_Message_Insert i);
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | Betree_Message_Delete =>
-      l <- betree_Node_filter_messages_for_key n key msgs1;
-      l1 <-
-        betree_List_push_front (u64 * betree_Message_t) l (key,
+      msgs2 <- betree_Node_filter_messages_for_key n key msgs1;
+      msgs3 <-
+        betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
           Betree_Message_Delete);
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | Betree_Message_Upsert s =>
       p1 <- betree_List_hd (u64 * betree_Message_t) msgs1;
       let (_, m) := p1 in
@@ -481,32 +483,33 @@ Definition betree_Node_apply_to_internal
       | Betree_Message_Insert prev =>
         v <- betree_upsert_update (Some prev) s;
         p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1;
-        let (_, l) := p2 in
-        l1 <-
-          betree_List_push_front (u64 * betree_Message_t) l (key,
+        let (_, msgs2) := p2 in
+        msgs3 <-
+          betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
             Betree_Message_Insert v);
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | Betree_Message_Delete =>
         p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1;
-        let (_, l) := p2 in
+        let (_, msgs2) := p2 in
         v <- betree_upsert_update None s;
-        l1 <-
-          betree_List_push_front (u64 * betree_Message_t) l (key,
+        msgs3 <-
+          betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
             Betree_Message_Insert v);
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | Betree_Message_Upsert _ =>
         p2 <- betree_Node_lookup_first_message_after_key n key msgs1;
         let (msgs2, lookup_first_message_after_key_back) := p2 in
-        l <-
+        msgs3 <-
           betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
             Betree_Message_Upsert s);
-        msgs3 <- lookup_first_message_after_key_back l;
-        lookup_first_message_for_key_back msgs3
+        msgs4 <- lookup_first_message_after_key_back msgs3;
+        lookup_first_message_for_key_back msgs4
       end
     end
   else (
-    l <- betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg);
-    lookup_first_message_for_key_back l)
+    msgs2 <-
+      betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg);
+    lookup_first_message_for_key_back msgs2)
 .
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
@@ -522,8 +525,8 @@ Fixpoint betree_Node_apply_messages_to_internal
     match new_msgs with
     | Betree_List_Cons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
-      l <- betree_Node_apply_to_internal n1 msgs i m;
-      betree_Node_apply_messages_to_internal n1 l new_msgs_tl
+      msgs1 <- betree_Node_apply_to_internal n1 msgs i m;
+      betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl
     | Betree_List_Nil => Return msgs
     end
   end
@@ -570,28 +573,28 @@ Definition betree_Node_apply_to_leaf
   if b
   then (
     p1 <- betree_List_pop_front (u64 * u64) bindings1;
-    let (hd, l) := p1 in
+    let (hd, bindings2) := p1 in
     match new_msg with
     | Betree_Message_Insert v =>
-      l1 <- betree_List_push_front (u64 * u64) l (key, v);
-      lookup_mut_in_bindings_back l1
-    | Betree_Message_Delete => lookup_mut_in_bindings_back l
+      bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v);
+      lookup_mut_in_bindings_back bindings3
+    | Betree_Message_Delete => lookup_mut_in_bindings_back bindings2
     | Betree_Message_Upsert s =>
       let (_, i) := hd in
       v <- betree_upsert_update (Some i) s;
-      l1 <- betree_List_push_front (u64 * u64) l (key, v);
-      lookup_mut_in_bindings_back l1
+      bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v);
+      lookup_mut_in_bindings_back bindings3
     end)
   else
     match new_msg with
     | Betree_Message_Insert v =>
-      l <- betree_List_push_front (u64 * u64) bindings1 (key, v);
-      lookup_mut_in_bindings_back l
+      bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v);
+      lookup_mut_in_bindings_back bindings2
     | Betree_Message_Delete => lookup_mut_in_bindings_back bindings1
     | Betree_Message_Upsert s =>
       v <- betree_upsert_update None s;
-      l <- betree_List_push_front (u64 * u64) bindings1 (key, v);
-      lookup_mut_in_bindings_back l
+      bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v);
+      lookup_mut_in_bindings_back bindings2
     end
 .
 
@@ -608,8 +611,8 @@ Fixpoint betree_Node_apply_messages_to_leaf
     match new_msgs with
     | Betree_List_Cons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
-      l <- betree_Node_apply_to_leaf n1 bindings i m;
-      betree_Node_apply_messages_to_leaf n1 l new_msgs_tl
+      bindings1 <- betree_Node_apply_to_leaf n1 bindings i m;
+      betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl
     | Betree_List_Nil => Return bindings
     end
   end
@@ -680,38 +683,39 @@ with betree_Node_apply_messages
     | Betree_Node_Internal node =>
       p <- betree_load_internal_node node.(betree_Internal_id) st;
       let (st1, content) := p in
-      l <- betree_Node_apply_messages_to_internal n1 content msgs;
-      num_msgs <- betree_List_len (u64 * betree_Message_t) n1 l;
+      content1 <- betree_Node_apply_messages_to_internal n1 content msgs;
+      num_msgs <- betree_List_len (u64 * betree_Message_t) n1 content1;
       if num_msgs s>= params.(betree_Params_min_flush_size)
       then (
-        p1 <- betree_Internal_flush n1 node params node_id_cnt l st1;
+        p1 <- betree_Internal_flush n1 node params node_id_cnt content1 st1;
         let (st2, p2) := p1 in
-        let (content1, p3) := p2 in
+        let (content2, p3) := p2 in
         let (node1, node_id_cnt1) := p3 in
         p4 <-
-          betree_store_internal_node node1.(betree_Internal_id) content1 st2;
+          betree_store_internal_node node1.(betree_Internal_id) content2 st2;
         let (st3, _) := p4 in
         Return (st3, (Betree_Node_Internal node1, node_id_cnt1)))
       else (
-        p1 <- betree_store_internal_node node.(betree_Internal_id) l st1;
+        p1 <-
+          betree_store_internal_node node.(betree_Internal_id) content1 st1;
         let (st2, _) := p1 in
         Return (st2, (Betree_Node_Internal node, node_id_cnt)))
     | Betree_Node_Leaf node =>
       p <- betree_load_leaf_node node.(betree_Leaf_id) st;
       let (st1, content) := p in
-      l <- betree_Node_apply_messages_to_leaf n1 content msgs;
-      len <- betree_List_len (u64 * u64) n1 l;
+      content1 <- betree_Node_apply_messages_to_leaf n1 content msgs;
+      len <- betree_List_len (u64 * u64) n1 content1;
       i <- u64_mul 2%u64 params.(betree_Params_split_size);
       if len s>= i
       then (
-        p1 <- betree_Leaf_split n1 node l params node_id_cnt st1;
+        p1 <- betree_Leaf_split n1 node content1 params node_id_cnt st1;
         let (st2, p2) := p1 in
-        let (new_node, nic) := p2 in
+        let (new_node, node_id_cnt1) := p2 in
         p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2;
         let (st3, _) := p3 in
-        Return (st3, (Betree_Node_Internal new_node, nic)))
+        Return (st3, (Betree_Node_Internal new_node, node_id_cnt1)))
       else (
-        p1 <- betree_store_leaf_node node.(betree_Leaf_id) l st1;
+        p1 <- betree_store_leaf_node node.(betree_Leaf_id) content1 st1;
         let (st2, _) := p1 in
         Return (st2, (Betree_Node_Leaf
           {| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len
@@ -744,7 +748,7 @@ Definition betree_BeTree_new
   :=
   node_id_cnt <- betree_NodeIdCounter_new;
   p <- betree_NodeIdCounter_fresh_id node_id_cnt;
-  let (id, nic) := p in
+  let (id, node_id_cnt1) := p in
   p1 <- betree_store_leaf_node id Betree_List_Nil st;
   let (st1, _) := p1 in
   Return (st1,
@@ -754,7 +758,7 @@ Definition betree_BeTree_new
           betree_Params_min_flush_size := min_flush_size;
           betree_Params_split_size := split_size
         |};
-      betree_BeTree_node_id_cnt := nic;
+      betree_BeTree_node_id_cnt := node_id_cnt1;
       betree_BeTree_root :=
         (Betree_Node_Leaf
           {| betree_Leaf_id := id; betree_Leaf_size := 0%u64 |})
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 2fccf6c0..d5a6e535 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -37,7 +37,7 @@ Definition incr (x : u32) : result u32 :=
 (** [demo::use_incr]:
     Source: 'src/demo.rs', lines 25:0-25:17 *)
 Definition use_incr : result unit :=
-  i <- incr 0%u32; i1 <- incr i; _ <- incr i1; Return tt
+  x <- incr 0%u32; x1 <- incr x; _ <- incr x1; Return tt
 .
 
 (** [demo::CList]
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index ab424e42..d709a8d5 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -26,9 +26,9 @@ Fixpoint hashMap_allocate_slots_loop
   | S n2 =>
     if n1 s> 0%usize
     then (
-      v <- alloc_vec_Vec_push (List_t T) slots List_Nil;
+      slots1 <- alloc_vec_Vec_push (List_t T) slots List_Nil;
       n3 <- usize_sub n1 1%usize;
-      hashMap_allocate_slots_loop T n2 v n3)
+      hashMap_allocate_slots_loop T n2 slots1 n3)
     else Return slots
   end
 .
@@ -190,8 +190,8 @@ Fixpoint hashMap_move_elements_from_list_loop
   | S n1 =>
     match ls with
     | List_Cons k v tl =>
-      hm <- hashMap_insert_no_resize T n1 ntable k v;
-      hashMap_move_elements_from_list_loop T n1 hm tl
+      ntable1 <- hashMap_insert_no_resize T n1 ntable k v;
+      hashMap_move_elements_from_list_loop T n1 ntable1 tl
     | List_Nil => Return ntable
     end
   end
@@ -224,12 +224,10 @@ Fixpoint hashMap_move_elements_loop
           (core_slice_index_SliceIndexUsizeSliceTInst (List_t T)) slots i;
       let (l, index_mut_back) := p in
       let (ls, l1) := core_mem_replace (List_t T) l List_Nil in
-      hm <- hashMap_move_elements_from_list T n1 ntable ls;
+      ntable1 <- hashMap_move_elements_from_list T n1 ntable ls;
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back l1;
-      back_'a <- hashMap_move_elements_loop T n1 hm slots1 i2;
-      let (hm1, v) := back_'a in
-      Return (hm1, v))
+      hashMap_move_elements_loop T n1 ntable1 slots1 i2)
     else Return (ntable, slots)
   end
 .
@@ -241,9 +239,7 @@ Definition hashMap_move_elements
   (slots : alloc_vec_Vec (List_t T)) (i : usize) :
   result ((HashMap_t T) * (alloc_vec_Vec (List_t T)))
   :=
-  back_'a <- hashMap_move_elements_loop T n ntable slots i;
-  let (hm, v) := back_'a in
-  Return (hm, v)
+  hashMap_move_elements_loop T n ntable slots i
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::try_resize]:
@@ -284,9 +280,11 @@ Definition hashMap_insert
   (T : Type) (n : nat) (self : HashMap_t T) (key : usize) (value : T) :
   result (HashMap_t T)
   :=
-  hm <- hashMap_insert_no_resize T n self key value;
-  i <- hashMap_len T hm;
-  if i s> hm.(hashMap_max_load) then hashMap_try_resize T n hm else Return hm
+  self1 <- hashMap_insert_no_resize T n self key value;
+  i <- hashMap_len T self1;
+  if i s> self1.(hashMap_max_load)
+  then hashMap_try_resize T n self1
+  else Return self1
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index aff4995f..9fb3c482 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -29,9 +29,9 @@ Fixpoint hashmap_HashMap_allocate_slots_loop
   | S n2 =>
     if n1 s> 0%usize
     then (
-      v <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
+      slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil;
       n3 <- usize_sub n1 1%usize;
-      hashmap_HashMap_allocate_slots_loop T n2 v n3)
+      hashmap_HashMap_allocate_slots_loop T n2 slots1 n3)
     else Return slots
   end
 .
@@ -204,8 +204,8 @@ Fixpoint hashmap_HashMap_move_elements_from_list_loop
   | S n1 =>
     match ls with
     | Hashmap_List_Cons k v tl =>
-      hm <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
-      hashmap_HashMap_move_elements_from_list_loop T n1 hm tl
+      ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v;
+      hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl
     | Hashmap_List_Nil => Return ntable
     end
   end
@@ -239,12 +239,10 @@ Fixpoint hashmap_HashMap_move_elements_loop
           i;
       let (l, index_mut_back) := p in
       let (ls, l1) := core_mem_replace (hashmap_List_t T) l Hashmap_List_Nil in
-      hm <- hashmap_HashMap_move_elements_from_list T n1 ntable ls;
+      ntable1 <- hashmap_HashMap_move_elements_from_list T n1 ntable ls;
       i2 <- usize_add i 1%usize;
       slots1 <- index_mut_back l1;
-      back_'a <- hashmap_HashMap_move_elements_loop T n1 hm slots1 i2;
-      let (hm1, v) := back_'a in
-      Return (hm1, v))
+      hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2)
     else Return (ntable, slots)
   end
 .
@@ -256,9 +254,7 @@ Definition hashmap_HashMap_move_elements
   (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) :
   result ((hashmap_HashMap_t T) * (alloc_vec_Vec (hashmap_List_t T)))
   :=
-  back_'a <- hashmap_HashMap_move_elements_loop T n ntable slots i;
-  let (hm, v) := back_'a in
-  Return (hm, v)
+  hashmap_HashMap_move_elements_loop T n ntable slots i
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
@@ -304,11 +300,11 @@ Definition hashmap_HashMap_insert
   (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) :
   result (hashmap_HashMap_t T)
   :=
-  hm <- hashmap_HashMap_insert_no_resize T n self key value;
-  i <- hashmap_HashMap_len T hm;
-  if i s> hm.(hashmap_HashMap_max_load)
-  then hashmap_HashMap_try_resize T n hm
-  else Return hm
+  self1 <- hashmap_HashMap_insert_no_resize T n self key value;
+  i <- hashmap_HashMap_len T self1;
+  if i s> self1.(hashmap_HashMap_max_load)
+  then hashmap_HashMap_try_resize T n self1
+  else Return self1
 .
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 91ea88c9..faf91fef 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -45,9 +45,9 @@ Definition custom_swap
   :=
   p <- core_mem_swap T x y st;
   let (st1, p1) := p in
-  let (t, t1) := p1 in
-  let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, t1)) in
-  Return (st1, (t, back_'a))
+  let (x1, y1) := p1 in
+  let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
+  Return (st1, (x1, back_'a))
 .
 
 (** [external::test_custom_swap]:
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 85b54510..7c83a014 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -29,16 +29,16 @@ Definition sum (n : nat) (max : u32) : result u32 :=
 (** [loops::sum_with_mut_borrows]: loop 0:
     Source: 'src/loops.rs', lines 19:0-31:1 *)
 Fixpoint sum_with_mut_borrows_loop
-  (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 :=
+  (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    if mi s< max
+    if i s< max
     then (
-      ms1 <- u32_add ms mi;
-      mi1 <- u32_add mi 1%u32;
-      sum_with_mut_borrows_loop n1 max mi1 ms1)
-    else u32_mul ms 2%u32
+      ms <- u32_add s i;
+      mi <- u32_add i 1%u32;
+      sum_with_mut_borrows_loop n1 max mi ms)
+    else u32_mul s 2%u32
   end
 .
 
@@ -245,10 +245,10 @@ Definition get_elem_mut
   p <-
     alloc_vec_Vec_index_mut (List_t usize) usize
       (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
-  let (l, index_mut_back) := p in
-  p1 <- get_elem_mut_loop n x l;
+  let (ls, index_mut_back) := p in
+  p1 <- get_elem_mut_loop n x ls;
   let (i, back) := p1 in
-  let back1 := fun (ret : usize) => l1 <- back ret; index_mut_back l1 in
+  let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in
   Return (i, back1)
 .
 
@@ -273,10 +273,10 @@ Definition get_elem_shared
   (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
   result usize
   :=
-  l <-
+  ls <-
     alloc_vec_Vec_index (List_t usize) usize
       (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize;
-  get_elem_shared_loop n x l
+  get_elem_shared_loop n x ls
 .
 
 (** [loops::id_mut]:
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 73c4ee58..76dc4cf6 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -475,9 +475,7 @@ Definition id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
   :=
-  let back_'a := fun (ret : (T1 * T2)) => let (t, t1) := ret in Return (t, t1)
-    in
-  Return ((x, y), back_'a)
+  Return ((x, y), Return)
 .
 
 (** [no_nested_borrows::id_mut_pair2]:
@@ -486,10 +484,7 @@ Definition id_mut_pair2
   (T1 T2 : Type) (p : (T1 * T2)) :
   result ((T1 * T2) * ((T1 * T2) -> result (T1 * T2)))
   :=
-  let (t, t1) := p in
-  let back_'a :=
-    fun (ret : (T1 * T2)) => let (t2, t3) := ret in Return (t2, t3) in
-  Return ((t, t1), back_'a)
+  let (t, t1) := p in Return ((t, t1), Return)
 .
 
 (** [no_nested_borrows::id_mut_pair3]:
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 769cf34c..ad77fa2a 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 :=
 (** [paper::test_incr]:
     Source: 'src/paper.rs', lines 8:0-8:18 *)
 Definition test_incr : result unit :=
-  i <- ref_incr 0%i32; if negb (i s= 1%i32) then Fail_ Failure else Return tt
+  x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Return tt
 .
 
 (** Unit test for [paper::test_incr] *)
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index 15c82e93..731c7290 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -28,17 +28,17 @@ let array_to_mut_slice_
 (** [arrays::array_len]:
     Source: 'src/arrays.rs', lines 25:0-25:40 *)
 let array_len (t : Type0) (s : array t 32) : result usize =
-  let* s1 = array_to_slice t 32 s in let i = slice_len t s1 in Return i
+  let* s1 = array_to_slice t 32 s in Return (slice_len t s1)
 
 (** [arrays::shared_array_len]:
     Source: 'src/arrays.rs', lines 29:0-29:48 *)
 let shared_array_len (t : Type0) (s : array t 32) : result usize =
-  let* s1 = array_to_slice t 32 s in let i = slice_len t s1 in Return i
+  let* s1 = array_to_slice t 32 s in Return (slice_len t s1)
 
 (** [arrays::shared_slice_len]:
     Source: 'src/arrays.rs', lines 33:0-33:44 *)
 let shared_slice_len (t : Type0) (s : slice t) : result usize =
-  let i = slice_len t s in Return i
+  Return (slice_len t s)
 
 (** [arrays::index_array_shared]:
     Source: 'src/arrays.rs', lines 37:0-37:57 *)
@@ -268,8 +268,8 @@ let update_mut_slice (x : slice u32) : result (slice u32) =
 let update_all : result unit =
   let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in
   let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in
-  let* a = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in
-  let* (s, to_slice_mut_back) = array_to_slice_mut u32 2 a in
+  let* x = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in
+  let* (s, to_slice_mut_back) = array_to_slice_mut u32 2 x in
   let* s1 = update_mut_slice s in
   let* _ = to_slice_mut_back s1 in
   Return ()
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 74044961..2469f98c 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -170,13 +170,14 @@ let betree_Leaf_split
   let (content0, content1) = p in
   let* p1 = betree_List_hd (u64 & u64) content1 in
   let (pivot, _) = p1 in
-  let* (id0, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in
-  let* (id1, nic1) = betree_NodeIdCounter_fresh_id nic in
+  let* (id0, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in
+  let* (id1, node_id_cnt2) = betree_NodeIdCounter_fresh_id node_id_cnt1 in
   let* (st1, _) = betree_store_leaf_node id0 content0 st in
   let* (st2, _) = betree_store_leaf_node id1 content1 st1 in
   let n = Betree_Node_Leaf { id = id0; size = params.split_size } in
   let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in
-  Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, nic1))
+  Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 },
+    node_id_cnt2))
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
     Source: 'src/betree.rs', lines 789:4-792:34 *)
@@ -229,21 +230,21 @@ let rec betree_Node_apply_upserts
   let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in
   if b
   then
-    let* (msg, l) = betree_List_pop_front (u64 & betree_Message_t) msgs in
+    let* (msg, msgs1) = betree_List_pop_front (u64 & betree_Message_t) msgs in
     let (_, m) = msg in
     begin match m with
     | Betree_Message_Insert _ -> Fail Failure
     | Betree_Message_Delete -> Fail Failure
     | Betree_Message_Upsert s ->
       let* v = betree_upsert_update prev s in
-      betree_Node_apply_upserts l (Some v) key st
+      betree_Node_apply_upserts msgs1 (Some v) key st
     end
   else
     let* (st1, v) = core_option_Option_unwrap u64 prev st in
-    let* l =
+    let* msgs1 =
       betree_List_push_front (u64 & betree_Message_t) msgs (key,
         Betree_Message_Insert v) in
-    Return (st1, (v, l))
+    Return (st1, (v, msgs1))
 
 (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
     Source: 'src/betree.rs', lines 395:4-395:63 *)
@@ -277,10 +278,11 @@ and betree_Node_lookup
       let (k, msg) = p in
       if k <> key
       then
-        let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in
+        let* (st2, (o, node1)) =
+          betree_Internal_lookup_in_children node key st1 in
         let* _ =
           lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in
-        Return (st2, (o, Betree_Node_Internal i))
+        Return (st2, (o, Betree_Node_Internal node1))
       else
         begin match msg with
         | Betree_Message_Insert v ->
@@ -294,19 +296,20 @@ and betree_Node_lookup
               Betree_Message_Delete) l) in
           Return (st1, (None, Betree_Node_Internal node))
         | Betree_Message_Upsert ufs ->
-          let* (st2, (v, i)) = betree_Internal_lookup_in_children node key st1
-            in
-          let* (st3, (v1, l1)) =
+          let* (st2, (v, node1)) =
+            betree_Internal_lookup_in_children node key st1 in
+          let* (st3, (v1, pending1)) =
             betree_Node_apply_upserts (Betree_List_Cons (k,
               Betree_Message_Upsert ufs) l) v key st2 in
-          let* msgs1 = lookup_first_message_for_key_back l1 in
-          let* (st4, _) = betree_store_internal_node i.id msgs1 st3 in
-          Return (st4, (Some v1, Betree_Node_Internal i))
+          let* msgs1 = lookup_first_message_for_key_back pending1 in
+          let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in
+          Return (st4, (Some v1, Betree_Node_Internal node1))
         end
     | Betree_List_Nil ->
-      let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in
+      let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1
+        in
       let* _ = lookup_first_message_for_key_back Betree_List_Nil in
-      Return (st2, (o, Betree_Node_Internal i))
+      Return (st2, (o, Betree_Node_Internal node1))
     end
   | Betree_Node_Leaf node ->
     let* (st1, bindings) = betree_load_leaf_node node.id st in
@@ -326,10 +329,10 @@ let rec betree_Node_filter_messages_for_key
     let (k, m) = p in
     if k = key
     then
-      let* (_, l1) =
+      let* (_, msgs1) =
         betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m)
           l) in
-      betree_Node_filter_messages_for_key key l1
+      betree_Node_filter_messages_for_key key msgs1
     else Return (Betree_List_Cons (k, m) l)
   | Betree_List_Nil -> Return Betree_List_Nil
   end
@@ -372,49 +375,51 @@ let betree_Node_apply_to_internal
   then
     begin match new_msg with
     | Betree_Message_Insert i ->
-      let* l = betree_Node_filter_messages_for_key key msgs1 in
-      let* l1 =
-        betree_List_push_front (u64 & betree_Message_t) l (key,
+      let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in
+      let* msgs3 =
+        betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
           Betree_Message_Insert i) in
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | Betree_Message_Delete ->
-      let* l = betree_Node_filter_messages_for_key key msgs1 in
-      let* l1 =
-        betree_List_push_front (u64 & betree_Message_t) l (key,
+      let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in
+      let* msgs3 =
+        betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
           Betree_Message_Delete) in
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | Betree_Message_Upsert s ->
       let* p = betree_List_hd (u64 & betree_Message_t) msgs1 in
       let (_, m) = p in
       begin match m with
       | Betree_Message_Insert prev ->
         let* v = betree_upsert_update (Some prev) s in
-        let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in
-        let* l1 =
-          betree_List_push_front (u64 & betree_Message_t) l (key,
+        let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1
+          in
+        let* msgs3 =
+          betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
             Betree_Message_Insert v) in
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | Betree_Message_Delete ->
-        let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in
+        let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1
+          in
         let* v = betree_upsert_update None s in
-        let* l1 =
-          betree_List_push_front (u64 & betree_Message_t) l (key,
+        let* msgs3 =
+          betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
             Betree_Message_Insert v) in
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | Betree_Message_Upsert _ ->
         let* (msgs2, lookup_first_message_after_key_back) =
           betree_Node_lookup_first_message_after_key key msgs1 in
-        let* l =
+        let* msgs3 =
           betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
             Betree_Message_Upsert s) in
-        let* msgs3 = lookup_first_message_after_key_back l in
-        lookup_first_message_for_key_back msgs3
+        let* msgs4 = lookup_first_message_after_key_back msgs3 in
+        lookup_first_message_for_key_back msgs4
       end
     end
   else
-    let* l =
+    let* msgs2 =
       betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in
-    lookup_first_message_for_key_back l
+    lookup_first_message_for_key_back msgs2
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
     Source: 'src/betree.rs', lines 502:4-505:5 *)
@@ -427,8 +432,8 @@ let rec betree_Node_apply_messages_to_internal
   begin match new_msgs with
   | Betree_List_Cons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
-    let* l = betree_Node_apply_to_internal msgs i m in
-    betree_Node_apply_messages_to_internal l new_msgs_tl
+    let* msgs1 = betree_Node_apply_to_internal msgs i m in
+    betree_Node_apply_messages_to_internal msgs1 new_msgs_tl
   | Betree_List_Nil -> Return msgs
   end
 
@@ -468,28 +473,28 @@ let betree_Node_apply_to_leaf
   let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in
   if b
   then
-    let* (hd, l) = betree_List_pop_front (u64 & u64) bindings1 in
+    let* (hd, bindings2) = betree_List_pop_front (u64 & u64) bindings1 in
     begin match new_msg with
     | Betree_Message_Insert v ->
-      let* l1 = betree_List_push_front (u64 & u64) l (key, v) in
-      lookup_mut_in_bindings_back l1
-    | Betree_Message_Delete -> lookup_mut_in_bindings_back l
+      let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in
+      lookup_mut_in_bindings_back bindings3
+    | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings2
     | Betree_Message_Upsert s ->
       let (_, i) = hd in
       let* v = betree_upsert_update (Some i) s in
-      let* l1 = betree_List_push_front (u64 & u64) l (key, v) in
-      lookup_mut_in_bindings_back l1
+      let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in
+      lookup_mut_in_bindings_back bindings3
     end
   else
     begin match new_msg with
     | Betree_Message_Insert v ->
-      let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in
-      lookup_mut_in_bindings_back l
+      let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in
+      lookup_mut_in_bindings_back bindings2
     | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings1
     | Betree_Message_Upsert s ->
       let* v = betree_upsert_update None s in
-      let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in
-      lookup_mut_in_bindings_back l
+      let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in
+      lookup_mut_in_bindings_back bindings2
     end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]:
@@ -503,8 +508,8 @@ let rec betree_Node_apply_messages_to_leaf
   begin match new_msgs with
   | Betree_List_Cons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
-    let* l = betree_Node_apply_to_leaf bindings i m in
-    betree_Node_apply_messages_to_leaf l new_msgs_tl
+    let* bindings1 = betree_Node_apply_to_leaf bindings i m in
+    betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl
   | Betree_List_Nil -> Return bindings
   end
 
@@ -558,31 +563,31 @@ and betree_Node_apply_messages
   begin match self with
   | Betree_Node_Internal node ->
     let* (st1, content) = betree_load_internal_node node.id st in
-    let* l = betree_Node_apply_messages_to_internal content msgs in
-    let* num_msgs = betree_List_len (u64 & betree_Message_t) l in
+    let* content1 = betree_Node_apply_messages_to_internal content msgs in
+    let* num_msgs = betree_List_len (u64 & betree_Message_t) content1 in
     if num_msgs >= params.min_flush_size
     then
-      let* (st2, (content1, p)) =
-        betree_Internal_flush node params node_id_cnt l st1 in
+      let* (st2, (content2, p)) =
+        betree_Internal_flush node params node_id_cnt content1 st1 in
       let (node1, node_id_cnt1) = p in
-      let* (st3, _) = betree_store_internal_node node1.id content1 st2 in
+      let* (st3, _) = betree_store_internal_node node1.id content2 st2 in
       Return (st3, (Betree_Node_Internal node1, node_id_cnt1))
     else
-      let* (st2, _) = betree_store_internal_node node.id l st1 in
+      let* (st2, _) = betree_store_internal_node node.id content1 st1 in
       Return (st2, (Betree_Node_Internal node, node_id_cnt))
   | Betree_Node_Leaf node ->
     let* (st1, content) = betree_load_leaf_node node.id st in
-    let* l = betree_Node_apply_messages_to_leaf content msgs in
-    let* len = betree_List_len (u64 & u64) l in
+    let* content1 = betree_Node_apply_messages_to_leaf content msgs in
+    let* len = betree_List_len (u64 & u64) content1 in
     let* i = u64_mul 2 params.split_size in
     if len >= i
     then
-      let* (st2, (new_node, nic)) =
-        betree_Leaf_split node l params node_id_cnt st1 in
+      let* (st2, (new_node, node_id_cnt1)) =
+        betree_Leaf_split node content1 params node_id_cnt st1 in
       let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in
-      Return (st3, (Betree_Node_Internal new_node, nic))
+      Return (st3, (Betree_Node_Internal new_node, node_id_cnt1))
     else
-      let* (st2, _) = betree_store_leaf_node node.id l st1 in
+      let* (st2, _) = betree_store_leaf_node node.id content1 st1 in
       Return (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt))
   end
 
@@ -607,12 +612,12 @@ let betree_BeTree_new
   result (state & betree_BeTree_t)
   =
   let* node_id_cnt = betree_NodeIdCounter_new in
-  let* (id, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in
+  let* (id, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in
   let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in
   Return (st1,
     {
       params = { min_flush_size = min_flush_size; split_size = split_size };
-      node_id_cnt = nic;
+      node_id_cnt = node_id_cnt1;
       root = (Betree_Node_Leaf { id = id; size = 0 })
     })
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 74044961..2469f98c 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -170,13 +170,14 @@ let betree_Leaf_split
   let (content0, content1) = p in
   let* p1 = betree_List_hd (u64 & u64) content1 in
   let (pivot, _) = p1 in
-  let* (id0, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in
-  let* (id1, nic1) = betree_NodeIdCounter_fresh_id nic in
+  let* (id0, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in
+  let* (id1, node_id_cnt2) = betree_NodeIdCounter_fresh_id node_id_cnt1 in
   let* (st1, _) = betree_store_leaf_node id0 content0 st in
   let* (st2, _) = betree_store_leaf_node id1 content1 st1 in
   let n = Betree_Node_Leaf { id = id0; size = params.split_size } in
   let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in
-  Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 }, nic1))
+  Return (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 },
+    node_id_cnt2))
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
     Source: 'src/betree.rs', lines 789:4-792:34 *)
@@ -229,21 +230,21 @@ let rec betree_Node_apply_upserts
   let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in
   if b
   then
-    let* (msg, l) = betree_List_pop_front (u64 & betree_Message_t) msgs in
+    let* (msg, msgs1) = betree_List_pop_front (u64 & betree_Message_t) msgs in
     let (_, m) = msg in
     begin match m with
     | Betree_Message_Insert _ -> Fail Failure
     | Betree_Message_Delete -> Fail Failure
     | Betree_Message_Upsert s ->
       let* v = betree_upsert_update prev s in
-      betree_Node_apply_upserts l (Some v) key st
+      betree_Node_apply_upserts msgs1 (Some v) key st
     end
   else
     let* (st1, v) = core_option_Option_unwrap u64 prev st in
-    let* l =
+    let* msgs1 =
       betree_List_push_front (u64 & betree_Message_t) msgs (key,
         Betree_Message_Insert v) in
-    Return (st1, (v, l))
+    Return (st1, (v, msgs1))
 
 (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
     Source: 'src/betree.rs', lines 395:4-395:63 *)
@@ -277,10 +278,11 @@ and betree_Node_lookup
       let (k, msg) = p in
       if k <> key
       then
-        let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in
+        let* (st2, (o, node1)) =
+          betree_Internal_lookup_in_children node key st1 in
         let* _ =
           lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l) in
-        Return (st2, (o, Betree_Node_Internal i))
+        Return (st2, (o, Betree_Node_Internal node1))
       else
         begin match msg with
         | Betree_Message_Insert v ->
@@ -294,19 +296,20 @@ and betree_Node_lookup
               Betree_Message_Delete) l) in
           Return (st1, (None, Betree_Node_Internal node))
         | Betree_Message_Upsert ufs ->
-          let* (st2, (v, i)) = betree_Internal_lookup_in_children node key st1
-            in
-          let* (st3, (v1, l1)) =
+          let* (st2, (v, node1)) =
+            betree_Internal_lookup_in_children node key st1 in
+          let* (st3, (v1, pending1)) =
             betree_Node_apply_upserts (Betree_List_Cons (k,
               Betree_Message_Upsert ufs) l) v key st2 in
-          let* msgs1 = lookup_first_message_for_key_back l1 in
-          let* (st4, _) = betree_store_internal_node i.id msgs1 st3 in
-          Return (st4, (Some v1, Betree_Node_Internal i))
+          let* msgs1 = lookup_first_message_for_key_back pending1 in
+          let* (st4, _) = betree_store_internal_node node1.id msgs1 st3 in
+          Return (st4, (Some v1, Betree_Node_Internal node1))
         end
     | Betree_List_Nil ->
-      let* (st2, (o, i)) = betree_Internal_lookup_in_children node key st1 in
+      let* (st2, (o, node1)) = betree_Internal_lookup_in_children node key st1
+        in
       let* _ = lookup_first_message_for_key_back Betree_List_Nil in
-      Return (st2, (o, Betree_Node_Internal i))
+      Return (st2, (o, Betree_Node_Internal node1))
     end
   | Betree_Node_Leaf node ->
     let* (st1, bindings) = betree_load_leaf_node node.id st in
@@ -326,10 +329,10 @@ let rec betree_Node_filter_messages_for_key
     let (k, m) = p in
     if k = key
     then
-      let* (_, l1) =
+      let* (_, msgs1) =
         betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m)
           l) in
-      betree_Node_filter_messages_for_key key l1
+      betree_Node_filter_messages_for_key key msgs1
     else Return (Betree_List_Cons (k, m) l)
   | Betree_List_Nil -> Return Betree_List_Nil
   end
@@ -372,49 +375,51 @@ let betree_Node_apply_to_internal
   then
     begin match new_msg with
     | Betree_Message_Insert i ->
-      let* l = betree_Node_filter_messages_for_key key msgs1 in
-      let* l1 =
-        betree_List_push_front (u64 & betree_Message_t) l (key,
+      let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in
+      let* msgs3 =
+        betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
           Betree_Message_Insert i) in
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | Betree_Message_Delete ->
-      let* l = betree_Node_filter_messages_for_key key msgs1 in
-      let* l1 =
-        betree_List_push_front (u64 & betree_Message_t) l (key,
+      let* msgs2 = betree_Node_filter_messages_for_key key msgs1 in
+      let* msgs3 =
+        betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
           Betree_Message_Delete) in
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | Betree_Message_Upsert s ->
       let* p = betree_List_hd (u64 & betree_Message_t) msgs1 in
       let (_, m) = p in
       begin match m with
       | Betree_Message_Insert prev ->
         let* v = betree_upsert_update (Some prev) s in
-        let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in
-        let* l1 =
-          betree_List_push_front (u64 & betree_Message_t) l (key,
+        let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1
+          in
+        let* msgs3 =
+          betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
             Betree_Message_Insert v) in
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | Betree_Message_Delete ->
-        let* (_, l) = betree_List_pop_front (u64 & betree_Message_t) msgs1 in
+        let* (_, msgs2) = betree_List_pop_front (u64 & betree_Message_t) msgs1
+          in
         let* v = betree_upsert_update None s in
-        let* l1 =
-          betree_List_push_front (u64 & betree_Message_t) l (key,
+        let* msgs3 =
+          betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
             Betree_Message_Insert v) in
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | Betree_Message_Upsert _ ->
         let* (msgs2, lookup_first_message_after_key_back) =
           betree_Node_lookup_first_message_after_key key msgs1 in
-        let* l =
+        let* msgs3 =
           betree_List_push_front (u64 & betree_Message_t) msgs2 (key,
             Betree_Message_Upsert s) in
-        let* msgs3 = lookup_first_message_after_key_back l in
-        lookup_first_message_for_key_back msgs3
+        let* msgs4 = lookup_first_message_after_key_back msgs3 in
+        lookup_first_message_for_key_back msgs4
       end
     end
   else
-    let* l =
+    let* msgs2 =
       betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in
-    lookup_first_message_for_key_back l
+    lookup_first_message_for_key_back msgs2
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
     Source: 'src/betree.rs', lines 502:4-505:5 *)
@@ -427,8 +432,8 @@ let rec betree_Node_apply_messages_to_internal
   begin match new_msgs with
   | Betree_List_Cons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
-    let* l = betree_Node_apply_to_internal msgs i m in
-    betree_Node_apply_messages_to_internal l new_msgs_tl
+    let* msgs1 = betree_Node_apply_to_internal msgs i m in
+    betree_Node_apply_messages_to_internal msgs1 new_msgs_tl
   | Betree_List_Nil -> Return msgs
   end
 
@@ -468,28 +473,28 @@ let betree_Node_apply_to_leaf
   let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in
   if b
   then
-    let* (hd, l) = betree_List_pop_front (u64 & u64) bindings1 in
+    let* (hd, bindings2) = betree_List_pop_front (u64 & u64) bindings1 in
     begin match new_msg with
     | Betree_Message_Insert v ->
-      let* l1 = betree_List_push_front (u64 & u64) l (key, v) in
-      lookup_mut_in_bindings_back l1
-    | Betree_Message_Delete -> lookup_mut_in_bindings_back l
+      let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in
+      lookup_mut_in_bindings_back bindings3
+    | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings2
     | Betree_Message_Upsert s ->
       let (_, i) = hd in
       let* v = betree_upsert_update (Some i) s in
-      let* l1 = betree_List_push_front (u64 & u64) l (key, v) in
-      lookup_mut_in_bindings_back l1
+      let* bindings3 = betree_List_push_front (u64 & u64) bindings2 (key, v) in
+      lookup_mut_in_bindings_back bindings3
     end
   else
     begin match new_msg with
     | Betree_Message_Insert v ->
-      let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in
-      lookup_mut_in_bindings_back l
+      let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in
+      lookup_mut_in_bindings_back bindings2
     | Betree_Message_Delete -> lookup_mut_in_bindings_back bindings1
     | Betree_Message_Upsert s ->
       let* v = betree_upsert_update None s in
-      let* l = betree_List_push_front (u64 & u64) bindings1 (key, v) in
-      lookup_mut_in_bindings_back l
+      let* bindings2 = betree_List_push_front (u64 & u64) bindings1 (key, v) in
+      lookup_mut_in_bindings_back bindings2
     end
 
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]:
@@ -503,8 +508,8 @@ let rec betree_Node_apply_messages_to_leaf
   begin match new_msgs with
   | Betree_List_Cons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
-    let* l = betree_Node_apply_to_leaf bindings i m in
-    betree_Node_apply_messages_to_leaf l new_msgs_tl
+    let* bindings1 = betree_Node_apply_to_leaf bindings i m in
+    betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl
   | Betree_List_Nil -> Return bindings
   end
 
@@ -558,31 +563,31 @@ and betree_Node_apply_messages
   begin match self with
   | Betree_Node_Internal node ->
     let* (st1, content) = betree_load_internal_node node.id st in
-    let* l = betree_Node_apply_messages_to_internal content msgs in
-    let* num_msgs = betree_List_len (u64 & betree_Message_t) l in
+    let* content1 = betree_Node_apply_messages_to_internal content msgs in
+    let* num_msgs = betree_List_len (u64 & betree_Message_t) content1 in
     if num_msgs >= params.min_flush_size
     then
-      let* (st2, (content1, p)) =
-        betree_Internal_flush node params node_id_cnt l st1 in
+      let* (st2, (content2, p)) =
+        betree_Internal_flush node params node_id_cnt content1 st1 in
       let (node1, node_id_cnt1) = p in
-      let* (st3, _) = betree_store_internal_node node1.id content1 st2 in
+      let* (st3, _) = betree_store_internal_node node1.id content2 st2 in
       Return (st3, (Betree_Node_Internal node1, node_id_cnt1))
     else
-      let* (st2, _) = betree_store_internal_node node.id l st1 in
+      let* (st2, _) = betree_store_internal_node node.id content1 st1 in
       Return (st2, (Betree_Node_Internal node, node_id_cnt))
   | Betree_Node_Leaf node ->
     let* (st1, content) = betree_load_leaf_node node.id st in
-    let* l = betree_Node_apply_messages_to_leaf content msgs in
-    let* len = betree_List_len (u64 & u64) l in
+    let* content1 = betree_Node_apply_messages_to_leaf content msgs in
+    let* len = betree_List_len (u64 & u64) content1 in
     let* i = u64_mul 2 params.split_size in
     if len >= i
     then
-      let* (st2, (new_node, nic)) =
-        betree_Leaf_split node l params node_id_cnt st1 in
+      let* (st2, (new_node, node_id_cnt1)) =
+        betree_Leaf_split node content1 params node_id_cnt st1 in
       let* (st3, _) = betree_store_leaf_node node.id Betree_List_Nil st2 in
-      Return (st3, (Betree_Node_Internal new_node, nic))
+      Return (st3, (Betree_Node_Internal new_node, node_id_cnt1))
     else
-      let* (st2, _) = betree_store_leaf_node node.id l st1 in
+      let* (st2, _) = betree_store_leaf_node node.id content1 st1 in
       Return (st2, (Betree_Node_Leaf { node with size = len }, node_id_cnt))
   end
 
@@ -607,12 +612,12 @@ let betree_BeTree_new
   result (state & betree_BeTree_t)
   =
   let* node_id_cnt = betree_NodeIdCounter_new in
-  let* (id, nic) = betree_NodeIdCounter_fresh_id node_id_cnt in
+  let* (id, node_id_cnt1) = betree_NodeIdCounter_fresh_id node_id_cnt in
   let* (st1, _) = betree_store_leaf_node id Betree_List_Nil st in
   Return (st1,
     {
       params = { min_flush_size = min_flush_size; split_size = split_size };
-      node_id_cnt = nic;
+      node_id_cnt = node_id_cnt1;
       root = (Betree_Node_Leaf { id = id; size = 0 })
     })
 
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index 4ad7cb65..d93bc847 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -31,7 +31,7 @@ let incr (x : u32) : result u32 =
 (** [demo::use_incr]:
     Source: 'src/demo.rs', lines 25:0-25:17 *)
 let use_incr : result unit =
-  let* i = incr 0 in let* i1 = incr i in let* _ = incr i1 in Return ()
+  let* x = incr 0 in let* x1 = incr x in let* _ = incr x1 in Return ()
 
 (** [demo::CList]
     Source: 'src/demo.rs', lines 34:0-34:17 *)
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 7ca8b9c1..fba711f1 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -21,9 +21,9 @@ let rec hashMap_allocate_slots_loop
   =
   if n > 0
   then
-    let* v = alloc_vec_Vec_push (list_t t) slots List_Nil in
+    let* slots1 = alloc_vec_Vec_push (list_t t) slots List_Nil in
     let* n1 = usize_sub n 1 in
-    hashMap_allocate_slots_loop t v n1
+    hashMap_allocate_slots_loop t slots1 n1
   else Return slots
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
@@ -142,8 +142,8 @@ let rec hashMap_move_elements_from_list_loop
   =
   begin match ls with
   | List_Cons k v tl ->
-    let* hm = hashMap_insert_no_resize t ntable k v in
-    hashMap_move_elements_from_list_loop t hm tl
+    let* ntable1 = hashMap_insert_no_resize t ntable k v in
+    hashMap_move_elements_from_list_loop t ntable1 tl
   | List_Nil -> Return ntable
   end
 
@@ -168,12 +168,10 @@ let rec hashMap_move_elements_loop
       alloc_vec_Vec_index_mut (list_t t) usize
         (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) slots i in
     let (ls, l1) = core_mem_replace (list_t t) l List_Nil in
-    let* hm = hashMap_move_elements_from_list t ntable ls in
+    let* ntable1 = hashMap_move_elements_from_list t ntable ls in
     let* i2 = usize_add i 1 in
     let* slots1 = index_mut_back l1 in
-    let* back_'a = hashMap_move_elements_loop t hm slots1 i2 in
-    let (hm1, v) = back_'a in
-    Return (hm1, v)
+    hashMap_move_elements_loop t ntable1 slots1 i2
   else Return (ntable, slots)
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements]:
@@ -183,9 +181,7 @@ let hashMap_move_elements
   (i : usize) :
   result ((hashMap_t t) & (alloc_vec_Vec (list_t t)))
   =
-  let* back_'a = hashMap_move_elements_loop t ntable slots i in
-  let (hm, v) = back_'a in
-  Return (hm, v)
+  hashMap_move_elements_loop t ntable slots i
 
 (** [hashmap::{hashmap::HashMap<T>}::try_resize]:
     Source: 'src/hashmap.rs', lines 140:4-140:28 *)
@@ -213,9 +209,9 @@ let hashMap_insert
   (t : Type0) (self : hashMap_t t) (key : usize) (value : t) :
   result (hashMap_t t)
   =
-  let* hm = hashMap_insert_no_resize t self key value in
-  let* i = hashMap_len t hm in
-  if i > hm.max_load then hashMap_try_resize t hm else Return hm
+  let* self1 = hashMap_insert_no_resize t self key value in
+  let* i = hashMap_len t self1 in
+  if i > self1.max_load then hashMap_try_resize t self1 else Return self1
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
     Source: 'src/hashmap.rs', lines 206:4-219:5 *)
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 9b5baaeb..97f4151f 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -22,9 +22,10 @@ let rec hashmap_HashMap_allocate_slots_loop
   =
   if n > 0
   then
-    let* v = alloc_vec_Vec_push (hashmap_List_t t) slots Hashmap_List_Nil in
+    let* slots1 = alloc_vec_Vec_push (hashmap_List_t t) slots Hashmap_List_Nil
+      in
     let* n1 = usize_sub n 1 in
-    hashmap_HashMap_allocate_slots_loop t v n1
+    hashmap_HashMap_allocate_slots_loop t slots1 n1
   else Return slots
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]:
@@ -149,8 +150,8 @@ let rec hashmap_HashMap_move_elements_from_list_loop
   =
   begin match ls with
   | Hashmap_List_Cons k v tl ->
-    let* hm = hashmap_HashMap_insert_no_resize t ntable k v in
-    hashmap_HashMap_move_elements_from_list_loop t hm tl
+    let* ntable1 = hashmap_HashMap_insert_no_resize t ntable k v in
+    hashmap_HashMap_move_elements_from_list_loop t ntable1 tl
   | Hashmap_List_Nil -> Return ntable
   end
 
@@ -178,12 +179,10 @@ let rec hashmap_HashMap_move_elements_loop
         (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t)) slots i
       in
     let (ls, l1) = core_mem_replace (hashmap_List_t t) l Hashmap_List_Nil in
-    let* hm = hashmap_HashMap_move_elements_from_list t ntable ls in
+    let* ntable1 = hashmap_HashMap_move_elements_from_list t ntable ls in
     let* i2 = usize_add i 1 in
     let* slots1 = index_mut_back l1 in
-    let* back_'a = hashmap_HashMap_move_elements_loop t hm slots1 i2 in
-    let (hm1, v) = back_'a in
-    Return (hm1, v)
+    hashmap_HashMap_move_elements_loop t ntable1 slots1 i2
   else Return (ntable, slots)
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]:
@@ -193,9 +192,7 @@ let hashmap_HashMap_move_elements
   (slots : alloc_vec_Vec (hashmap_List_t t)) (i : usize) :
   result ((hashmap_HashMap_t t) & (alloc_vec_Vec (hashmap_List_t t)))
   =
-  let* back_'a = hashmap_HashMap_move_elements_loop t ntable slots i in
-  let (hm, v) = back_'a in
-  Return (hm, v)
+  hashmap_HashMap_move_elements_loop t ntable slots i
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
     Source: 'src/hashmap.rs', lines 140:4-140:28 *)
@@ -223,9 +220,11 @@ let hashmap_HashMap_insert
   (t : Type0) (self : hashmap_HashMap_t t) (key : usize) (value : t) :
   result (hashmap_HashMap_t t)
   =
-  let* hm = hashmap_HashMap_insert_no_resize t self key value in
-  let* i = hashmap_HashMap_len t hm in
-  if i > hm.max_load then hashmap_HashMap_try_resize t hm else Return hm
+  let* self1 = hashmap_HashMap_insert_no_resize t self key value in
+  let* i = hashmap_HashMap_len t self1 in
+  if i > self1.max_load
+  then hashmap_HashMap_try_resize t self1
+  else Return self1
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
     Source: 'src/hashmap.rs', lines 206:4-219:5 *)
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 6672b523..3ba20022 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -33,8 +33,8 @@ let custom_swap
   (t : Type0) (x : t) (y : t) (st : state) :
   result (state & (t & (t -> state -> result (state & (t & t)))))
   =
-  let* (st1, (x1, x2)) = core_mem_swap t x y st in
-  let back_'a = fun ret st2 -> Return (st2, (ret, x2)) in
+  let* (st1, (x1, y1)) = core_mem_swap t x y st in
+  let back_'a = fun ret st2 -> Return (st2, (ret, y1)) in
   Return (st1, (x1, back_'a))
 
 (** [external::test_custom_swap]:
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index c8ed16f4..e43f8170 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -13,8 +13,7 @@ unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
 (** [loops::sum_with_mut_borrows]: decreases clause
     Source: 'src/loops.rs', lines 19:0-31:1 *)
 unfold
-let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat
-  =
+let sum_with_mut_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
   admit ()
 
 (** [loops::sum_with_shared_borrows]: decreases clause
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index c87f693b..7c099da2 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -25,15 +25,15 @@ let sum (max : u32) : result u32 =
 (** [loops::sum_with_mut_borrows]: loop 0:
     Source: 'src/loops.rs', lines 19:0-31:1 *)
 let rec sum_with_mut_borrows_loop
-  (max : u32) (mi : u32) (ms : u32) :
-  Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms))
+  (max : u32) (i : u32) (s : u32) :
+  Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max i s))
   =
-  if mi < max
+  if i < max
   then
-    let* ms1 = u32_add ms mi in
-    let* mi1 = u32_add mi 1 in
-    sum_with_mut_borrows_loop max mi1 ms1
-  else u32_mul ms 2
+    let* ms = u32_add s i in
+    let* mi = u32_add i 1 in
+    sum_with_mut_borrows_loop max mi ms
+  else u32_mul s 2
 
 (** [loops::sum_with_mut_borrows]:
     Source: 'src/loops.rs', lines 19:0-19:44 *)
@@ -185,11 +185,11 @@ let get_elem_mut
   (slots : alloc_vec_Vec (list_t usize)) (x : usize) :
   result (usize & (usize -> result (alloc_vec_Vec (list_t usize))))
   =
-  let* (l, index_mut_back) =
+  let* (ls, index_mut_back) =
     alloc_vec_Vec_index_mut (list_t usize) usize
       (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in
-  let* (i, back) = get_elem_mut_loop x l in
-  let back1 = fun ret -> let* l1 = back ret in index_mut_back l1 in
+  let* (i, back) = get_elem_mut_loop x ls in
+  let back1 = fun ret -> let* l = back ret in index_mut_back l in
   Return (i, back1)
 
 (** [loops::get_elem_shared]: loop 0:
@@ -207,10 +207,10 @@ let rec get_elem_shared_loop
     Source: 'src/loops.rs', lines 129:0-129:68 *)
 let get_elem_shared
   (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize =
-  let* l =
+  let* ls =
     alloc_vec_Vec_index (list_t usize) usize
       (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in
-  get_elem_shared_loop x l
+  get_elem_shared_loop x ls
 
 (** [loops::id_mut]:
     Source: 'src/loops.rs', lines 145:0-145:50 *)
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index c71f8dbb..db63eb0d 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -425,8 +425,7 @@ let id_mut_pair1
   (t1 t2 : Type0) (x : t1) (y : t2) :
   result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2)))
   =
-  let back_'a = fun ret -> let (x1, x2) = ret in Return (x1, x2) in
-  Return ((x, y), back_'a)
+  Return ((x, y), Return)
 
 (** [no_nested_borrows::id_mut_pair2]:
     Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 *)
@@ -434,9 +433,7 @@ let id_mut_pair2
   (t1 t2 : Type0) (p : (t1 & t2)) :
   result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2)))
   =
-  let (x, x1) = p in
-  let back_'a = fun ret -> let (x2, x3) = ret in Return (x2, x3) in
-  Return ((x, x1), back_'a)
+  let (x, x1) = p in Return ((x, x1), Return)
 
 (** [no_nested_borrows::id_mut_pair3]:
     Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 *)
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index cf4dc454..ddc5e7a8 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -13,7 +13,7 @@ let ref_incr (x : i32) : result i32 =
 (** [paper::test_incr]:
     Source: 'src/paper.rs', lines 8:0-8:18 *)
 let test_incr : result unit =
-  let* i = ref_incr 0 in if not (i = 1) then Fail Failure else Return ()
+  let* x = ref_incr 0 in if not (x = 1) then Fail Failure else Return ()
 
 (** Unit test for [paper::test_incr] *)
 let _ = assert_norm (test_incr = Return ())
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index cd1b6544..207f31b9 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -35,22 +35,19 @@ def array_to_mut_slice_
 def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
-  let i := Slice.len T s1
-  Result.ret i
+  Result.ret (Slice.len T s1)
 
 /- [arrays::shared_array_len]:
    Source: 'src/arrays.rs', lines 29:0-29:48 -/
 def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
-  let i := Slice.len T s1
-  Result.ret i
+  Result.ret (Slice.len T s1)
 
 /- [arrays::shared_slice_len]:
    Source: 'src/arrays.rs', lines 33:0-33:44 -/
 def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
-  let i := Slice.len T s
-  Result.ret i
+  Result.ret (Slice.len T s)
 
 /- [arrays::index_array_shared]:
    Source: 'src/arrays.rs', lines 37:0-37:57 -/
@@ -305,8 +302,8 @@ def update_all : Result Unit :=
   do
   let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
-  let a ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
-  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize a
+  let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize x
   let s1 ← update_mut_slice s
   let _ ← to_slice_mut_back s1
   Result.ret ()
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index bd5921a8..ca9b48da 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -168,13 +168,13 @@ def betree.Leaf.split
   let (content0, content1) := p
   let p1 ← betree.List.hd (U64 × U64) content1
   let (pivot, _) := p1
-  let (id0, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt
-  let (id1, nic1) ← betree.NodeIdCounter.fresh_id nic
+  let (id0, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt
+  let (id1, node_id_cnt2) ← betree.NodeIdCounter.fresh_id node_id_cnt1
   let (st1, _) ← betree.store_leaf_node id0 content0 st
   let (st2, _) ← betree.store_leaf_node id1 content1 st1
   let n := betree.Node.Leaf { id := id0, size := params.split_size }
   let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
-  Result.ret (st2, (betree.Internal.mk self.id pivot n n1, nic1))
+  Result.ret (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
    Source: 'src/betree.rs', lines 789:4-792:34 -/
@@ -227,7 +227,7 @@ divergent def betree.Node.apply_upserts
   if b
   then
     do
-    let (msg, l) ← betree.List.pop_front (U64 × betree.Message) msgs
+    let (msg, msgs1) ← betree.List.pop_front (U64 × betree.Message) msgs
     let (_, m) := msg
     match m with
     | betree.Message.Insert _ => Result.fail .panic
@@ -235,14 +235,14 @@ divergent def betree.Node.apply_upserts
     | betree.Message.Upsert s =>
       do
       let v ← betree.upsert_update prev s
-      betree.Node.apply_upserts l (some v) key st
+      betree.Node.apply_upserts msgs1 (some v) key st
   else
     do
     let (st1, v) ← core.option.Option.unwrap U64 prev st
-    let l ←
+    let msgs1 ←
       betree.List.push_front (U64 × betree.Message) msgs (key,
         betree.Message.Insert v)
-    Result.ret (st1, (v, l))
+    Result.ret (st1, (v, msgs1))
 
 /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
    Source: 'src/betree.rs', lines 395:4-395:63 -/
@@ -280,12 +280,12 @@ divergent def betree.Node.lookup
       if k != key
       then
         do
-        let (st2, (o, i2)) ←
+        let (st2, (o, node1)) ←
           betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
             st1
         let _ ←
           lookup_first_message_for_key_back (betree.List.Cons (k, msg) l)
-        Result.ret (st2, (o, betree.Node.Internal i2))
+        Result.ret (st2, (o, betree.Node.Internal node1))
       else
         match msg with
         | betree.Message.Insert v =>
@@ -304,24 +304,24 @@ divergent def betree.Node.lookup
             n n1)))
         | betree.Message.Upsert ufs =>
           do
-          let (st2, (v, i2)) ←
+          let (st2, (v, node1)) ←
             betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1)
               key st1
-          let (st3, (v1, l1)) ←
+          let (st3, (v1, pending1)) ←
             betree.Node.apply_upserts (betree.List.Cons (k,
               betree.Message.Upsert ufs) l) v key st2
-          let ⟨ i3, i4, n2, n3 ⟩ := i2
-          let msgs1 ← lookup_first_message_for_key_back l1
-          let (st4, _) ← betree.store_internal_node i3 msgs1 st3
+          let ⟨ i2, i3, n2, n3 ⟩ := node1
+          let msgs1 ← lookup_first_message_for_key_back pending1
+          let (st4, _) ← betree.store_internal_node i2 msgs1 st3
           Result.ret (st4, (some v1, betree.Node.Internal (betree.Internal.mk
-            i3 i4 n2 n3)))
+            i2 i3 n2 n3)))
     | betree.List.Nil =>
       do
-      let (st2, (o, i2)) ←
+      let (st2, (o, node1)) ←
         betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
           st1
       let _ ← lookup_first_message_for_key_back betree.List.Nil
-      Result.ret (st2, (o, betree.Node.Internal i2))
+      Result.ret (st2, (o, betree.Node.Internal node1))
   | betree.Node.Leaf node =>
     do
     let (st1, bindings) ← betree.load_leaf_node node.id st
@@ -342,10 +342,10 @@ divergent def betree.Node.filter_messages_for_key
     if k = key
     then
       do
-      let (_, l1) ←
+      let (_, msgs1) ←
         betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m)
           l)
-      betree.Node.filter_messages_for_key key l1
+      betree.Node.filter_messages_for_key key msgs1
     else Result.ret (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ret betree.List.Nil
 
@@ -389,18 +389,18 @@ def betree.Node.apply_to_internal
     match new_msg with
     | betree.Message.Insert i =>
       do
-      let l ← betree.Node.filter_messages_for_key key msgs1
-      let l1 ←
-        betree.List.push_front (U64 × betree.Message) l (key,
+      let msgs2 ← betree.Node.filter_messages_for_key key msgs1
+      let msgs3 ←
+        betree.List.push_front (U64 × betree.Message) msgs2 (key,
           betree.Message.Insert i)
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | betree.Message.Delete =>
       do
-      let l ← betree.Node.filter_messages_for_key key msgs1
-      let l1 ←
-        betree.List.push_front (U64 × betree.Message) l (key,
+      let msgs2 ← betree.Node.filter_messages_for_key key msgs1
+      let msgs3 ←
+        betree.List.push_front (U64 × betree.Message) msgs2 (key,
           betree.Message.Delete)
-      lookup_first_message_for_key_back l1
+      lookup_first_message_for_key_back msgs3
     | betree.Message.Upsert s =>
       do
       let p ← betree.List.hd (U64 × betree.Message) msgs1
@@ -409,33 +409,33 @@ def betree.Node.apply_to_internal
       | betree.Message.Insert prev =>
         do
         let v ← betree.upsert_update (some prev) s
-        let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1
-        let l1 ←
-          betree.List.push_front (U64 × betree.Message) l (key,
+        let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1
+        let msgs3 ←
+          betree.List.push_front (U64 × betree.Message) msgs2 (key,
             betree.Message.Insert v)
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | betree.Message.Delete =>
         do
-        let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1
+        let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1
         let v ← betree.upsert_update none s
-        let l1 ←
-          betree.List.push_front (U64 × betree.Message) l (key,
+        let msgs3 ←
+          betree.List.push_front (U64 × betree.Message) msgs2 (key,
             betree.Message.Insert v)
-        lookup_first_message_for_key_back l1
+        lookup_first_message_for_key_back msgs3
       | betree.Message.Upsert _ =>
         do
         let (msgs2, lookup_first_message_after_key_back) ←
           betree.Node.lookup_first_message_after_key key msgs1
-        let l ←
+        let msgs3 ←
           betree.List.push_front (U64 × betree.Message) msgs2 (key,
             betree.Message.Upsert s)
-        let msgs3 ← lookup_first_message_after_key_back l
-        lookup_first_message_for_key_back msgs3
+        let msgs4 ← lookup_first_message_after_key_back msgs3
+        lookup_first_message_for_key_back msgs4
   else
     do
-    let l ←
+    let msgs2 ←
       betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg)
-    lookup_first_message_for_key_back l
+    lookup_first_message_for_key_back msgs2
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
    Source: 'src/betree.rs', lines 502:4-505:5 -/
@@ -448,8 +448,8 @@ divergent def betree.Node.apply_messages_to_internal
   | betree.List.Cons new_msg new_msgs_tl =>
     do
     let (i, m) := new_msg
-    let l ← betree.Node.apply_to_internal msgs i m
-    betree.Node.apply_messages_to_internal l new_msgs_tl
+    let msgs1 ← betree.Node.apply_to_internal msgs i m
+    betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
   | betree.List.Nil => Result.ret msgs
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
@@ -490,31 +490,31 @@ def betree.Node.apply_to_leaf
   if b
   then
     do
-    let (hd, l) ← betree.List.pop_front (U64 × U64) bindings1
+    let (hd, bindings2) ← betree.List.pop_front (U64 × U64) bindings1
     match new_msg with
     | betree.Message.Insert v =>
       do
-      let l1 ← betree.List.push_front (U64 × U64) l (key, v)
-      lookup_mut_in_bindings_back l1
-    | betree.Message.Delete => lookup_mut_in_bindings_back l
+      let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v)
+      lookup_mut_in_bindings_back bindings3
+    | betree.Message.Delete => lookup_mut_in_bindings_back bindings2
     | betree.Message.Upsert s =>
       do
       let (_, i) := hd
       let v ← betree.upsert_update (some i) s
-      let l1 ← betree.List.push_front (U64 × U64) l (key, v)
-      lookup_mut_in_bindings_back l1
+      let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v)
+      lookup_mut_in_bindings_back bindings3
   else
     match new_msg with
     | betree.Message.Insert v =>
       do
-      let l ← betree.List.push_front (U64 × U64) bindings1 (key, v)
-      lookup_mut_in_bindings_back l
+      let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v)
+      lookup_mut_in_bindings_back bindings2
     | betree.Message.Delete => lookup_mut_in_bindings_back bindings1
     | betree.Message.Upsert s =>
       do
       let v ← betree.upsert_update none s
-      let l ← betree.List.push_front (U64 × U64) bindings1 (key, v)
-      lookup_mut_in_bindings_back l
+      let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v)
+      lookup_mut_in_bindings_back bindings2
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]:
    Source: 'src/betree.rs', lines 444:4-447:5 -/
@@ -527,8 +527,8 @@ divergent def betree.Node.apply_messages_to_leaf
   | betree.List.Cons new_msg new_msgs_tl =>
     do
     let (i, m) := new_msg
-    let l ← betree.Node.apply_to_leaf bindings i m
-    betree.Node.apply_messages_to_leaf l new_msgs_tl
+    let bindings1 ← betree.Node.apply_to_leaf bindings i m
+    betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
   | betree.List.Nil => Result.ret bindings
 
 /- [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
@@ -583,40 +583,40 @@ divergent def betree.Node.apply_messages
     do
     let ⟨ i, i1, n, n1 ⟩ := node
     let (st1, content) ← betree.load_internal_node i st
-    let l ← betree.Node.apply_messages_to_internal content msgs
-    let num_msgs ← betree.List.len (U64 × betree.Message) l
+    let content1 ← betree.Node.apply_messages_to_internal content msgs
+    let num_msgs ← betree.List.len (U64 × betree.Message) content1
     if num_msgs >= params.min_flush_size
     then
       do
-      let (st2, (content1, p)) ←
+      let (st2, (content2, p)) ←
         betree.Internal.flush (betree.Internal.mk i i1 n n1) params node_id_cnt
-          l st1
+          content1 st1
       let (node1, node_id_cnt1) := p
       let ⟨ i2, i3, n2, n3 ⟩ := node1
-      let (st3, _) ← betree.store_internal_node i2 content1 st2
+      let (st3, _) ← betree.store_internal_node i2 content2 st2
       Result.ret (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
         node_id_cnt1))
     else
       do
-      let (st2, _) ← betree.store_internal_node i l st1
+      let (st2, _) ← betree.store_internal_node i content1 st1
       Result.ret (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
         node_id_cnt))
   | betree.Node.Leaf node =>
     do
     let (st1, content) ← betree.load_leaf_node node.id st
-    let l ← betree.Node.apply_messages_to_leaf content msgs
-    let len ← betree.List.len (U64 × U64) l
+    let content1 ← betree.Node.apply_messages_to_leaf content msgs
+    let len ← betree.List.len (U64 × U64) content1
     let i ← 2#u64 * params.split_size
     if len >= i
     then
       do
-      let (st2, (new_node, nic)) ←
-        betree.Leaf.split node l params node_id_cnt st1
+      let (st2, (new_node, node_id_cnt1)) ←
+        betree.Leaf.split node content1 params node_id_cnt st1
       let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2
-      Result.ret (st3, (betree.Node.Internal new_node, nic))
+      Result.ret (st3, (betree.Node.Internal new_node, node_id_cnt1))
     else
       do
-      let (st2, _) ← betree.store_leaf_node node.id l st1
+      let (st2, _) ← betree.store_leaf_node node.id content1 st1
       Result.ret (st2, (betree.Node.Leaf { node with size := len },
         node_id_cnt))
 
@@ -645,12 +645,12 @@ def betree.BeTree.new
   :=
   do
   let node_id_cnt ← betree.NodeIdCounter.new
-  let (id, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt
+  let (id, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt
   let (st1, _) ← betree.store_leaf_node id betree.List.Nil st
   Result.ret (st1,
     {
       params := { min_flush_size := min_flush_size, split_size := split_size },
-      node_id_cnt := nic,
+      node_id_cnt := node_id_cnt1,
       root := (betree.Node.Leaf { id := id, size := 0#u64 })
     })
 
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 09032820..4acc69c8 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -40,9 +40,9 @@ def incr (x : U32) : Result U32 :=
    Source: 'src/demo.rs', lines 25:0-25:17 -/
 def use_incr : Result Unit :=
   do
-  let i ← incr 0#u32
-  let i1 ← incr i
-  let _ ← incr i1
+  let x ← incr 0#u32
+  let x1 ← incr x
+  let _ ← incr x1
   Result.ret ()
 
 /- [demo::CList]
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index db15aacc..8b645037 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -38,9 +38,9 @@ def custom_swap
   Result (State × (T × (T → State → Result (State × (T × T)))))
   :=
   do
-  let (st1, (t, t1)) ← core.mem.swap T x y st
-  let back_'a := fun ret st2 => Result.ret (st2, (ret, t1))
-  Result.ret (st1, (t, back_'a))
+  let (st1, (x1, y1)) ← core.mem.swap T x y st
+  let back_'a := fun ret st2 => Result.ret (st2, (ret, y1))
+  Result.ret (st1, (x1, back_'a))
 
 /- [external::test_custom_swap]:
    Source: 'src/external.rs', lines 29:0-29:59 -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index d33b6571..1c95f7c9 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -20,9 +20,9 @@ divergent def HashMap.allocate_slots_loop
   if n > 0#usize
   then
     do
-    let v ← alloc.vec.Vec.push (List T) slots List.Nil
+    let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil
     let n1 ← n - 1#usize
-    HashMap.allocate_slots_loop T v n1
+    HashMap.allocate_slots_loop T slots1 n1
   else Result.ret slots
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
@@ -142,8 +142,8 @@ divergent def HashMap.move_elements_from_list_loop
   match ls with
   | List.Cons k v tl =>
     do
-    let hm ← HashMap.insert_no_resize T ntable k v
-    HashMap.move_elements_from_list_loop T hm tl
+    let ntable1 ← HashMap.insert_no_resize T ntable k v
+    HashMap.move_elements_from_list_loop T ntable1 tl
   | List.Nil => Result.ret ntable
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
@@ -167,12 +167,10 @@ divergent def HashMap.move_elements_loop
       alloc.vec.Vec.index_mut (List T) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i
     let (ls, l1) := core.mem.replace (List T) l List.Nil
-    let hm ← HashMap.move_elements_from_list T ntable ls
+    let ntable1 ← HashMap.move_elements_from_list T ntable ls
     let i2 ← i + 1#usize
     let slots1 ← index_mut_back l1
-    let back_'a ← HashMap.move_elements_loop T hm slots1 i2
-    let (hm1, v) := back_'a
-    Result.ret (hm1, v)
+    HashMap.move_elements_loop T ntable1 slots1 i2
   else Result.ret (ntable, slots)
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements]:
@@ -182,10 +180,7 @@ def HashMap.move_elements
   :
   Result ((HashMap T) × (alloc.vec.Vec (List T)))
   :=
-  do
-  let back_'a ← HashMap.move_elements_loop T ntable slots i
-  let (hm, v) := back_'a
-  Result.ret (hm, v)
+  HashMap.move_elements_loop T ntable slots i
 
 /- [hashmap::{hashmap::HashMap<T>}::try_resize]:
    Source: 'src/hashmap.rs', lines 140:4-140:28 -/
@@ -218,11 +213,11 @@ def HashMap.insert
   Result (HashMap T)
   :=
   do
-  let hm ← HashMap.insert_no_resize T self key value
-  let i ← HashMap.len T hm
-  if i > hm.max_load
-  then HashMap.try_resize T hm
-  else Result.ret hm
+  let self1 ← HashMap.insert_no_resize T self key value
+  let i ← HashMap.len T self1
+  if i > self1.max_load
+  then HashMap.try_resize T self1
+  else Result.ret self1
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
    Source: 'src/hashmap.rs', lines 206:4-219:5 -/
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 8a277700..6a6934b8 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -21,9 +21,9 @@ divergent def hashmap.HashMap.allocate_slots_loop
   if n > 0#usize
   then
     do
-    let v ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil
+    let slots1 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil
     let n1 ← n - 1#usize
-    hashmap.HashMap.allocate_slots_loop T v n1
+    hashmap.HashMap.allocate_slots_loop T slots1 n1
   else Result.ret slots
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]:
@@ -150,8 +150,8 @@ divergent def hashmap.HashMap.move_elements_from_list_loop
   match ls with
   | hashmap.List.Cons k v tl =>
     do
-    let hm ← hashmap.HashMap.insert_no_resize T ntable k v
-    hashmap.HashMap.move_elements_from_list_loop T hm tl
+    let ntable1 ← hashmap.HashMap.insert_no_resize T ntable k v
+    hashmap.HashMap.move_elements_from_list_loop T ntable1 tl
   | hashmap.List.Nil => Result.ret ntable
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]:
@@ -177,12 +177,10 @@ divergent def hashmap.HashMap.move_elements_loop
       alloc.vec.Vec.index_mut (hashmap.List T) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i
     let (ls, l1) := core.mem.replace (hashmap.List T) l hashmap.List.Nil
-    let hm ← hashmap.HashMap.move_elements_from_list T ntable ls
+    let ntable1 ← hashmap.HashMap.move_elements_from_list T ntable ls
     let i2 ← i + 1#usize
     let slots1 ← index_mut_back l1
-    let back_'a ← hashmap.HashMap.move_elements_loop T hm slots1 i2
-    let (hm1, v) := back_'a
-    Result.ret (hm1, v)
+    hashmap.HashMap.move_elements_loop T ntable1 slots1 i2
   else Result.ret (ntable, slots)
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]:
@@ -192,10 +190,7 @@ def hashmap.HashMap.move_elements
   (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
   Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T)))
   :=
-  do
-  let back_'a ← hashmap.HashMap.move_elements_loop T ntable slots i
-  let (hm, v) := back_'a
-  Result.ret (hm, v)
+  hashmap.HashMap.move_elements_loop T ntable slots i
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
    Source: 'src/hashmap.rs', lines 140:4-140:28 -/
@@ -229,11 +224,11 @@ def hashmap.HashMap.insert
   Result (hashmap.HashMap T)
   :=
   do
-  let hm ← hashmap.HashMap.insert_no_resize T self key value
-  let i ← hashmap.HashMap.len T hm
-  if i > hm.max_load
-  then hashmap.HashMap.try_resize T hm
-  else Result.ret hm
+  let self1 ← hashmap.HashMap.insert_no_resize T self key value
+  let i ← hashmap.HashMap.len T self1
+  if i > self1.max_load
+  then hashmap.HashMap.try_resize T self1
+  else Result.ret self1
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
    Source: 'src/hashmap.rs', lines 206:4-219:5 -/
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 3f075347..0f3d77c2 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -23,14 +23,14 @@ def sum (max : U32) : Result U32 :=
 /- [loops::sum_with_mut_borrows]: loop 0:
    Source: 'src/loops.rs', lines 19:0-31:1 -/
 divergent def sum_with_mut_borrows_loop
-  (max : U32) (mi : U32) (ms : U32) : Result U32 :=
-  if mi < max
+  (max : U32) (i : U32) (s : U32) : Result U32 :=
+  if i < max
   then
     do
-    let ms1 ← ms + mi
-    let mi1 ← mi + 1#u32
-    sum_with_mut_borrows_loop max mi1 ms1
-  else ms * 2#u32
+    let ms ← s + i
+    let mi ← i + 1#u32
+    sum_with_mut_borrows_loop max mi ms
+  else s * 2#u32
 
 /- [loops::sum_with_mut_borrows]:
    Source: 'src/loops.rs', lines 19:0-19:44 -/
@@ -187,13 +187,13 @@ def get_elem_mut
   Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize))))
   :=
   do
-  let (l, index_mut_back) ←
+  let (ls, index_mut_back) ←
     alloc.vec.Vec.index_mut (List Usize) Usize
       (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
-  let (i, back) ← get_elem_mut_loop x l
+  let (i, back) ← get_elem_mut_loop x ls
   let back1 := fun ret => do
-                          let l1 ← back ret
-                          index_mut_back l1
+                          let l ← back ret
+                          index_mut_back l
   Result.ret (i, back1)
 
 /- [loops::get_elem_shared]: loop 0:
@@ -211,10 +211,10 @@ divergent def get_elem_shared_loop
 def get_elem_shared
   (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-  let l ←
+  let ls ←
     alloc.vec.Vec.index (List Usize) Usize
       (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
-  get_elem_shared_loop x l
+  get_elem_shared_loop x ls
 
 /- [loops::id_mut]:
    Source: 'src/loops.rs', lines 145:0-145:50 -/
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 2112e282..5f9ec0f2 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -487,9 +487,7 @@ def id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
   :=
-  let back_'a := fun ret => let (t, t1) := ret
-                            Result.ret (t, t1)
-  Result.ret ((x, y), back_'a)
+  Result.ret ((x, y), Result.ret)
 
 /- [no_nested_borrows::id_mut_pair2]:
    Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 -/
@@ -498,9 +496,7 @@ def id_mut_pair2
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
   :=
   let (t, t1) := p
-  let back_'a := fun ret => let (t2, t3) := ret
-                            Result.ret (t2, t3)
-  Result.ret ((t, t1), back_'a)
+  Result.ret ((t, t1), Result.ret)
 
 /- [no_nested_borrows::id_mut_pair3]:
    Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 -/
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 4930a05c..924ff36c 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -14,8 +14,8 @@ def ref_incr (x : I32) : Result I32 :=
    Source: 'src/paper.rs', lines 8:0-8:18 -/
 def test_incr : Result Unit :=
   do
-  let i ← ref_incr 0#i32
-  if ¬ (i = 1#i32)
+  let x ← ref_incr 0#i32
+  if ¬ (x = 1#i32)
   then Result.fail .panic
   else Result.ret ()
 
-- 
cgit v1.2.3