Merge pull request #64 from AeneasVerif/son/merge_back

Merge the forward/backward functions

4 files changed, 404 insertions, 807 deletions

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index a5dd4230..cefab0f4 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -12,7 +12,7 @@ Require Import BetreeMain_FunsExternal.
 Include BetreeMain_FunsExternal.
 Module BetreeMain_Funs.
 
-(** [betree_main::betree::load_internal_node]: forward function
+(** [betree_main::betree::load_internal_node]:
     Source: 'src/betree.rs', lines 36:0-36:52 *)
 Definition betree_load_internal_node
   (id : u64) (st : state) :
@@ -21,70 +21,57 @@ Definition betree_load_internal_node
   betree_utils_load_internal_node id st
 .
 
-(** [betree_main::betree::store_internal_node]: forward function
+(** [betree_main::betree::store_internal_node]:
     Source: 'src/betree.rs', lines 41:0-41:60 *)
 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 (st0, _) := p in
-  Return (st0, tt)
+  let (st1, _) := p in
+  Return (st1, tt)
 .
 
-(** [betree_main::betree::load_leaf_node]: forward function
+(** [betree_main::betree::load_leaf_node]:
     Source: 'src/betree.rs', lines 46:0-46:44 *)
 Definition betree_load_leaf_node
   (id : u64) (st : state) : result (state * (betree_List_t (u64 * u64))) :=
   betree_utils_load_leaf_node id st
 .
 
-(** [betree_main::betree::store_leaf_node]: forward function
+(** [betree_main::betree::store_leaf_node]:
     Source: 'src/betree.rs', lines 51:0-51:52 *)
 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 (st0, _) := p in
-  Return (st0, tt)
+  let (st1, _) := p in
+  Return (st1, tt)
 .
 
-(** [betree_main::betree::fresh_node_id]: forward function
+(** [betree_main::betree::fresh_node_id]:
     Source: 'src/betree.rs', lines 55:0-55:48 *)
-Definition betree_fresh_node_id (counter : u64) : result u64 :=
-  _ <- u64_add counter 1%u64; Return counter
+Definition betree_fresh_node_id (counter : u64) : result (u64 * u64) :=
+  counter1 <- u64_add counter 1%u64; Return (counter, counter1)
 .
 
-(** [betree_main::betree::fresh_node_id]: backward function 0
-    Source: 'src/betree.rs', lines 55:0-55:48 *)
-Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
-  u64_add counter 1%u64
-.
-
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
     Source: 'src/betree.rs', lines 206:4-206:20 *)
 Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
   Return {| betree_NodeIdCounter_next_node_id := 0%u64 |}
 .
 
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
     Source: 'src/betree.rs', lines 210:4-210:36 *)
 Definition betree_NodeIdCounter_fresh_id
-  (self : betree_NodeIdCounter_t) : result u64 :=
-  _ <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
-  Return self.(betree_NodeIdCounter_next_node_id)
-.
-
-(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0
-    Source: 'src/betree.rs', lines 210:4-210:36 *)
-Definition betree_NodeIdCounter_fresh_id_back
-  (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t :=
+  (self : betree_NodeIdCounter_t) : result (u64 * betree_NodeIdCounter_t) :=
   i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
-  Return {| betree_NodeIdCounter_next_node_id := i |}
+  Return (self.(betree_NodeIdCounter_next_node_id),
+    {| betree_NodeIdCounter_next_node_id := i |})
 .
 
-(** [betree_main::betree::upsert_update]: forward function
+(** [betree_main::betree::upsert_update]:
     Source: 'src/betree.rs', lines 234:0-234:70 *)
 Definition betree_upsert_update
   (prev : option u64) (st : betree_UpsertFunState_t) : result u64 :=
@@ -92,109 +79,95 @@ Definition betree_upsert_update
   | None =>
     match st with
     | Betree_UpsertFunState_Add v => Return v
-    | Betree_UpsertFunState_Sub i => Return 0%u64
+    | Betree_UpsertFunState_Sub _ => Return 0%u64
     end
-  | Some prev0 =>
+  | Some prev1 =>
     match st with
     | Betree_UpsertFunState_Add v =>
-      margin <- u64_sub core_u64_max prev0;
-      if margin s>= v then u64_add prev0 v else Return core_u64_max
+      margin <- u64_sub core_u64_max prev1;
+      if margin s>= v then u64_add prev1 v else Return core_u64_max
     | Betree_UpsertFunState_Sub v =>
-      if prev0 s>= v then u64_sub prev0 v else Return 0%u64
+      if prev1 s>= v then u64_sub prev1 v else Return 0%u64
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]:
     Source: 'src/betree.rs', lines 276:4-276:24 *)
 Fixpoint betree_List_len
   (T : Type) (n : nat) (self : betree_List_t T) : result u64 :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match self with
-    | Betree_List_Cons t tl => i <- betree_List_len T n0 tl; u64_add 1%u64 i
+    | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i
     | Betree_List_Nil => Return 0%u64
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]:
     Source: 'src/betree.rs', lines 284:4-284:51 *)
 Fixpoint betree_List_split_at
-  (T : Type) (n : nat) (self : betree_List_t T) (n0 : u64) :
+  (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) :
   result ((betree_List_t T) * (betree_List_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n1 =>
-    if n0 s= 0%u64
+  | S n2 =>
+    if n1 s= 0%u64
     then Return (Betree_List_Nil, self)
     else
       match self with
       | Betree_List_Cons hd tl =>
-        i <- u64_sub n0 1%u64;
-        p <- betree_List_split_at T n1 tl i;
+        i <- u64_sub n1 1%u64;
+        p <- betree_List_split_at T n2 tl i;
         let (ls0, ls1) := p in
-        let l := ls0 in
-        Return (Betree_List_Cons hd l, ls1)
+        Return (Betree_List_Cons hd ls0, ls1)
       | Betree_List_Nil => Fail_ Failure
       end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]:
     Source: 'src/betree.rs', lines 299:4-299:34 *)
 Definition betree_List_push_front
   (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
-  let tl := core_mem_replace (betree_List_t T) self Betree_List_Nil in
-  let l := tl in
-  Return (Betree_List_Cons x l)
+  let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
+  Return (Betree_List_Cons x tl)
 .
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
     Source: 'src/betree.rs', lines 306:4-306:32 *)
 Definition betree_List_pop_front
-  (T : Type) (self : betree_List_t T) : result T :=
-  let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in
+  (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) :=
+  let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
   match ls with
-  | Betree_List_Cons x tl => Return x
+  | Betree_List_Cons x tl => Return (x, tl)
   | Betree_List_Nil => Fail_ Failure
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0
-    Source: 'src/betree.rs', lines 306:4-306:32 *)
-Definition betree_List_pop_front_back
-  (T : Type) (self : betree_List_t T) : result (betree_List_t T) :=
-  let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in
-  match ls with
-  | Betree_List_Cons x tl => Return tl
-  | Betree_List_Nil => Fail_ Failure
-  end
-.
-
-(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]:
     Source: 'src/betree.rs', lines 318:4-318:22 *)
 Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
   match self with
-  | Betree_List_Cons hd l => Return hd
+  | Betree_List_Cons hd _ => Return hd
   | Betree_List_Nil => Fail_ Failure
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
     Source: 'src/betree.rs', lines 327:4-327:44 *)
 Definition betree_ListTupleU64T_head_has_key
   (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
   match self with
-  | Betree_List_Cons hd l => let (i, _) := hd in Return (i s= key)
+  | Betree_List_Cons hd _ => let (i, _) := hd in Return (i s= key)
   | Betree_List_Nil => Return false
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
     Source: 'src/betree.rs', lines 339:4-339:73 *)
 Fixpoint betree_ListTupleU64T_partition_at_pivot
   (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
@@ -202,123 +175,85 @@ Fixpoint betree_ListTupleU64T_partition_at_pivot
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match self with
     | Betree_List_Cons hd tl =>
       let (i, t) := hd in
       if i s>= pivot
       then Return (Betree_List_Nil, Betree_List_Cons (i, t) tl)
       else (
-        p <- betree_ListTupleU64T_partition_at_pivot T n0 tl pivot;
+        p <- betree_ListTupleU64T_partition_at_pivot T n1 tl pivot;
         let (ls0, ls1) := p in
-        let l := ls0 in
-        Return (Betree_List_Cons (i, t) l, ls1))
+        Return (Betree_List_Cons (i, t) ls0, ls1))
     | Betree_List_Nil => Return (Betree_List_Nil, Betree_List_Nil)
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]:
     Source: 'src/betree.rs', lines 359:4-364:17 *)
 Definition betree_Leaf_split
   (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
   (st : state) :
-  result (state * betree_Internal_t)
+  result (state * (betree_Internal_t * betree_NodeIdCounter_t))
   :=
   p <-
     betree_List_split_at (u64 * u64) n content
       params.(betree_Params_split_size);
   let (content0, content1) := p in
-  p0 <- betree_List_hd (u64 * u64) content1;
-  let (pivot, _) := p0 in
-  id0 <- betree_NodeIdCounter_fresh_id node_id_cnt;
-  node_id_cnt0 <- betree_NodeIdCounter_fresh_id_back node_id_cnt;
-  id1 <- betree_NodeIdCounter_fresh_id node_id_cnt0;
-  p1 <- betree_store_leaf_node id0 content0 st;
-  let (st0, _) := p1 in
-  p2 <- betree_store_leaf_node id1 content1 st0;
-  let (st1, _) := p2 in
-  let n0 := Betree_Node_Leaf
+  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
+  p4 <- betree_store_leaf_node id0 content0 st;
+  let (st1, _) := p4 in
+  p5 <- betree_store_leaf_node id1 content1 st1;
+  let (st2, _) := p5 in
+  let n1 := Betree_Node_Leaf
     {|
       betree_Leaf_id := id0;
       betree_Leaf_size := params.(betree_Params_split_size)
     |} in
-  let n1 := Betree_Node_Leaf
+  let n2 := Betree_Node_Leaf
     {|
       betree_Leaf_id := id1;
       betree_Leaf_size := params.(betree_Params_split_size)
     |} in
-  Return (st1, mkbetree_Internal_t self.(betree_Leaf_id) pivot n0 n1)
+  Return (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, nic1))
 .
 
-(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2
-    Source: 'src/betree.rs', lines 359:4-364:17 *)
-Definition betree_Leaf_split_back
-  (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
-  (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
-  (st : state) :
-  result betree_NodeIdCounter_t
-  :=
-  p <-
-    betree_List_split_at (u64 * u64) n content
-      params.(betree_Params_split_size);
-  let (content0, content1) := p in
-  _ <- betree_List_hd (u64 * u64) content1;
-  id0 <- betree_NodeIdCounter_fresh_id node_id_cnt;
-  node_id_cnt0 <- betree_NodeIdCounter_fresh_id_back node_id_cnt;
-  id1 <- betree_NodeIdCounter_fresh_id node_id_cnt0;
-  p0 <- betree_store_leaf_node id0 content0 st;
-  let (st0, _) := p0 in
-  _ <- betree_store_leaf_node id1 content1 st0;
-  betree_NodeIdCounter_fresh_id_back node_id_cnt0
-.
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
     Source: 'src/betree.rs', lines 789:4-792:34 *)
 Fixpoint betree_Node_lookup_first_message_for_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
-  result (betree_List_t (u64 * betree_Message_t))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match msgs with
-    | Betree_List_Cons x next_msgs =>
-      let (i, m) := x in
-      if i s>= key
-      then Return (Betree_List_Cons (i, m) next_msgs)
-      else betree_Node_lookup_first_message_for_key n0 key next_msgs
-    | Betree_List_Nil => Return Betree_List_Nil
-    end
-  end
-.
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0
-    Source: 'src/betree.rs', lines 789:4-792:34 *)
-Fixpoint betree_Node_lookup_first_message_for_key_back
-  (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t))
-  (ret : betree_List_t (u64 * betree_Message_t)) :
-  result (betree_List_t (u64 * betree_Message_t))
+  result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
+    betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match msgs with
     | Betree_List_Cons x next_msgs =>
       let (i, m) := x in
       if i s>= key
-      then Return ret
+      then Return (Betree_List_Cons (i, m) next_msgs, Return)
       else (
-        next_msgs0 <-
-          betree_Node_lookup_first_message_for_key_back n0 key next_msgs ret;
-        Return (Betree_List_Cons (i, m) next_msgs0))
-    | Betree_List_Nil => Return ret
+        p <- betree_Node_lookup_first_message_for_key n1 key next_msgs;
+        let (l, lookup_first_message_for_key_back) := p in
+        let back_'a :=
+          fun (ret : betree_List_t (u64 * betree_Message_t)) =>
+            next_msgs1 <- lookup_first_message_for_key_back ret;
+            Return (Betree_List_Cons (i, m) next_msgs1) in
+        Return (l, back_'a))
+    | Betree_List_Nil => Return (Betree_List_Nil, Return)
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
     Source: 'src/betree.rs', lines 636:4-636:80 *)
 Fixpoint betree_Node_lookup_in_bindings
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
@@ -326,263 +261,146 @@ Fixpoint betree_Node_lookup_in_bindings
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match bindings with
     | Betree_List_Cons hd tl =>
-      let (i, i0) := hd in
+      let (i, i1) := hd in
       if i s= key
-      then Return (Some i0)
+      then Return (Some i1)
       else
         if i s> key
         then Return None
-        else betree_Node_lookup_in_bindings n0 key tl
+        else betree_Node_lookup_in_bindings n1 key tl
     | Betree_List_Nil => Return None
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]:
     Source: 'src/betree.rs', lines 819:4-819:90 *)
 Fixpoint betree_Node_apply_upserts
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
-  result (state * u64)
+  result (state * (u64 * (betree_List_t (u64 * betree_Message_t))))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key;
     if b
     then (
-      msg <- betree_List_pop_front (u64 * betree_Message_t) msgs;
+      p <- betree_List_pop_front (u64 * betree_Message_t) msgs;
+      let (msg, l) := p in
       let (_, m) := msg in
       match m with
-      | Betree_Message_Insert i => Fail_ Failure
+      | Betree_Message_Insert _ => Fail_ Failure
       | Betree_Message_Delete => Fail_ Failure
       | Betree_Message_Upsert s =>
         v <- betree_upsert_update prev s;
-        msgs0 <- betree_List_pop_front_back (u64 * betree_Message_t) msgs;
-        betree_Node_apply_upserts n0 msgs0 (Some v) key st
+        betree_Node_apply_upserts n1 l (Some v) key st
       end)
     else (
       p <- core_option_Option_unwrap u64 prev st;
-      let (st0, v) := p in
-      _ <-
+      let (st1, v) := p in
+      l <-
         betree_List_push_front (u64 * betree_Message_t) msgs (key,
           Betree_Message_Insert v);
-      Return (st0, v))
-  end
-.
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0
-    Source: 'src/betree.rs', lines 819:4-819:90 *)
-Fixpoint betree_Node_apply_upserts_back
-  (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
-  (key : u64) (st : state) :
-  result (betree_List_t (u64 * betree_Message_t))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key;
-    if b
-    then (
-      msg <- betree_List_pop_front (u64 * betree_Message_t) msgs;
-      let (_, m) := msg in
-      match m with
-      | Betree_Message_Insert i => Fail_ Failure
-      | Betree_Message_Delete => Fail_ Failure
-      | Betree_Message_Upsert s =>
-        v <- betree_upsert_update prev s;
-        msgs0 <- betree_List_pop_front_back (u64 * betree_Message_t) msgs;
-        betree_Node_apply_upserts_back n0 msgs0 (Some v) key st
-      end)
-    else (
-      p <- core_option_Option_unwrap u64 prev st;
-      let (_, v) := p in
-      betree_List_push_front (u64 * betree_Message_t) msgs (key,
-        Betree_Message_Insert v))
+      Return (st1, (v, l)))
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
     Source: 'src/betree.rs', lines 395:4-395:63 *)
 Fixpoint betree_Internal_lookup_in_children
   (n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
-  result (state * (option u64))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    if key s< self.(betree_Internal_pivot)
-    then betree_Node_lookup n0 self.(betree_Internal_left) key st
-    else betree_Node_lookup n0 self.(betree_Internal_right) key st
-  end
-
-(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0
-    Source: 'src/betree.rs', lines 395:4-395:63 *)
-with betree_Internal_lookup_in_children_back
-  (n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
-  result betree_Internal_t
+  result (state * ((option u64) * betree_Internal_t))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     if key s< self.(betree_Internal_pivot)
     then (
-      n1 <- betree_Node_lookup_back n0 self.(betree_Internal_left) key st;
-      Return (mkbetree_Internal_t self.(betree_Internal_id)
-        self.(betree_Internal_pivot) n1 self.(betree_Internal_right)))
+      p <- betree_Node_lookup n1 self.(betree_Internal_left) key st;
+      let (st1, p1) := p in
+      let (o, n2) := p1 in
+      Return (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
+        self.(betree_Internal_pivot) n2 self.(betree_Internal_right))))
     else (
-      n1 <- betree_Node_lookup_back n0 self.(betree_Internal_right) key st;
-      Return (mkbetree_Internal_t self.(betree_Internal_id)
-        self.(betree_Internal_pivot) self.(betree_Internal_left) n1))
+      p <- betree_Node_lookup n1 self.(betree_Internal_right) key st;
+      let (st1, p1) := p in
+      let (o, n2) := p1 in
+      Return (st1, (o, mkbetree_Internal_t self.(betree_Internal_id)
+        self.(betree_Internal_pivot) self.(betree_Internal_left) n2)))
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
     Source: 'src/betree.rs', lines 709:4-709:58 *)
 with betree_Node_lookup
   (n : nat) (self : betree_Node_t) (key : u64) (st : state) :
-  result (state * (option u64))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match self with
-    | Betree_Node_Internal node =>
-      p <- betree_load_internal_node node.(betree_Internal_id) st;
-      let (st0, msgs) := p in
-      pending <- betree_Node_lookup_first_message_for_key n0 key msgs;
-      match pending with
-      | Betree_List_Cons p0 l =>
-        let (k, msg) := p0 in
-        if k s<> key
-        then (
-          p1 <- betree_Internal_lookup_in_children n0 node key st0;
-          let (st1, o) := p1 in
-          _ <-
-            betree_Node_lookup_first_message_for_key_back n0 key msgs
-              (Betree_List_Cons (k, msg) l);
-          Return (st1, o))
-        else
-          match msg with
-          | Betree_Message_Insert v =>
-            _ <-
-              betree_Node_lookup_first_message_for_key_back n0 key msgs
-                (Betree_List_Cons (k, Betree_Message_Insert v) l);
-            Return (st0, Some v)
-          | Betree_Message_Delete =>
-            _ <-
-              betree_Node_lookup_first_message_for_key_back n0 key msgs
-                (Betree_List_Cons (k, Betree_Message_Delete) l);
-            Return (st0, None)
-          | Betree_Message_Upsert ufs =>
-            p1 <- betree_Internal_lookup_in_children n0 node key st0;
-            let (st1, v) := p1 in
-            p2 <-
-              betree_Node_apply_upserts n0 (Betree_List_Cons (k,
-                Betree_Message_Upsert ufs) l) v key st1;
-            let (st2, v0) := p2 in
-            node0 <- betree_Internal_lookup_in_children_back n0 node key st0;
-            pending0 <-
-              betree_Node_apply_upserts_back n0 (Betree_List_Cons (k,
-                Betree_Message_Upsert ufs) l) v key st1;
-            msgs0 <-
-              betree_Node_lookup_first_message_for_key_back n0 key msgs
-                pending0;
-            p3 <-
-              betree_store_internal_node node0.(betree_Internal_id) msgs0 st2;
-            let (st3, _) := p3 in
-            Return (st3, Some v0)
-          end
-      | Betree_List_Nil =>
-        p0 <- betree_Internal_lookup_in_children n0 node key st0;
-        let (st1, o) := p0 in
-        _ <-
-          betree_Node_lookup_first_message_for_key_back n0 key msgs
-            Betree_List_Nil;
-        Return (st1, o)
-      end
-    | Betree_Node_Leaf node =>
-      p <- betree_load_leaf_node node.(betree_Leaf_id) st;
-      let (st0, bindings) := p in
-      o <- betree_Node_lookup_in_bindings n0 key bindings;
-      Return (st0, o)
-    end
-  end
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0
-    Source: 'src/betree.rs', lines 709:4-709:58 *)
-with betree_Node_lookup_back
-  (n : nat) (self : betree_Node_t) (key : u64) (st : state) :
-  result betree_Node_t
+  result (state * ((option u64) * betree_Node_t))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match self with
     | Betree_Node_Internal node =>
       p <- betree_load_internal_node node.(betree_Internal_id) st;
-      let (st0, msgs) := p in
-      pending <- betree_Node_lookup_first_message_for_key n0 key msgs;
+      let (st1, msgs) := p in
+      p1 <- betree_Node_lookup_first_message_for_key n1 key msgs;
+      let (pending, lookup_first_message_for_key_back) := p1 in
       match pending with
-      | Betree_List_Cons p0 l =>
-        let (k, msg) := p0 in
+      | Betree_List_Cons p2 l =>
+        let (k, msg) := p2 in
         if k s<> key
         then (
-          _ <-
-            betree_Node_lookup_first_message_for_key_back n0 key msgs
-              (Betree_List_Cons (k, msg) l);
-          node0 <- betree_Internal_lookup_in_children_back n0 node key st0;
-          Return (Betree_Node_Internal node0))
+          p3 <- betree_Internal_lookup_in_children n1 node key st1;
+          let (st2, p4) := p3 in
+          let (o, i) := p4 in
+          _ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l);
+          Return (st2, (o, Betree_Node_Internal i)))
         else
           match msg with
           | Betree_Message_Insert v =>
             _ <-
-              betree_Node_lookup_first_message_for_key_back n0 key msgs
-                (Betree_List_Cons (k, Betree_Message_Insert v) l);
-            Return (Betree_Node_Internal node)
+              lookup_first_message_for_key_back (Betree_List_Cons (k,
+                Betree_Message_Insert v) l);
+            Return (st1, (Some v, Betree_Node_Internal node))
           | Betree_Message_Delete =>
             _ <-
-              betree_Node_lookup_first_message_for_key_back n0 key msgs
-                (Betree_List_Cons (k, Betree_Message_Delete) l);
-            Return (Betree_Node_Internal node)
+              lookup_first_message_for_key_back (Betree_List_Cons (k,
+                Betree_Message_Delete) l);
+            Return (st1, (None, Betree_Node_Internal node))
           | Betree_Message_Upsert ufs =>
-            p1 <- betree_Internal_lookup_in_children n0 node key st0;
-            let (st1, v) := p1 in
-            p2 <-
-              betree_Node_apply_upserts n0 (Betree_List_Cons (k,
-                Betree_Message_Upsert ufs) l) v key st1;
-            let (st2, _) := p2 in
-            node0 <- betree_Internal_lookup_in_children_back n0 node key st0;
-            pending0 <-
-              betree_Node_apply_upserts_back n0 (Betree_List_Cons (k,
-                Betree_Message_Upsert ufs) l) v key st1;
-            msgs0 <-
-              betree_Node_lookup_first_message_for_key_back n0 key msgs
-                pending0;
-            _ <-
-              betree_store_internal_node node0.(betree_Internal_id) msgs0 st2;
-            Return (Betree_Node_Internal node0)
+            p3 <- betree_Internal_lookup_in_children n1 node key st1;
+            let (st2, p4) := p3 in
+            let (v, i) := 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 (st4, _) := p7 in
+            Return (st4, (Some v1, Betree_Node_Internal i))
           end
       | Betree_List_Nil =>
-        _ <-
-          betree_Node_lookup_first_message_for_key_back n0 key msgs
-            Betree_List_Nil;
-        node0 <- betree_Internal_lookup_in_children_back n0 node key st0;
-        Return (Betree_Node_Internal node0)
+        p2 <- betree_Internal_lookup_in_children n1 node key st1;
+        let (st2, p3) := p2 in
+        let (o, i) := p3 in
+        _ <- lookup_first_message_for_key_back Betree_List_Nil;
+        Return (st2, (o, Betree_Node_Internal i))
       end
     | Betree_Node_Leaf node =>
       p <- betree_load_leaf_node node.(betree_Leaf_id) st;
-      let (_, bindings) := p in
-      _ <- betree_Node_lookup_in_bindings n0 key bindings;
-      Return (Betree_Node_Leaf node)
+      let (st1, bindings) := p in
+      o <- betree_Node_lookup_in_bindings n1 key bindings;
+      Return (st1, (o, Betree_Node_Leaf node))
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]:
     Source: 'src/betree.rs', lines 674:4-674:77 *)
 Fixpoint betree_Node_filter_messages_for_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
@@ -590,127 +408,112 @@ Fixpoint betree_Node_filter_messages_for_key
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match msgs with
     | Betree_List_Cons p l =>
       let (k, m) := p in
       if k s= key
       then (
-        msgs0 <-
-          betree_List_pop_front_back (u64 * betree_Message_t) (Betree_List_Cons
-            (k, m) l);
-        betree_Node_filter_messages_for_key n0 key msgs0)
+        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)
       else Return (Betree_List_Cons (k, m) l)
     | Betree_List_Nil => Return Betree_List_Nil
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]:
     Source: 'src/betree.rs', lines 689:4-692:34 *)
 Fixpoint betree_Node_lookup_first_message_after_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
-  result (betree_List_t (u64 * betree_Message_t))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match msgs with
-    | Betree_List_Cons p next_msgs =>
-      let (k, m) := p in
-      if k s= key
-      then betree_Node_lookup_first_message_after_key n0 key next_msgs
-      else Return (Betree_List_Cons (k, m) next_msgs)
-    | Betree_List_Nil => Return Betree_List_Nil
-    end
-  end
-.
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0
-    Source: 'src/betree.rs', lines 689:4-692:34 *)
-Fixpoint betree_Node_lookup_first_message_after_key_back
-  (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t))
-  (ret : betree_List_t (u64 * betree_Message_t)) :
-  result (betree_List_t (u64 * betree_Message_t))
+  result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
+    betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match msgs with
     | Betree_List_Cons p next_msgs =>
       let (k, m) := p in
       if k s= key
       then (
-        next_msgs0 <-
-          betree_Node_lookup_first_message_after_key_back n0 key next_msgs ret;
-        Return (Betree_List_Cons (k, m) next_msgs0))
-      else Return ret
-    | Betree_List_Nil => Return ret
+        p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs;
+        let (l, lookup_first_message_after_key_back) := p1 in
+        let back_'a :=
+          fun (ret : betree_List_t (u64 * betree_Message_t)) =>
+            next_msgs1 <- lookup_first_message_after_key_back ret;
+            Return (Betree_List_Cons (k, m) next_msgs1) in
+        Return (l, back_'a))
+      else Return (Betree_List_Cons (k, m) next_msgs, Return)
+    | Betree_List_Nil => Return (Betree_List_Nil, Return)
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]:
     Source: 'src/betree.rs', lines 521:4-521:89 *)
 Definition betree_Node_apply_to_internal
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64)
   (new_msg : betree_Message_t) :
   result (betree_List_t (u64 * betree_Message_t))
   :=
-  msgs0 <- betree_Node_lookup_first_message_for_key n key msgs;
-  b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs0 key;
+  p <- betree_Node_lookup_first_message_for_key n key msgs;
+  let (msgs1, lookup_first_message_for_key_back) := p in
+  b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs1 key;
   if b
   then
     match new_msg with
     | Betree_Message_Insert i =>
-      msgs1 <- betree_Node_filter_messages_for_key n key msgs0;
-      msgs2 <-
-        betree_List_push_front (u64 * betree_Message_t) msgs1 (key,
+      l <- betree_Node_filter_messages_for_key n key msgs1;
+      l1 <-
+        betree_List_push_front (u64 * betree_Message_t) l (key,
           Betree_Message_Insert i);
-      betree_Node_lookup_first_message_for_key_back n key msgs msgs2
+      lookup_first_message_for_key_back l1
     | Betree_Message_Delete =>
-      msgs1 <- betree_Node_filter_messages_for_key n key msgs0;
-      msgs2 <-
-        betree_List_push_front (u64 * betree_Message_t) msgs1 (key,
+      l <- betree_Node_filter_messages_for_key n key msgs1;
+      l1 <-
+        betree_List_push_front (u64 * betree_Message_t) l (key,
           Betree_Message_Delete);
-      betree_Node_lookup_first_message_for_key_back n key msgs msgs2
+      lookup_first_message_for_key_back l1
     | Betree_Message_Upsert s =>
-      p <- betree_List_hd (u64 * betree_Message_t) msgs0;
-      let (_, m) := p in
+      p1 <- betree_List_hd (u64 * betree_Message_t) msgs1;
+      let (_, m) := p1 in
       match m with
       | Betree_Message_Insert prev =>
         v <- betree_upsert_update (Some prev) s;
-        msgs1 <- betree_List_pop_front_back (u64 * betree_Message_t) msgs0;
-        msgs2 <-
-          betree_List_push_front (u64 * betree_Message_t) msgs1 (key,
+        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,
             Betree_Message_Insert v);
-        betree_Node_lookup_first_message_for_key_back n key msgs msgs2
+        lookup_first_message_for_key_back l1
       | Betree_Message_Delete =>
+        p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1;
+        let (_, l) := p2 in
         v <- betree_upsert_update None s;
-        msgs1 <- betree_List_pop_front_back (u64 * betree_Message_t) msgs0;
-        msgs2 <-
-          betree_List_push_front (u64 * betree_Message_t) msgs1 (key,
+        l1 <-
+          betree_List_push_front (u64 * betree_Message_t) l (key,
             Betree_Message_Insert v);
-        betree_Node_lookup_first_message_for_key_back n key msgs msgs2
-      | Betree_Message_Upsert ufs =>
-        msgs1 <- betree_Node_lookup_first_message_after_key n key msgs0;
-        msgs2 <-
-          betree_List_push_front (u64 * betree_Message_t) msgs1 (key,
+        lookup_first_message_for_key_back l1
+      | 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 <-
+          betree_List_push_front (u64 * betree_Message_t) msgs2 (key,
             Betree_Message_Upsert s);
-        msgs3 <-
-          betree_Node_lookup_first_message_after_key_back n key msgs0 msgs2;
-        betree_Node_lookup_first_message_for_key_back n key msgs msgs3
+        msgs3 <- lookup_first_message_after_key_back l;
+        lookup_first_message_for_key_back msgs3
       end
     end
   else (
-    msgs1 <-
-      betree_List_push_front (u64 * betree_Message_t) msgs0 (key, new_msg);
-    betree_Node_lookup_first_message_for_key_back n key msgs msgs1)
+    l <- betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg);
+    lookup_first_message_for_key_back l)
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
     Source: 'src/betree.rs', lines 502:4-505:5 *)
 Fixpoint betree_Node_apply_messages_to_internal
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t))
@@ -719,104 +522,84 @@ Fixpoint betree_Node_apply_messages_to_internal
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match new_msgs with
     | Betree_List_Cons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
-      msgs0 <- betree_Node_apply_to_internal n0 msgs i m;
-      betree_Node_apply_messages_to_internal n0 msgs0 new_msgs_tl
+      l <- betree_Node_apply_to_internal n1 msgs i m;
+      betree_Node_apply_messages_to_internal n1 l new_msgs_tl
     | Betree_List_Nil => Return msgs
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
     Source: 'src/betree.rs', lines 653:4-656:32 *)
 Fixpoint betree_Node_lookup_mut_in_bindings
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
-  result (betree_List_t (u64 * u64))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match bindings with
-    | Betree_List_Cons hd tl =>
-      let (i, i0) := hd in
-      if i s>= key
-      then Return (Betree_List_Cons (i, i0) tl)
-      else betree_Node_lookup_mut_in_bindings n0 key tl
-    | Betree_List_Nil => Return Betree_List_Nil
-    end
-  end
-.
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0
-    Source: 'src/betree.rs', lines 653:4-656:32 *)
-Fixpoint betree_Node_lookup_mut_in_bindings_back
-  (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64))
-  (ret : betree_List_t (u64 * u64)) :
-  result (betree_List_t (u64 * u64))
+  result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result
+    (betree_List_t (u64 * u64))))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match bindings with
     | Betree_List_Cons hd tl =>
-      let (i, i0) := hd in
+      let (i, i1) := hd in
       if i s>= key
-      then Return ret
+      then Return (Betree_List_Cons (i, i1) tl, Return)
       else (
-        tl0 <- betree_Node_lookup_mut_in_bindings_back n0 key tl ret;
-        Return (Betree_List_Cons (i, i0) tl0))
-    | Betree_List_Nil => Return ret
+        p <- betree_Node_lookup_mut_in_bindings n1 key tl;
+        let (l, lookup_mut_in_bindings_back) := p in
+        let back_'a :=
+          fun (ret : betree_List_t (u64 * u64)) =>
+            tl1 <- lookup_mut_in_bindings_back ret;
+            Return (Betree_List_Cons (i, i1) tl1) in
+        Return (l, back_'a))
+    | Betree_List_Nil => Return (Betree_List_Nil, Return)
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
     Source: 'src/betree.rs', lines 460:4-460:87 *)
 Definition betree_Node_apply_to_leaf
   (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64)
   (new_msg : betree_Message_t) :
   result (betree_List_t (u64 * u64))
   :=
-  bindings0 <- betree_Node_lookup_mut_in_bindings n key bindings;
-  b <- betree_ListTupleU64T_head_has_key u64 bindings0 key;
+  p <- betree_Node_lookup_mut_in_bindings n key bindings;
+  let (bindings1, lookup_mut_in_bindings_back) := p in
+  b <- betree_ListTupleU64T_head_has_key u64 bindings1 key;
   if b
   then (
-    hd <- betree_List_pop_front (u64 * u64) bindings0;
+    p1 <- betree_List_pop_front (u64 * u64) bindings1;
+    let (hd, l) := p1 in
     match new_msg with
     | Betree_Message_Insert v =>
-      bindings1 <- betree_List_pop_front_back (u64 * u64) bindings0;
-      bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v);
-      betree_Node_lookup_mut_in_bindings_back n key bindings bindings2
-    | Betree_Message_Delete =>
-      bindings1 <- betree_List_pop_front_back (u64 * u64) bindings0;
-      betree_Node_lookup_mut_in_bindings_back n key bindings bindings1
+      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
     | Betree_Message_Upsert s =>
       let (_, i) := hd in
       v <- betree_upsert_update (Some i) s;
-      bindings1 <- betree_List_pop_front_back (u64 * u64) bindings0;
-      bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v);
-      betree_Node_lookup_mut_in_bindings_back n key bindings bindings2
+      l1 <- betree_List_push_front (u64 * u64) l (key, v);
+      lookup_mut_in_bindings_back l1
     end)
   else
     match new_msg with
     | Betree_Message_Insert v =>
-      bindings1 <- betree_List_push_front (u64 * u64) bindings0 (key, v);
-      betree_Node_lookup_mut_in_bindings_back n key bindings bindings1
-    | Betree_Message_Delete =>
-      betree_Node_lookup_mut_in_bindings_back n key bindings bindings0
+      l <- betree_List_push_front (u64 * u64) bindings1 (key, v);
+      lookup_mut_in_bindings_back l
+    | Betree_Message_Delete => lookup_mut_in_bindings_back bindings1
     | Betree_Message_Upsert s =>
       v <- betree_upsert_update None s;
-      bindings1 <- betree_List_push_front (u64 * u64) bindings0 (key, v);
-      betree_Node_lookup_mut_in_bindings_back n key bindings bindings1
+      l <- betree_List_push_front (u64 * u64) bindings1 (key, v);
+      lookup_mut_in_bindings_back l
     end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]:
     Source: 'src/betree.rs', lines 444:4-447:5 *)
 Fixpoint betree_Node_apply_messages_to_leaf
   (n : nat) (bindings : betree_List_t (u64 * u64))
@@ -825,404 +608,229 @@ Fixpoint betree_Node_apply_messages_to_leaf
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match new_msgs with
     | Betree_List_Cons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
-      bindings0 <- betree_Node_apply_to_leaf n0 bindings i m;
-      betree_Node_apply_messages_to_leaf n0 bindings0 new_msgs_tl
+      l <- betree_Node_apply_to_leaf n1 bindings i m;
+      betree_Node_apply_messages_to_leaf n1 l new_msgs_tl
     | Betree_List_Nil => Return bindings
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
     Source: 'src/betree.rs', lines 410:4-415:26 *)
 Fixpoint betree_Internal_flush
   (n : nat) (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
   (content : betree_List_t (u64 * betree_Message_t)) (st : state) :
-  result (state * (betree_List_t (u64 * betree_Message_t)))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <-
-      betree_ListTupleU64T_partition_at_pivot betree_Message_t n0 content
-        self.(betree_Internal_pivot);
-    let (msgs_left, msgs_right) := p in
-    len_left <- betree_List_len (u64 * betree_Message_t) n0 msgs_left;
-    if len_left s>= params.(betree_Params_min_flush_size)
-    then (
-      p0 <-
-        betree_Node_apply_messages n0 self.(betree_Internal_left) params
-          node_id_cnt msgs_left st;
-      let (st0, _) := p0 in
-      p1 <-
-        betree_Node_apply_messages_back n0 self.(betree_Internal_left) params
-          node_id_cnt msgs_left st;
-      let (_, node_id_cnt0) := p1 in
-      len_right <- betree_List_len (u64 * betree_Message_t) n0 msgs_right;
-      if len_right s>= params.(betree_Params_min_flush_size)
-      then (
-        p2 <-
-          betree_Node_apply_messages n0 self.(betree_Internal_right) params
-            node_id_cnt0 msgs_right st0;
-        let (st1, _) := p2 in
-        _ <-
-          betree_Node_apply_messages_back n0 self.(betree_Internal_right)
-            params node_id_cnt0 msgs_right st0;
-        Return (st1, Betree_List_Nil))
-      else Return (st0, msgs_right))
-    else (
-      p0 <-
-        betree_Node_apply_messages n0 self.(betree_Internal_right) params
-          node_id_cnt msgs_right st;
-      let (st0, _) := p0 in
-      _ <-
-        betree_Node_apply_messages_back n0 self.(betree_Internal_right) params
-          node_id_cnt msgs_right st;
-      Return (st0, msgs_left))
-  end
-
-(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0
-    Source: 'src/betree.rs', lines 410:4-415:26 *)
-with betree_Internal_flush_back
-  (n : nat) (self : betree_Internal_t) (params : betree_Params_t)
-  (node_id_cnt : betree_NodeIdCounter_t)
-  (content : betree_List_t (u64 * betree_Message_t)) (st : state) :
-  result (betree_Internal_t * betree_NodeIdCounter_t)
+  result (state * ((betree_List_t (u64 * betree_Message_t)) *
+    (betree_Internal_t * betree_NodeIdCounter_t)))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     p <-
-      betree_ListTupleU64T_partition_at_pivot betree_Message_t n0 content
+      betree_ListTupleU64T_partition_at_pivot betree_Message_t n1 content
         self.(betree_Internal_pivot);
     let (msgs_left, msgs_right) := p in
-    len_left <- betree_List_len (u64 * betree_Message_t) n0 msgs_left;
+    len_left <- betree_List_len (u64 * betree_Message_t) n1 msgs_left;
     if len_left s>= params.(betree_Params_min_flush_size)
     then (
-      p0 <-
-        betree_Node_apply_messages n0 self.(betree_Internal_left) params
-          node_id_cnt msgs_left st;
-      let (st0, _) := p0 in
       p1 <-
-        betree_Node_apply_messages_back n0 self.(betree_Internal_left) params
+        betree_Node_apply_messages n1 self.(betree_Internal_left) params
           node_id_cnt msgs_left st;
-      let (n1, node_id_cnt0) := p1 in
-      len_right <- betree_List_len (u64 * betree_Message_t) n0 msgs_right;
+      let (st1, p2) := p1 in
+      let (n2, node_id_cnt1) := p2 in
+      len_right <- betree_List_len (u64 * betree_Message_t) n1 msgs_right;
       if len_right s>= params.(betree_Params_min_flush_size)
       then (
-        p2 <-
-          betree_Node_apply_messages_back n0 self.(betree_Internal_right)
-            params node_id_cnt0 msgs_right st0;
-        let (n2, node_id_cnt1) := p2 in
-        Return (mkbetree_Internal_t self.(betree_Internal_id)
-          self.(betree_Internal_pivot) n1 n2, node_id_cnt1))
+        p3 <-
+          betree_Node_apply_messages n1 self.(betree_Internal_right) params
+            node_id_cnt1 msgs_right st1;
+        let (st2, p4) := p3 in
+        let (n3, node_id_cnt2) := p4 in
+        Return (st2, (Betree_List_Nil, (mkbetree_Internal_t
+          self.(betree_Internal_id) self.(betree_Internal_pivot) n2 n3,
+          node_id_cnt2))))
       else
-        Return (mkbetree_Internal_t self.(betree_Internal_id)
-          self.(betree_Internal_pivot) n1 self.(betree_Internal_right),
-          node_id_cnt0))
+        Return (st1, (msgs_right, (mkbetree_Internal_t
+          self.(betree_Internal_id) self.(betree_Internal_pivot) n2
+          self.(betree_Internal_right), node_id_cnt1))))
     else (
-      p0 <-
-        betree_Node_apply_messages_back n0 self.(betree_Internal_right) params
+      p1 <-
+        betree_Node_apply_messages n1 self.(betree_Internal_right) params
           node_id_cnt msgs_right st;
-      let (n1, node_id_cnt0) := p0 in
-      Return (mkbetree_Internal_t self.(betree_Internal_id)
-        self.(betree_Internal_pivot) self.(betree_Internal_left) n1,
-        node_id_cnt0))
+      let (st1, p2) := p1 in
+      let (n2, node_id_cnt1) := p2 in
+      Return (st1, (msgs_left, (mkbetree_Internal_t self.(betree_Internal_id)
+        self.(betree_Internal_pivot) self.(betree_Internal_left) n2,
+        node_id_cnt1))))
   end
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
     Source: 'src/betree.rs', lines 588:4-593:5 *)
 with betree_Node_apply_messages
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
   (msgs : betree_List_t (u64 * betree_Message_t)) (st : state) :
-  result (state * unit)
+  result (state * (betree_Node_t * betree_NodeIdCounter_t))
   :=
   match n with
   | O => Fail_ OutOfFuel
-  | S n0 =>
+  | S n1 =>
     match self with
     | Betree_Node_Internal node =>
       p <- betree_load_internal_node node.(betree_Internal_id) st;
-      let (st0, content) := p in
-      content0 <- betree_Node_apply_messages_to_internal n0 content msgs;
-      num_msgs <- betree_List_len (u64 * betree_Message_t) n0 content0;
+      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;
       if num_msgs s>= params.(betree_Params_min_flush_size)
       then (
-        p0 <- betree_Internal_flush n0 node params node_id_cnt content0 st0;
-        let (st1, content1) := p0 in
-        p1 <-
-          betree_Internal_flush_back n0 node params node_id_cnt content0 st0;
-        let (node0, _) := p1 in
-        p2 <-
-          betree_store_internal_node node0.(betree_Internal_id) content1 st1;
-        let (st2, _) := p2 in
-        Return (st2, tt))
+        p1 <- betree_Internal_flush n1 node params node_id_cnt l st1;
+        let (st2, p2) := p1 in
+        let (content1, p3) := p2 in
+        let (node1, node_id_cnt1) := p3 in
+        p4 <-
+          betree_store_internal_node node1.(betree_Internal_id) content1 st2;
+        let (st3, _) := p4 in
+        Return (st3, (Betree_Node_Internal node1, node_id_cnt1)))
       else (
-        p0 <-
-          betree_store_internal_node node.(betree_Internal_id) content0 st0;
-        let (st1, _) := p0 in
-        Return (st1, tt))
-    | Betree_Node_Leaf node =>
-      p <- betree_load_leaf_node node.(betree_Leaf_id) st;
-      let (st0, content) := p in
-      content0 <- betree_Node_apply_messages_to_leaf n0 content msgs;
-      len <- betree_List_len (u64 * u64) n0 content0;
-      i <- u64_mul 2%u64 params.(betree_Params_split_size);
-      if len s>= i
-      then (
-        p0 <- betree_Leaf_split n0 node content0 params node_id_cnt st0;
-        let (st1, _) := p0 in
-        p1 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st1;
+        p1 <- betree_store_internal_node node.(betree_Internal_id) l st1;
         let (st2, _) := p1 in
-        Return (st2, tt))
-      else (
-        p0 <- betree_store_leaf_node node.(betree_Leaf_id) content0 st0;
-        let (st1, _) := p0 in
-        Return (st1, tt))
-    end
-  end
-
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0
-    Source: 'src/betree.rs', lines 588:4-593:5 *)
-with betree_Node_apply_messages_back
-  (n : nat) (self : betree_Node_t) (params : betree_Params_t)
-  (node_id_cnt : betree_NodeIdCounter_t)
-  (msgs : betree_List_t (u64 * betree_Message_t)) (st : state) :
-  result (betree_Node_t * betree_NodeIdCounter_t)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match self with
-    | Betree_Node_Internal node =>
-      p <- betree_load_internal_node node.(betree_Internal_id) st;
-      let (st0, content) := p in
-      content0 <- betree_Node_apply_messages_to_internal n0 content msgs;
-      num_msgs <- betree_List_len (u64 * betree_Message_t) n0 content0;
-      if num_msgs s>= params.(betree_Params_min_flush_size)
-      then (
-        p0 <- betree_Internal_flush n0 node params node_id_cnt content0 st0;
-        let (st1, content1) := p0 in
-        p1 <-
-          betree_Internal_flush_back n0 node params node_id_cnt content0 st0;
-        let (node0, node_id_cnt0) := p1 in
-        _ <-
-          betree_store_internal_node node0.(betree_Internal_id) content1 st1;
-        Return (Betree_Node_Internal node0, node_id_cnt0))
-      else (
-        _ <- betree_store_internal_node node.(betree_Internal_id) content0 st0;
-        Return (Betree_Node_Internal node, node_id_cnt))
+        Return (st2, (Betree_Node_Internal node, node_id_cnt)))
     | Betree_Node_Leaf node =>
       p <- betree_load_leaf_node node.(betree_Leaf_id) st;
-      let (st0, content) := p in
-      content0 <- betree_Node_apply_messages_to_leaf n0 content msgs;
-      len <- betree_List_len (u64 * u64) n0 content0;
+      let (st1, content) := p in
+      l <- betree_Node_apply_messages_to_leaf n1 content msgs;
+      len <- betree_List_len (u64 * u64) n1 l;
       i <- u64_mul 2%u64 params.(betree_Params_split_size);
       if len s>= i
       then (
-        p0 <- betree_Leaf_split n0 node content0 params node_id_cnt st0;
-        let (st1, new_node) := p0 in
-        _ <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st1;
-        node_id_cnt0 <-
-          betree_Leaf_split_back n0 node content0 params node_id_cnt st0;
-        Return (Betree_Node_Internal new_node, node_id_cnt0))
+        p1 <- betree_Leaf_split n1 node l params node_id_cnt st1;
+        let (st2, p2) := p1 in
+        let (new_node, nic) := 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)))
       else (
-        _ <- betree_store_leaf_node node.(betree_Leaf_id) content0 st0;
-        Return (Betree_Node_Leaf
+        p1 <- betree_store_leaf_node node.(betree_Leaf_id) l st1;
+        let (st2, _) := p1 in
+        Return (st2, (Betree_Node_Leaf
           {| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len
-          |}, node_id_cnt))
+          |}, node_id_cnt)))
     end
   end
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]:
     Source: 'src/betree.rs', lines 576:4-582:5 *)
 Definition betree_Node_apply
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
   (new_msg : betree_Message_t) (st : state) :
-  result (state * unit)
+  result (state * (betree_Node_t * betree_NodeIdCounter_t))
   :=
-  let l := Betree_List_Nil in
   p <-
     betree_Node_apply_messages n self params node_id_cnt (Betree_List_Cons
-      (key, new_msg) l) st;
-  let (st0, _) := p in
-  _ <-
-    betree_Node_apply_messages_back n self params node_id_cnt (Betree_List_Cons
-      (key, new_msg) l) st;
-  Return (st0, tt)
+      (key, new_msg) Betree_List_Nil) st;
+  let (st1, p1) := p in
+  let (self1, node_id_cnt1) := p1 in
+  Return (st1, (self1, node_id_cnt1))
 .
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0
-    Source: 'src/betree.rs', lines 576:4-582:5 *)
-Definition betree_Node_apply_back
-  (n : nat) (self : betree_Node_t) (params : betree_Params_t)
-  (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
-  (new_msg : betree_Message_t) (st : state) :
-  result (betree_Node_t * betree_NodeIdCounter_t)
-  :=
-  let l := Betree_List_Nil in
-  betree_Node_apply_messages_back n self params node_id_cnt (Betree_List_Cons
-    (key, new_msg) l) st
-.
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
     Source: 'src/betree.rs', lines 849:4-849:60 *)
 Definition betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state * betree_BeTree_t)
   :=
   node_id_cnt <- betree_NodeIdCounter_new;
-  id <- betree_NodeIdCounter_fresh_id node_id_cnt;
-  p <- betree_store_leaf_node id Betree_List_Nil st;
-  let (st0, _) := p in
-  node_id_cnt0 <- betree_NodeIdCounter_fresh_id_back node_id_cnt;
-  Return (st0,
+  p <- betree_NodeIdCounter_fresh_id node_id_cnt;
+  let (id, nic) := p in
+  p1 <- betree_store_leaf_node id Betree_List_Nil st;
+  let (st1, _) := p1 in
+  Return (st1,
     {|
       betree_BeTree_params :=
         {|
           betree_Params_min_flush_size := min_flush_size;
           betree_Params_split_size := split_size
         |};
-      betree_BeTree_node_id_cnt := node_id_cnt0;
+      betree_BeTree_node_id_cnt := nic;
       betree_BeTree_root :=
         (Betree_Node_Leaf
           {| betree_Leaf_id := id; betree_Leaf_size := 0%u64 |})
     |})
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]:
     Source: 'src/betree.rs', lines 868:4-868:47 *)
 Definition betree_BeTree_apply
   (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
   (st : state) :
-  result (state * unit)
+  result (state * betree_BeTree_t)
   :=
   p <-
     betree_Node_apply n self.(betree_BeTree_root) self.(betree_BeTree_params)
       self.(betree_BeTree_node_id_cnt) key msg st;
-  let (st0, _) := p in
-  _ <-
-    betree_Node_apply_back n self.(betree_BeTree_root)
-      self.(betree_BeTree_params) self.(betree_BeTree_node_id_cnt) key msg st;
-  Return (st0, tt)
-.
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0
-    Source: 'src/betree.rs', lines 868:4-868:47 *)
-Definition betree_BeTree_apply_back
-  (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
-  (st : state) :
-  result betree_BeTree_t
-  :=
-  p <-
-    betree_Node_apply_back n self.(betree_BeTree_root)
-      self.(betree_BeTree_params) self.(betree_BeTree_node_id_cnt) key msg st;
-  let (n0, nic) := p in
-  Return
+  let (st1, p1) := p in
+  let (n1, nic) := p1 in
+  Return (st1,
     {|
       betree_BeTree_params := self.(betree_BeTree_params);
       betree_BeTree_node_id_cnt := nic;
-      betree_BeTree_root := n0
-    |}
+      betree_BeTree_root := n1
+    |})
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]:
     Source: 'src/betree.rs', lines 874:4-874:52 *)
 Definition betree_BeTree_insert
   (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
-  result (state * unit)
-  :=
-  p <- betree_BeTree_apply n self key (Betree_Message_Insert value) st;
-  let (st0, _) := p in
-  _ <- betree_BeTree_apply_back n self key (Betree_Message_Insert value) st;
-  Return (st0, tt)
-.
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0
-    Source: 'src/betree.rs', lines 874:4-874:52 *)
-Definition betree_BeTree_insert_back
-  (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
-  result betree_BeTree_t
+  result (state * betree_BeTree_t)
   :=
-  betree_BeTree_apply_back n self key (Betree_Message_Insert value) st
+  betree_BeTree_apply n self key (Betree_Message_Insert value) st
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]:
     Source: 'src/betree.rs', lines 880:4-880:38 *)
 Definition betree_BeTree_delete
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
-  result (state * unit)
-  :=
-  p <- betree_BeTree_apply n self key Betree_Message_Delete st;
-  let (st0, _) := p in
-  _ <- betree_BeTree_apply_back n self key Betree_Message_Delete st;
-  Return (st0, tt)
-.
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0
-    Source: 'src/betree.rs', lines 880:4-880:38 *)
-Definition betree_BeTree_delete_back
-  (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
-  result betree_BeTree_t
+  result (state * betree_BeTree_t)
   :=
-  betree_BeTree_apply_back n self key Betree_Message_Delete st
+  betree_BeTree_apply n self key Betree_Message_Delete st
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]:
     Source: 'src/betree.rs', lines 886:4-886:59 *)
 Definition betree_BeTree_upsert
   (n : nat) (self : betree_BeTree_t) (key : u64)
   (upd : betree_UpsertFunState_t) (st : state) :
-  result (state * unit)
-  :=
-  p <- betree_BeTree_apply n self key (Betree_Message_Upsert upd) st;
-  let (st0, _) := p in
-  _ <- betree_BeTree_apply_back n self key (Betree_Message_Upsert upd) st;
-  Return (st0, tt)
-.
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0
-    Source: 'src/betree.rs', lines 886:4-886:59 *)
-Definition betree_BeTree_upsert_back
-  (n : nat) (self : betree_BeTree_t) (key : u64)
-  (upd : betree_UpsertFunState_t) (st : state) :
-  result betree_BeTree_t
+  result (state * betree_BeTree_t)
   :=
-  betree_BeTree_apply_back n self key (Betree_Message_Upsert upd) st
+  betree_BeTree_apply n self key (Betree_Message_Upsert upd) st
 .
 
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]:
     Source: 'src/betree.rs', lines 895:4-895:62 *)
 Definition betree_BeTree_lookup
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
-  result (state * (option u64))
-  :=
-  betree_Node_lookup n self.(betree_BeTree_root) key st
-.
-
-(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0
-    Source: 'src/betree.rs', lines 895:4-895:62 *)
-Definition betree_BeTree_lookup_back
-  (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
-  result betree_BeTree_t
+  result (state * ((option u64) * betree_BeTree_t))
   :=
-  n0 <- betree_Node_lookup_back n self.(betree_BeTree_root) key st;
-  Return
+  p <- betree_Node_lookup n self.(betree_BeTree_root) key st;
+  let (st1, p1) := p in
+  let (o, n1) := p1 in
+  Return (st1, (o,
     {|
       betree_BeTree_params := self.(betree_BeTree_params);
       betree_BeTree_node_id_cnt := self.(betree_BeTree_node_id_cnt);
-      betree_BeTree_root := n0
-    |}
+      betree_BeTree_root := n1
+    |}))
 .
 
-(** [betree_main::main]: forward function
+(** [betree_main::main]:
     Source: 'src/betree_main.rs', lines 5:0-5:9 *)
 Definition main : result unit :=
   Return tt.
diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
index 36022a20..a9969448 100644
--- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v
+++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
@@ -11,13 +11,13 @@ Require Import BetreeMain_Types.
 Include BetreeMain_Types.
 Module BetreeMain_FunsExternal_Template.
 
-(** [betree_main::betree_utils::load_internal_node]: forward function
+(** [betree_main::betree_utils::load_internal_node]:
     Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
 Axiom betree_utils_load_internal_node
   : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t)))
 .
 
-(** [betree_main::betree_utils::store_internal_node]: forward function
+(** [betree_main::betree_utils::store_internal_node]:
     Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
 Axiom betree_utils_store_internal_node
   :
@@ -25,19 +25,19 @@ Axiom betree_utils_store_internal_node
     unit)
 .
 
-(** [betree_main::betree_utils::load_leaf_node]: forward function
+(** [betree_main::betree_utils::load_leaf_node]:
     Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
 Axiom betree_utils_load_leaf_node
   : u64 -> state -> result (state * (betree_List_t (u64 * u64)))
 .
 
-(** [betree_main::betree_utils::store_leaf_node]: forward function
+(** [betree_main::betree_utils::store_leaf_node]:
     Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
 Axiom betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit)
 .
 
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+(** [core::option::{core::option::Option<T>}::unwrap]:
     Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
 Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
index 22989256..acbc2085 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -61,31 +61,31 @@ with betree_Node_t :=
 .
 
 Definition betree_Internal_id (x : betree_Internal_t) :=
-  match x with | mkbetree_Internal_t x0 _ _ _ => x0 end
+  match x with | mkbetree_Internal_t x1 _ _ _ => x1 end
 .
 
-Notation "x1 .(betree_Internal_id)" := (betree_Internal_id x1) (at level 9).
+Notation "x2 .(betree_Internal_id)" := (betree_Internal_id x2) (at level 9).
 
 Definition betree_Internal_pivot (x : betree_Internal_t) :=
-  match x with | mkbetree_Internal_t _ x0 _ _ => x0 end
+  match x with | mkbetree_Internal_t _ x1 _ _ => x1 end
 .
 
-Notation "x1 .(betree_Internal_pivot)" := (betree_Internal_pivot x1)
+Notation "x2 .(betree_Internal_pivot)" := (betree_Internal_pivot x2)
   (at level 9)
 .
 
 Definition betree_Internal_left (x : betree_Internal_t) :=
-  match x with | mkbetree_Internal_t _ _ x0 _ => x0 end
+  match x with | mkbetree_Internal_t _ _ x1 _ => x1 end
 .
 
-Notation "x1 .(betree_Internal_left)" := (betree_Internal_left x1) (at level 9)
+Notation "x2 .(betree_Internal_left)" := (betree_Internal_left x2) (at level 9)
 .
 
 Definition betree_Internal_right (x : betree_Internal_t) :=
-  match x with | mkbetree_Internal_t _ _ _ x0 => x0 end
+  match x with | mkbetree_Internal_t _ _ _ x1 => x1 end
 .
 
-Notation "x1 .(betree_Internal_right)" := (betree_Internal_right x1)
+Notation "x2 .(betree_Internal_right)" := (betree_Internal_right x2)
   (at level 9)
 .
 
diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index 84280b96..990e27e4 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -67,8 +67,7 @@ Definition string := Coq.Strings.String.string.
 Definition char := Coq.Strings.Ascii.ascii.
 Definition char_of_byte := Coq.Strings.Ascii.ascii_of_byte.
 
-Definition core_mem_replace (a : Type) (x : a) (y : a) : a := x .
-Definition core_mem_replace_back (a : Type) (x : a) (y : a) : a := y .
+Definition core_mem_replace (a : Type) (x : a) (y : a) : a * a := (x, x) .
 
 Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }.
 Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }.
@@ -504,13 +503,15 @@ Arguments core_ops_index_Index_index {_ _}.
 (* Trait declaration: [core::ops::index::IndexMut] *)
 Record core_ops_index_IndexMut (Self Idx : Type) := mk_core_ops_index_IndexMut {
   core_ops_index_IndexMut_indexInst : core_ops_index_Index Self Idx;
-  core_ops_index_IndexMut_index_mut : Self -> Idx -> result core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output);
-  core_ops_index_IndexMut_index_mut_back : Self -> Idx -> core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output) -> result Self;
+  core_ops_index_IndexMut_index_mut :
+    Self ->
+    Idx ->
+    result (core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output) *
+            (core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output) -> result Self));
 }.
 Arguments mk_core_ops_index_IndexMut {_ _}.
 Arguments core_ops_index_IndexMut_indexInst {_ _}.
 Arguments core_ops_index_IndexMut_index_mut {_ _}.
-Arguments core_ops_index_IndexMut_index_mut_back {_ _}.
 
 (* Trait declaration [core::ops::deref::Deref] *)
 Record core_ops_deref_Deref (Self : Type) := mk_core_ops_deref_Deref {
@@ -524,13 +525,14 @@ Arguments core_ops_deref_Deref_deref {_}.
 (* Trait declaration [core::ops::deref::DerefMut] *)
 Record core_ops_deref_DerefMut (Self : Type) := mk_core_ops_deref_DerefMut {
   core_ops_deref_DerefMut_derefInst : core_ops_deref_Deref Self;
-  core_ops_deref_DerefMut_deref_mut : Self -> result core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target);
-  core_ops_deref_DerefMut_deref_mut_back : Self -> core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target) -> result Self;
+  core_ops_deref_DerefMut_deref_mut :
+    Self ->
+    result (core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target) *
+            (core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target) -> result Self));
 }.
 Arguments mk_core_ops_deref_DerefMut {_}.
 Arguments core_ops_deref_DerefMut_derefInst {_}.
 Arguments core_ops_deref_DerefMut_deref_mut {_}.
-Arguments core_ops_deref_DerefMut_deref_mut_back {_}.
 
 Record core_ops_range_Range (T : Type) := mk_core_ops_range_Range {
   core_ops_range_Range_start : T;
@@ -543,8 +545,8 @@ Arguments core_ops_range_Range_end_ {_}.
 (*** [alloc] *)
 
 Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x.
-Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result T := Return x.
-Definition alloc_boxed_Box_deref_mut_back (T : Type) (_ : T) (x : T) : result T := Return x.
+Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) :=
+  Return (x, fun x => Return x).
 
 (* Trait instance *)
 Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
@@ -556,7 +558,6 @@ Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref
 Definition alloc_boxed_Box_coreopsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {|
   core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreopsDerefInst Self;
   core_ops_deref_DerefMut_deref_mut := alloc_boxed_Box_deref_mut Self;
-  core_ops_deref_DerefMut_deref_mut_back := alloc_boxed_Box_deref_mut_back Self;
 |}.
 
 
@@ -584,6 +585,13 @@ Axiom array_repeat : forall (T : Type) (n : usize) (x : T), array T n.
 Axiom array_index_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T.
 Axiom array_update_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n).
 
+Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usize) :
+  result (T * (T -> result (array T n))) :=
+  match array_index_usize T n a i with
+  | Fail_ e => Fail_ e
+  | Return x => Return (x, array_update_usize T n a i)
+  end.
+
 (*** Slice *)
 Definition slice T := { l: list T | Z.of_nat (length l) <= usize_max}.
 
@@ -591,11 +599,25 @@ Axiom slice_len : forall (T : Type) (s : slice T), usize.
 Axiom slice_index_usize : forall (T : Type) (x : slice T) (i : usize), result T.
 Axiom slice_update_usize : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T).
 
+Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) :
+  result (T * (T -> result (slice T))) :=
+  match slice_index_usize T s i with
+  | Fail_ e => Fail_ e
+  | Return x => Return (x, slice_update_usize T s i)
+  end.
+
 (*** Subslices *)
 
 Axiom array_to_slice : forall (T : Type) (n : usize) (x : array T n), result (slice T).
 Axiom array_from_slice : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n).
 
+Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) :
+  result (slice T * (slice T -> result (array T n))) :=
+  match array_to_slice T n a with
+  | Fail_ e => Fail_ e
+  | Return x => Return (x, array_from_slice T n a)
+  end.
+
 Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T).
 Axiom array_update_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize) (ns : slice T), result (array T n).
 
@@ -639,16 +661,9 @@ Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (l
   | right _ => Fail_ Failure
   end.
 
-(* The **forward** function shouldn't be used *)
-Definition alloc_vec_Vec_push_fwd (T: Type) (v: alloc_vec_Vec T) (x: T) : unit := tt.
-
 Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l => Return (l ++ [x])).
 
-(* The **forward** function shouldn't be used *)
-Definition alloc_vec_Vec_insert_fwd (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result unit :=
-  if to_Z i <? alloc_vec_Vec_length v then Return tt else Fail_ Failure.
-
 Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) :=
   alloc_vec_Vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
@@ -661,6 +676,14 @@ Axiom alloc_vec_Vec_index_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : u
 (* Helper *)
 Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result (alloc_vec_Vec T).
 
+Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) :
+  result (T * (T -> result (alloc_vec_Vec T))) :=
+  match alloc_vec_Vec_index_usize v i with
+  | Return x =>
+    Return (x, alloc_vec_Vec_update_usize v i)
+  | Fail_ e => Fail_ e
+  end.
+
 (* Trait declaration: [core::slice::index::private_slice_index::Sealed] *)
 Definition core_slice_index_private_slice_index_Sealed (self : Type) := unit.
 
@@ -669,25 +692,23 @@ Record core_slice_index_SliceIndex (Self T : Type) := mk_core_slice_index_SliceI
   core_slice_index_SliceIndex_sealedInst : core_slice_index_private_slice_index_Sealed Self;
   core_slice_index_SliceIndex_Output : Type;
   core_slice_index_SliceIndex_get : Self -> T -> result (option core_slice_index_SliceIndex_Output);
-  core_slice_index_SliceIndex_get_mut : Self -> T -> result (option core_slice_index_SliceIndex_Output);
-  core_slice_index_SliceIndex_get_mut_back : Self -> T -> option core_slice_index_SliceIndex_Output -> result T;
+  core_slice_index_SliceIndex_get_mut :
+    Self -> T -> result (option core_slice_index_SliceIndex_Output * (option core_slice_index_SliceIndex_Output -> result T));
   core_slice_index_SliceIndex_get_unchecked : Self -> const_raw_ptr T -> result (const_raw_ptr core_slice_index_SliceIndex_Output);
   core_slice_index_SliceIndex_get_unchecked_mut : Self -> mut_raw_ptr T -> result (mut_raw_ptr core_slice_index_SliceIndex_Output);
   core_slice_index_SliceIndex_index : Self -> T -> result core_slice_index_SliceIndex_Output;
-  core_slice_index_SliceIndex_index_mut : Self -> T -> result core_slice_index_SliceIndex_Output;
-  core_slice_index_SliceIndex_index_mut_back : Self -> T -> core_slice_index_SliceIndex_Output -> result T;
+  core_slice_index_SliceIndex_index_mut :
+    Self -> T -> result (core_slice_index_SliceIndex_Output * (core_slice_index_SliceIndex_Output -> result T));
 }.
 Arguments mk_core_slice_index_SliceIndex {_ _}.
 Arguments core_slice_index_SliceIndex_sealedInst {_ _}.
 Arguments core_slice_index_SliceIndex_Output {_ _}.
 Arguments core_slice_index_SliceIndex_get {_ _}.
 Arguments core_slice_index_SliceIndex_get_mut {_ _}.
-Arguments core_slice_index_SliceIndex_get_mut_back {_ _}.
 Arguments core_slice_index_SliceIndex_get_unchecked {_ _}.
 Arguments core_slice_index_SliceIndex_get_unchecked_mut {_ _}.
 Arguments core_slice_index_SliceIndex_index {_ _}.
 Arguments core_slice_index_SliceIndex_index_mut {_ _}.
-Arguments core_slice_index_SliceIndex_index_mut_back {_ _}.
 
 (* [core::slice::index::[T]::index]: forward function *)
 Definition core_slice_index_Slice_index
@@ -704,11 +725,9 @@ Axiom core_slice_index_RangeUsize_get : forall (T : Type) (i : core_ops_range_Ra
 
 (* [core::slice::index::Range::get_mut]: forward function *)
 Axiom core_slice_index_RangeUsize_get_mut :
-  forall (T : Type), core_ops_range_Range usize -> slice T -> result (option (slice T)).
-
-(* [core::slice::index::Range::get_mut]: backward function 0 *)
-Axiom core_slice_index_RangeUsize_get_mut_back :
-  forall (T : Type), core_ops_range_Range usize -> slice T -> option (slice T) -> result (slice T).
+  forall (T : Type),
+    core_ops_range_Range usize -> slice T ->
+    result (option (slice T) * (option (slice T) -> result (slice T))).
 
 (* [core::slice::index::Range::get_unchecked]: forward function *)
 Definition core_slice_index_RangeUsize_get_unchecked
@@ -732,21 +751,14 @@ Axiom core_slice_index_RangeUsize_index :
 
 (* [core::slice::index::Range::index_mut]: forward function *)
 Axiom core_slice_index_RangeUsize_index_mut :
-  forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T).
-
-(* [core::slice::index::Range::index_mut]: backward function 0 *)
-Axiom core_slice_index_RangeUsize_index_mut_back :
-  forall (T : Type), core_ops_range_Range usize -> slice T -> slice T -> result (slice T).
+  forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T * (slice T -> result (slice T))).
 
 (* [core::slice::index::[T]::index_mut]: forward function *)
 Axiom core_slice_index_Slice_index_mut :
   forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)),
-  slice T -> Idx -> result inst.(core_slice_index_SliceIndex_Output).
-
-(* [core::slice::index::[T]::index_mut]: backward function 0 *)
-Axiom core_slice_index_Slice_index_mut_back :
-  forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)),
-  slice T -> Idx -> inst.(core_slice_index_SliceIndex_Output) -> result (slice T).
+  slice T -> Idx ->
+  result (inst.(core_slice_index_SliceIndex_Output) *
+          (inst.(core_slice_index_SliceIndex_Output) -> result (slice T))).
 
 (* [core::array::[T; N]::index]: forward function *)
 Axiom core_array_Array_index :
@@ -756,12 +768,9 @@ Axiom core_array_Array_index :
 (* [core::array::[T; N]::index_mut]: forward function *)
 Axiom core_array_Array_index_mut :
   forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx)
-  (a : array T N) (i : Idx), result inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output).
-
-(* [core::array::[T; N]::index_mut]: backward function 0 *)
-Axiom core_array_Array_index_mut_back :
-  forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx)
-  (a : array T N) (i : Idx) (x : inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output)), result (array T N).
+  (a : array T N) (i : Idx),
+  result (inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output) *
+          (inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output) -> result (array T N))).
 
 (* Trait implementation: [core::slice::index::private_slice_index::Range] *)
 Definition core_slice_index_private_slice_index_SealedRangeUsizeInst
@@ -774,12 +783,10 @@ Definition core_slice_index_SliceIndexRangeUsizeSliceTInst (T : Type) :
   core_slice_index_SliceIndex_Output := slice T;
   core_slice_index_SliceIndex_get := core_slice_index_RangeUsize_get T;
   core_slice_index_SliceIndex_get_mut := core_slice_index_RangeUsize_get_mut T;
-  core_slice_index_SliceIndex_get_mut_back := core_slice_index_RangeUsize_get_mut_back T;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_RangeUsize_get_unchecked T;
   core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_RangeUsize_get_unchecked_mut T;
   core_slice_index_SliceIndex_index := core_slice_index_RangeUsize_index T;
   core_slice_index_SliceIndex_index_mut := core_slice_index_RangeUsize_index_mut T;
-  core_slice_index_SliceIndex_index_mut_back := core_slice_index_RangeUsize_index_mut_back T;
 |}.
 
 (* Trait implementation: [core::slice::index::[T]] *)
@@ -796,7 +803,6 @@ Definition core_ops_index_IndexMutSliceTIInst (T Idx : Type)
   core_ops_index_IndexMut (slice T) Idx := {|
   core_ops_index_IndexMut_indexInst := core_ops_index_IndexSliceTIInst T Idx inst;
   core_ops_index_IndexMut_index_mut := core_slice_index_Slice_index_mut T Idx inst;
-  core_ops_index_IndexMut_index_mut_back := core_slice_index_Slice_index_mut_back T Idx inst;
 |}.
 
 (* Trait implementation: [core::array::[T; N]] *)
@@ -813,18 +819,14 @@ Definition core_ops_index_IndexMutArrayInst (T Idx : Type) (N : usize)
   core_ops_index_IndexMut (array T N) Idx := {|
   core_ops_index_IndexMut_indexInst := core_ops_index_IndexArrayInst T Idx N inst.(core_ops_index_IndexMut_indexInst);
   core_ops_index_IndexMut_index_mut := core_array_Array_index_mut T Idx N inst;
-  core_ops_index_IndexMut_index_mut_back := core_array_Array_index_mut_back T Idx N inst;
 |}.
 
 (* [core::slice::index::usize::get]: forward function *)
 Axiom core_slice_index_usize_get : forall (T : Type), usize -> slice T -> result (option T).
 
 (* [core::slice::index::usize::get_mut]: forward function *)
-Axiom core_slice_index_usize_get_mut : forall (T : Type), usize -> slice T -> result (option T).
-
-(* [core::slice::index::usize::get_mut]: backward function 0 *)
-Axiom core_slice_index_usize_get_mut_back :
-  forall (T : Type), usize -> slice T -> option T -> result (slice T).
+Axiom core_slice_index_usize_get_mut :
+  forall (T : Type), usize -> slice T -> result (option T * (option T -> result (slice T))).
 
 (* [core::slice::index::usize::get_unchecked]: forward function *)
 Axiom core_slice_index_usize_get_unchecked :
@@ -838,11 +840,8 @@ Axiom core_slice_index_usize_get_unchecked_mut :
 Axiom core_slice_index_usize_index : forall (T : Type), usize -> slice T -> result T.
 
 (* [core::slice::index::usize::index_mut]: forward function *)
-Axiom core_slice_index_usize_index_mut : forall (T : Type), usize -> slice T -> result T.
-
-(* [core::slice::index::usize::index_mut]: backward function 0 *)
-Axiom core_slice_index_usize_index_mut_back :
-  forall (T : Type), usize -> slice T -> T -> result (slice T).
+Axiom core_slice_index_usize_index_mut :
+  forall (T : Type), usize -> slice T -> result (T * (T -> result (slice T))).
 
 (* Trait implementation: [core::slice::index::private_slice_index::usize] *)
 Definition core_slice_index_private_slice_index_SealedUsizeInst
@@ -855,12 +854,10 @@ Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) :
   core_slice_index_SliceIndex_Output := T;
   core_slice_index_SliceIndex_get := core_slice_index_usize_get T;
   core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut T;
-  core_slice_index_SliceIndex_get_mut_back := core_slice_index_usize_get_mut_back T;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_usize_get_unchecked T;
   core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_usize_get_unchecked_mut T;
   core_slice_index_SliceIndex_index := core_slice_index_usize_index T;
   core_slice_index_SliceIndex_index_mut := core_slice_index_usize_index_mut T;
-  core_slice_index_SliceIndex_index_mut_back := core_slice_index_usize_index_mut_back T;
 |}.
 
 (* [alloc::vec::Vec::index]: forward function *)
@@ -869,12 +866,9 @@ Axiom alloc_vec_Vec_index : forall (T Idx : Type) (inst : core_slice_index_Slice
 
 (* [alloc::vec::Vec::index_mut]: forward function *)
 Axiom alloc_vec_Vec_index_mut : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T))
-  (Self : alloc_vec_Vec T) (i : Idx), result inst.(core_slice_index_SliceIndex_Output).
-
-(* [alloc::vec::Vec::index_mut]: backward function 0 *)
-Axiom alloc_vec_Vec_index_mut_back :
-  forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T))
-  (Self : alloc_vec_Vec T) (i : Idx) (x : inst.(core_slice_index_SliceIndex_Output)), result (alloc_vec_Vec T).
+  (Self : alloc_vec_Vec T) (i : Idx),
+  result (inst.(core_slice_index_SliceIndex_Output) *
+          (inst.(core_slice_index_SliceIndex_Output) -> result (alloc_vec_Vec T))).
 
 (* Trait implementation: [alloc::vec::Vec] *)
 Definition alloc_vec_Vec_coreopsindexIndexInst (T Idx : Type)
@@ -890,7 +884,6 @@ Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type)
   core_ops_index_IndexMut (alloc_vec_Vec T) Idx := {|
   core_ops_index_IndexMut_indexInst := alloc_vec_Vec_coreopsindexIndexInst T Idx inst;
   core_ops_index_IndexMut_index_mut := alloc_vec_Vec_index_mut T Idx inst;
-  core_ops_index_IndexMut_index_mut_back := alloc_vec_Vec_index_mut_back T Idx inst;
 |}.
 
 (*** Theorems *)
@@ -901,10 +894,6 @@ Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usiz
 
 Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
   alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
-    alloc_vec_Vec_index_usize v i.
-
-Axiom alloc_vec_Vec_index_mut_back_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
-  alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x =
-    alloc_vec_Vec_update_usize v i x.
+    alloc_vec_Vec_index_mut_usize v i.
 
 End Primitives.