Merge pull request #33 from AeneasVerif/son_refactor

Update the code following Charon's refactor

23 files changed, 1513 insertions, 1495 deletions

diff --git a/README.md b/README.md
index 3acba834..31dc74f4 100644
--- a/README.md
+++ b/README.md
@@ -13,24 +13,18 @@ Wall in Pompei, digital image from Michael Lahanis.
 
 Aeneas is a verification toolchain for Rust programs.  It relies on a translation from Rusts's MIR
 internal language to a pure lamdba calculus.  It is intended to be used in combination with
-[Charon](https://github.com/Kachoc/charon), which compiles Rust programs to an intermediate
-representation called LLBC. It currently has backends for the [F\*](https://www.fstar-lang.org)
-theorem prover and the [Coq](https://coq.inria.fr/) proof assistant, and we intend to add 
-backends for other provers such as [HOL4](https://hol-theorem-prover.org/) or [LEAN](https://leanprover.github.io/).
+[Charon](https://github.com/AeneasVerif/charon), which compiles Rust programs to an intermediate
+representation called LLBC. It currently has backends for [F\*](https://www.fstar-lang.org),
+[Coq](https://coq.inria.fr/), [HOL4](https://hol-theorem-prover.org/) and [LEAN](https://leanprover.github.io/).
 
 ## Project Structure
 
 - `src`: the OCaml sources. Note that we rely on [Dune](https://github.com/ocaml/dune)
   to build the project.
-- `fstar`: F\* files providing basic definitions and notations for the
-  generated code (basic definitions for arithmetic types and operations,
-  collections like vectors, etc.).
+- `backends`: standard libraries for the existing backends (definitions for
+   arithmetic operations, for standard collections like vectors, theorems, tactics, etc.)
 - `tests`: files generated by applying Aeneas on some of the test files of Charon,
   completed with hand-written files (proof scripts, mostly).
-- `rust-tests`: miscelleanous files, to test the semantics of Rust or generate
-  code in a one-shot manner (mostly used for the arithmetic definitions, for
-  instance to generate `MIN` and `MAX` constants for all the integer types
-  supported by Rust).
 
 ## Installation & Build
 
@@ -83,27 +77,34 @@ to display a detailed documentation.
 
 ## Targeted Subset And Current Limitations
 
-We target **safe** Rust.
+We target **safe** Rust. This means we have no support for unsafe Rust, though we plan to
+design a mechanism to allow using Aeneas in combination with tools targeting unsafe Rust.
 
 We have the following limitations, that we plan to address one by one:
 
-- **no loops**: ongoing work. We are currently working on a "join" operation on
-  environments to address this issue.
-- **no functions pointers/closures/traits**: ongoing work.
+- **loops**: no nested loops for now. We are working on lifting this limitation.
+- **no functions pointers/closures/traits**: ongoing work. We are actively working on this
+  and plan to have support soon.
 - **limited type parametricity**: it is not possible for now to instantiate a type
   parameter with a type containing a borrow. This is mostly an engineering
   issue. We intend to quickly address the issue for types (i.e., allow `Option<&mut T>`),
   and later address it for functions (i.e., allow `f<&mut T>` - we consider this to
   be less urgent).
 - **no nested borrows in function signatures**: ongoing work.
-- **no interior mutability**: long-term effort. Interior mutability introduces
-  true aliasing: we will probably have to use a low-level memory model to address
-  this issue.
-  Note that interior mutability is truely necessary for concurrent execution (it
-  is exploited to implement the synchronisation primitives).
+- **interior mutability**: ongoing work. We are thinking of modeling the effects of
+  interior mutability by using ghost states.
 - **no concurrent execution**: long-term effort. We plan to address coarse-grained
   parallelism as a long-term goal.
 
+## Backend Support
+
+We currently support F\*, Coq, HOL4 and Lean. We would be interested in having an Isabelle
+backend. Our most mature backends are Lean and HOL4, for which we have in particular
+support for partial functions and extrinsic proofs of termination (see
+`./backends/lean/Base/Diverge/Elab.lean` and `./backends/hol4/divDefLib.sig` for instance)
+and tactics specialized for monadic programs (see
+`./backends/lean/Base/Progress/Progress.lean` and `./backends/hol4/primitivesLib.sml`).
+
 ## Formalization
 
 The translation has been formalized and published at ICFP2022: [Aeneas: Rust
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index d819768b..b646a53d 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -214,7 +214,9 @@ let () =
 
       (* Print a warning if the crate contains loops (loops are experimental for now) *)
       let has_loops =
-        List.exists Aeneas.LlbcAstUtils.fun_decl_has_loops m.functions
+        A.FunDeclId.Map.exists
+          (fun _ -> Aeneas.LlbcAstUtils.fun_decl_has_loops)
+          m.functions
       in
       if has_loops then log#lwarning (lazy "Support for loops is experimental");
 
@@ -222,7 +224,9 @@ let () =
          whenever there are opaque functions *)
       if
         !backend = Lean
-        && List.exists (fun (d : A.fun_decl) -> d.body = None) m.functions
+        && A.FunDeclId.Map.exists
+             (fun _ (d : A.fun_decl) -> d.body = None)
+             m.functions
         && not !split_files
       then (
         log#error
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 449463c8..154c5a21 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -15,7 +15,9 @@ let log = L.interpreter_log
 let compute_type_fun_global_contexts (m : A.crate) :
     C.type_context * C.fun_context * C.global_context =
   let type_decls_list, _, _ = split_declarations m.declarations in
-  let type_decls, fun_decls, global_decls = compute_defs_maps m in
+  let type_decls = m.types in
+  let fun_decls = m.functions in
+  let global_decls = m.globals in
   let type_decls_groups, _funs_defs_groups, _globals_defs_groups =
     split_declarations_to_group_maps m.declarations
   in
@@ -488,7 +490,7 @@ module Test = struct
    *)
   let test_unit_function (crate : A.crate) (fid : A.FunDeclId.id) : unit =
     (* Retrieve the function declaration *)
-    let fdef = A.FunDeclId.nth crate.functions fid in
+    let fdef = A.FunDeclId.Map.find fid crate.functions in
     let body = Option.get fdef.body in
 
     (* Debug *)
@@ -541,11 +543,15 @@ module Test = struct
 
   (** Test all the unit functions in a list of function definitions *)
   let test_unit_functions (crate : A.crate) : unit =
-    let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in
-    let test_unit_fun (def : A.fun_decl) : unit =
+    let unit_funs =
+      A.FunDeclId.Map.filter
+        (fun _ -> fun_decl_is_transparent_unit)
+        crate.functions
+    in
+    let test_unit_fun _ (def : A.fun_decl) : unit =
       test_unit_function crate def.A.def_id
     in
-    List.iter test_unit_fun unit_funs
+    A.FunDeclId.Map.iter test_unit_fun unit_funs
 
   (** Execute the symbolic interpreter on a function. *)
   let test_function_symbolic (synthesize : bool) (type_context : C.type_context)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 8b193ee2..b348ba1d 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -426,7 +426,9 @@ let remove_shallow_borrows (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
 let apply_passes (crate : A.crate) : A.crate =
   let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in
   let functions =
-    List.fold_left (fun fl pass -> List.map pass fl) crate.functions passes
+    List.fold_left
+      (fun fl pass -> A.FunDeclId.Map.map pass fl)
+      crate.functions passes
   in
   let crate = { crate with functions } in
   log#ldebug
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 6c6435c5..70ef5e3d 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -291,7 +291,9 @@ let translate_crate_to_pure (crate : A.crate) :
   let trans_ctx = { type_context; fun_context; global_context } in
 
   (* Translate all the type definitions *)
-  let type_decls = SymbolicToPure.translate_type_decls crate.types in
+  let type_decls =
+    SymbolicToPure.translate_type_decls (T.TypeDeclId.Map.values crate.types)
+  in
 
   (* Compute the type definition map *)
   let type_decls_map =
@@ -318,7 +320,7 @@ let translate_crate_to_pure (crate : A.crate) :
                 (LlbcAstUtils.fun_body_get_input_vars body)
         in
         (A.Regular fdef.def_id, input_names, fdef.signature))
-      crate.functions
+      (A.FunDeclId.Map.values crate.functions)
   in
   let sigs = List.append assumed_sigs local_sigs in
   let fun_sigs =
@@ -330,7 +332,7 @@ let translate_crate_to_pure (crate : A.crate) :
   let pure_translations =
     List.map
       (translate_function_to_pure trans_ctx fun_sigs type_decls_map)
-      crate.functions
+      (A.FunDeclId.Map.values crate.functions)
   in
 
   (* Apply the micro-passes *)
@@ -989,7 +991,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   in
 
   let ctx =
-    List.fold_left Extract.extract_global_decl_register_names ctx crate.globals
+    List.fold_left Extract.extract_global_decl_register_names ctx
+      (A.GlobalDeclId.Map.values crate.globals)
   in
 
   (* Open the output file *)
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 85aecfc8..e15085ff 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -260,28 +260,6 @@ Definition betree_leaf_split_back
   betree_node_id_counter_fresh_id_back node_id_cnt0
 .
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
-Fixpoint betree_node_lookup_in_bindings_fwd
-  (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
-  result (option u64)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match bindings with
-    | BetreeListCons hd tl =>
-      let (i, i0) := hd in
-      if i s= key
-      then Return (Some i0)
-      else
-        if i s> key
-        then Return None
-        else betree_node_lookup_in_bindings_fwd n0 key tl
-    | BetreeListNil => Return None
-    end
-  end
-.
-
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
 Fixpoint betree_node_lookup_first_message_for_key_fwd
   (n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) :
@@ -386,8 +364,62 @@ Fixpoint betree_node_apply_upserts_back
   end
 .
 
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+Fixpoint betree_node_lookup_in_bindings_fwd
+  (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
+  result (option u64)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match bindings with
+    | BetreeListCons hd tl =>
+      let (i, i0) := hd in
+      if i s= key
+      then Return (Some i0)
+      else
+        if i s> key
+        then Return None
+        else betree_node_lookup_in_bindings_fwd n0 key tl
+    | BetreeListNil => Return None
+    end
+  end
+.
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+Fixpoint betree_internal_lookup_in_children_fwd
+  (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_fwd n0 self.(Betree_internal_left) key st
+    else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
+  end
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+with betree_internal_lookup_in_children_back
+  (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
+  result Betree_internal_t
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    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)))
+    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))
+  end
+
 (** [betree_main::betree::Node::{5}::lookup]: forward function *)
-Fixpoint betree_node_lookup_fwd
+with betree_node_lookup_fwd
   (n : nat) (self : Betree_node_t) (key : u64) (st : state) :
   result (state * (option u64))
   :=
@@ -526,144 +558,6 @@ with betree_node_lookup_back
       Return (BetreeNodeLeaf node)
     end
   end
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
-with betree_internal_lookup_in_children_fwd
-  (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_fwd n0 self.(Betree_internal_left) key st
-    else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
-  end
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
-with betree_internal_lookup_in_children_back
-  (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
-  result Betree_internal_t
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    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)))
-    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))
-  end
-.
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
-Fixpoint betree_node_lookup_mut_in_bindings_fwd
-  (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
-    | BetreeListCons hd tl =>
-      let (i, i0) := hd in
-      if i s>= key
-      then Return (BetreeListCons (i, i0) tl)
-      else betree_node_lookup_mut_in_bindings_fwd n0 key tl
-    | BetreeListNil => Return BetreeListNil
-    end
-  end
-.
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
-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))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match bindings with
-    | BetreeListCons hd tl =>
-      let (i, i0) := hd in
-      if i s>= key
-      then Return ret
-      else (
-        tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret;
-        Return (BetreeListCons (i, i0) tl0))
-    | BetreeListNil => Return ret
-    end
-  end
-.
-
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
-Definition betree_node_apply_to_leaf_fwd_back
-  (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_fwd n key bindings;
-  b <- betree_list_head_has_key_fwd u64 bindings0 key;
-  if b
-  then (
-    hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
-    match new_msg with
-    | BetreeMessageInsert v =>
-      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-      bindings2 <-
-        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
-    | BetreeMessageDelete =>
-      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
-    | BetreeMessageUpsert s =>
-      let (_, i) := hd in
-      v <- betree_upsert_update_fwd (Some i) s;
-      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
-      bindings2 <-
-        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
-    end)
-  else
-    match new_msg with
-    | BetreeMessageInsert v =>
-      bindings1 <-
-        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
-    | BetreeMessageDelete =>
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings0
-    | BetreeMessageUpsert s =>
-      v <- betree_upsert_update_fwd None s;
-      bindings1 <-
-        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
-      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
-    end
-.
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
-Fixpoint betree_node_apply_messages_to_leaf_fwd_back
-  (n : nat) (bindings : Betree_list_t (u64 * u64))
-  (new_msgs : Betree_list_t (u64 * Betree_message_t)) :
-  result (Betree_list_t (u64 * u64))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    match new_msgs with
-    | BetreeListCons new_msg new_msgs_tl =>
-      let (i, m) := new_msg in
-      bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
-      betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
-    | BetreeListNil => Return bindings
-    end
-  end
 .
 
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
@@ -811,8 +705,210 @@ Fixpoint betree_node_apply_messages_to_internal_fwd_back
   end
 .
 
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+Fixpoint betree_node_lookup_mut_in_bindings_fwd
+  (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
+    | BetreeListCons hd tl =>
+      let (i, i0) := hd in
+      if i s>= key
+      then Return (BetreeListCons (i, i0) tl)
+      else betree_node_lookup_mut_in_bindings_fwd n0 key tl
+    | BetreeListNil => Return BetreeListNil
+    end
+  end
+.
+
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+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))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match bindings with
+    | BetreeListCons hd tl =>
+      let (i, i0) := hd in
+      if i s>= key
+      then Return ret
+      else (
+        tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret;
+        Return (BetreeListCons (i, i0) tl0))
+    | BetreeListNil => Return ret
+    end
+  end
+.
+
+(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+Definition betree_node_apply_to_leaf_fwd_back
+  (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_fwd n key bindings;
+  b <- betree_list_head_has_key_fwd u64 bindings0 key;
+  if b
+  then (
+    hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
+    match new_msg with
+    | BetreeMessageInsert v =>
+      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+      bindings2 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
+    | BetreeMessageDelete =>
+      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+    | BetreeMessageUpsert s =>
+      let (_, i) := hd in
+      v <- betree_upsert_update_fwd (Some i) s;
+      bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+      bindings2 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings2
+    end)
+  else
+    match new_msg with
+    | BetreeMessageInsert v =>
+      bindings1 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+    | BetreeMessageDelete =>
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings0
+    | BetreeMessageUpsert s =>
+      v <- betree_upsert_update_fwd None s;
+      bindings1 <-
+        betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
+      betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+    end
+.
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+Fixpoint betree_node_apply_messages_to_leaf_fwd_back
+  (n : nat) (bindings : Betree_list_t (u64 * u64))
+  (new_msgs : Betree_list_t (u64 * Betree_message_t)) :
+  result (Betree_list_t (u64 * u64))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    match new_msgs with
+    | BetreeListCons new_msg new_msgs_tl =>
+      let (i, m) := new_msg in
+      bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
+      betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
+    | BetreeListNil => Return bindings
+    end
+  end
+.
+
+(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+Fixpoint betree_internal_flush_fwd
+  (n : nat) (self : Betree_internal_t) (params : Betree_params_t)
+  (node_id_cnt : Betree_node_id_counter_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_list_partition_at_pivot_fwd Betree_message_t n0 content
+        self.(Betree_internal_pivot);
+    let (msgs_left, msgs_right) := p in
+    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
+    if len_left s>= params.(Betree_params_min_flush_size)
+    then (
+      p0 <-
+        betree_node_apply_messages_fwd 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_fwd (u64 * Betree_message_t) n0 msgs_right;
+      if len_right s>= params.(Betree_params_min_flush_size)
+      then (
+        p2 <-
+          betree_node_apply_messages_fwd 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, BetreeListNil))
+      else Return (st0, msgs_right))
+    else (
+      p0 <-
+        betree_node_apply_messages_fwd 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::Internal::{4}::flush]: backward function 0 *)
+with betree_internal_flush_back
+  (n : nat) (self : Betree_internal_t) (params : Betree_params_t)
+  (node_id_cnt : Betree_node_id_counter_t)
+  (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
+  result (Betree_internal_t * Betree_node_id_counter_t)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n0 =>
+    p <-
+      betree_list_partition_at_pivot_fwd Betree_message_t n0 content
+        self.(Betree_internal_pivot);
+    let (msgs_left, msgs_right) := p in
+    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
+    if len_left s>= params.(Betree_params_min_flush_size)
+    then (
+      p0 <-
+        betree_node_apply_messages_fwd 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 (n1, node_id_cnt0) := p1 in
+      len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 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))
+      else
+        Return (mkBetree_internal_t self.(Betree_internal_id)
+          self.(Betree_internal_pivot) n1 self.(Betree_internal_right),
+          node_id_cnt0))
+    else (
+      p0 <-
+        betree_node_apply_messages_back n0 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))
+  end
+
 (** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
-Fixpoint betree_node_apply_messages_fwd
+with betree_node_apply_messages_fwd
   (n : nat) (self : Betree_node_t) (params : Betree_params_t)
   (node_id_cnt : Betree_node_id_counter_t)
   (msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) :
@@ -922,102 +1018,6 @@ with betree_node_apply_messages_back
           |}, node_id_cnt))
     end
   end
-
-(** [betree_main::betree::Internal::{4}::flush]: forward function *)
-with betree_internal_flush_fwd
-  (n : nat) (self : Betree_internal_t) (params : Betree_params_t)
-  (node_id_cnt : Betree_node_id_counter_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_list_partition_at_pivot_fwd Betree_message_t n0 content
-        self.(Betree_internal_pivot);
-    let (msgs_left, msgs_right) := p in
-    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
-    if len_left s>= params.(Betree_params_min_flush_size)
-    then (
-      p0 <-
-        betree_node_apply_messages_fwd 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_fwd (u64 * Betree_message_t) n0 msgs_right;
-      if len_right s>= params.(Betree_params_min_flush_size)
-      then (
-        p2 <-
-          betree_node_apply_messages_fwd 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, BetreeListNil))
-      else Return (st0, msgs_right))
-    else (
-      p0 <-
-        betree_node_apply_messages_fwd 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::Internal::{4}::flush]: backward function 0 *)
-with betree_internal_flush_back
-  (n : nat) (self : Betree_internal_t) (params : Betree_params_t)
-  (node_id_cnt : Betree_node_id_counter_t)
-  (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
-  result (Betree_internal_t * Betree_node_id_counter_t)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n0 =>
-    p <-
-      betree_list_partition_at_pivot_fwd Betree_message_t n0 content
-        self.(Betree_internal_pivot);
-    let (msgs_left, msgs_right) := p in
-    len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
-    if len_left s>= params.(Betree_params_min_flush_size)
-    then (
-      p0 <-
-        betree_node_apply_messages_fwd 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 (n1, node_id_cnt0) := p1 in
-      len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 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))
-      else
-        Return (mkBetree_internal_t self.(Betree_internal_id)
-          self.(Betree_internal_pivot) n1 self.(Betree_internal_right),
-          node_id_cnt0))
-    else (
-      p0 <-
-        betree_node_apply_messages_back n0 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))
-  end
 .
 
 (** [betree_main::betree::Node::{5}::apply]: forward function *)
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
index c8af54cd..4a4e75aa 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -37,19 +37,19 @@ mkBetree_leaf_t {
 }
 .
 
-(** [betree_main::betree::Node] *)
-Inductive Betree_node_t :=
-| BetreeNodeInternal : Betree_internal_t -> Betree_node_t
-| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t
-
 (** [betree_main::betree::Internal] *)
-with Betree_internal_t :=
+Inductive Betree_internal_t :=
 | mkBetree_internal_t :
   u64 ->
   u64 ->
   Betree_node_t ->
   Betree_node_t ->
   Betree_internal_t
+
+(** [betree_main::betree::Node] *)
+with Betree_node_t :=
+| BetreeNodeInternal : Betree_internal_t -> Betree_node_t
+| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t
 .
 
 Definition Betree_internal_id (x : Betree_internal_t) :=
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index f93254e1..c1c24e00 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -238,23 +238,23 @@ Definition test_char_fwd : result char :=
   Return (char_of_byte Coq.Init.Byte.x61)
 .
 
-(** [no_nested_borrows::NodeElem] *)
-Inductive Node_elem_t (T : Type) :=
-| NodeElemCons : Tree_t T -> Node_elem_t T -> Node_elem_t T
-| NodeElemNil : Node_elem_t T
-
 (** [no_nested_borrows::Tree] *)
-with Tree_t (T : Type) :=
+Inductive Tree_t (T : Type) :=
 | TreeLeaf : T -> Tree_t T
 | TreeNode : T -> Node_elem_t T -> Tree_t T -> Tree_t T
-.
 
-Arguments NodeElemCons {T} _ _.
-Arguments NodeElemNil {T}.
+(** [no_nested_borrows::NodeElem] *)
+with Node_elem_t (T : Type) :=
+| NodeElemCons : Tree_t T -> Node_elem_t T -> Node_elem_t T
+| NodeElemNil : Node_elem_t T
+.
 
 Arguments TreeLeaf {T} _.
 Arguments TreeNode {T} _ _ _.
 
+Arguments NodeElemCons {T} _ _.
+Arguments NodeElemNil {T}.
+
 (** [no_nested_borrows::list_length]: forward function *)
 Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
   match l with
diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
index 5a9776ab..823df03a 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
@@ -23,12 +23,6 @@ let betree_list_partition_at_pivot_decreases (t : Type0)
   (self : betree_list_t (u64 & t)) (pivot : u64) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
-
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
 unfold
 let betree_node_lookup_first_message_for_key_decreases (key : u64)
@@ -42,10 +36,10 @@ let betree_node_apply_upserts_decreases
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
 unfold
-let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
-  (st : state) : nat =
+let betree_node_lookup_in_bindings_decreases (key : u64)
+  (bindings : betree_list_t (u64 & u64)) : nat =
   admit ()
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
@@ -54,17 +48,10 @@ let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_mut_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
 unfold
-let betree_node_apply_messages_to_leaf_decreases
-  (bindings : betree_list_t (u64 & u64))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
+let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
+  (st : state) : nat =
   admit ()
 
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
@@ -86,11 +73,17 @@ let betree_node_apply_messages_to_internal_decreases
   (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
 unfold
-let betree_node_apply_messages_decreases (self : betree_node_t)
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
+let betree_node_lookup_mut_in_bindings_decreases (key : u64)
+  (bindings : betree_list_t (u64 & u64)) : nat =
+  admit ()
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *)
+unfold
+let betree_node_apply_messages_to_leaf_decreases
+  (bindings : betree_list_t (u64 & u64))
+  (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
   admit ()
 
 (** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
@@ -100,3 +93,10 @@ let betree_internal_flush_decreases (self : betree_internal_t)
   (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
   admit ()
 
+(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+unfold
+let betree_node_apply_messages_decreases (self : betree_node_t)
+  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
+  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
+  admit ()
+
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index f1bc1191..bd4e37d4 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -222,24 +222,6 @@ let betree_leaf_split_back
   let* _ = betree_store_leaf_node_fwd id1 content1 st0 in
   betree_node_id_counter_fresh_id_back node_id_cnt0
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
-let rec betree_node_lookup_in_bindings_fwd
-  (key : u64) (bindings : betree_list_t (u64 & u64)) :
-  Tot (result (option u64))
-  (decreases (betree_node_lookup_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i = key
-    then Return (Some i0)
-    else
-      if i > key
-      then Return None
-      else betree_node_lookup_in_bindings_fwd key tl
-  | BetreeListNil -> Return None
-  end
-
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
 let rec betree_node_lookup_first_message_for_key_fwd
   (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
@@ -326,8 +308,50 @@ let rec betree_node_apply_upserts_back
     betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
       BetreeMessageInsert v)
 
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+let rec betree_node_lookup_in_bindings_fwd
+  (key : u64) (bindings : betree_list_t (u64 & u64)) :
+  Tot (result (option u64))
+  (decreases (betree_node_lookup_in_bindings_decreases key bindings))
+  =
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i = key
+    then Return (Some i0)
+    else
+      if i > key
+      then Return None
+      else betree_node_lookup_in_bindings_fwd key tl
+  | BetreeListNil -> Return None
+  end
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+let rec betree_internal_lookup_in_children_fwd
+  (self : betree_internal_t) (key : u64) (st : state) :
+  Tot (result (state & (option u64)))
+  (decreases (betree_internal_lookup_in_children_decreases self key st))
+  =
+  if key < self.betree_internal_pivot
+  then betree_node_lookup_fwd self.betree_internal_left key st
+  else betree_node_lookup_fwd self.betree_internal_right key st
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+and betree_internal_lookup_in_children_back
+  (self : betree_internal_t) (key : u64) (st : state) :
+  Tot (result betree_internal_t)
+  (decreases (betree_internal_lookup_in_children_decreases self key st))
+  =
+  if key < self.betree_internal_pivot
+  then
+    let* n = betree_node_lookup_back self.betree_internal_left key st in
+    Return { self with betree_internal_left = n }
+  else
+    let* n = betree_node_lookup_back self.betree_internal_right key st in
+    Return { self with betree_internal_right = n }
+
 (** [betree_main::betree::Node::{5}::lookup]: forward function *)
-let rec betree_node_lookup_fwd
+and betree_node_lookup_fwd
   (self : betree_node_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
   (decreases (betree_node_lookup_decreases self key st))
@@ -451,123 +475,6 @@ and betree_node_lookup_back
     Return (BetreeNodeLeaf node)
   end
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
-and betree_internal_lookup_in_children_fwd
-  (self : betree_internal_t) (key : u64) (st : state) :
-  Tot (result (state & (option u64)))
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then betree_node_lookup_fwd self.betree_internal_left key st
-  else betree_node_lookup_fwd self.betree_internal_right key st
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
-and betree_internal_lookup_in_children_back
-  (self : betree_internal_t) (key : u64) (st : state) :
-  Tot (result betree_internal_t)
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then
-    let* n = betree_node_lookup_back self.betree_internal_left key st in
-    Return { self with betree_internal_left = n }
-  else
-    let* n = betree_node_lookup_back self.betree_internal_right key st in
-    Return { self with betree_internal_right = n }
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
-let rec betree_node_lookup_mut_in_bindings_fwd
-  (key : u64) (bindings : betree_list_t (u64 & u64)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return (BetreeListCons (i, i0) tl)
-    else betree_node_lookup_mut_in_bindings_fwd key tl
-  | BetreeListNil -> Return BetreeListNil
-  end
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
-let rec betree_node_lookup_mut_in_bindings_back
-  (key : u64) (bindings : betree_list_t (u64 & u64))
-  (ret : betree_list_t (u64 & u64)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return ret
-    else
-      let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
-      Return (BetreeListCons (i, i0) tl0)
-  | BetreeListNil -> Return ret
-  end
-
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
-let betree_node_apply_to_leaf_fwd_back
-  (bindings : betree_list_t (u64 & u64)) (key : u64)
-  (new_msg : betree_message_t) :
-  result (betree_list_t (u64 & u64))
-  =
-  let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
-  let* b = betree_list_head_has_key_fwd u64 bindings0 key in
-  if b
-  then
-    let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
-    begin match new_msg with
-    | BetreeMessageInsert v ->
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      let* bindings2 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    | BetreeMessageDelete ->
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    | BetreeMessageUpsert s ->
-      let (_, i) = hd in
-      let* v = betree_upsert_update_fwd (Some i) s in
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      let* bindings2 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    end
-  else
-    begin match new_msg with
-    | BetreeMessageInsert v ->
-      let* bindings1 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    | BetreeMessageDelete ->
-      betree_node_lookup_mut_in_bindings_back key bindings bindings0
-    | BetreeMessageUpsert s ->
-      let* v = betree_upsert_update_fwd None s in
-      let* bindings1 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    end
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
-let rec betree_node_apply_messages_to_leaf_fwd_back
-  (bindings : betree_list_t (u64 & u64))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
-  =
-  begin match new_msgs with
-  | BetreeListCons new_msg new_msgs_tl ->
-    let (i, m) = new_msg in
-    let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
-    betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
-  | BetreeListNil -> Return bindings
-  end
-
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec betree_node_filter_messages_for_key_fwd_back
@@ -699,8 +606,181 @@ let rec betree_node_apply_messages_to_internal_fwd_back
   | BetreeListNil -> Return msgs
   end
 
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+let rec betree_node_lookup_mut_in_bindings_fwd
+  (key : u64) (bindings : betree_list_t (u64 & u64)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
+  =
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i >= key
+    then Return (BetreeListCons (i, i0) tl)
+    else betree_node_lookup_mut_in_bindings_fwd key tl
+  | BetreeListNil -> Return BetreeListNil
+  end
+
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+let rec betree_node_lookup_mut_in_bindings_back
+  (key : u64) (bindings : betree_list_t (u64 & u64))
+  (ret : betree_list_t (u64 & u64)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
+  =
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i >= key
+    then Return ret
+    else
+      let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
+      Return (BetreeListCons (i, i0) tl0)
+  | BetreeListNil -> Return ret
+  end
+
+(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+let betree_node_apply_to_leaf_fwd_back
+  (bindings : betree_list_t (u64 & u64)) (key : u64)
+  (new_msg : betree_message_t) :
+  result (betree_list_t (u64 & u64))
+  =
+  let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
+  let* b = betree_list_head_has_key_fwd u64 bindings0 key in
+  if b
+  then
+    let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
+    begin match new_msg with
+    | BetreeMessageInsert v ->
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      let* bindings2 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings2
+    | BetreeMessageDelete ->
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    | BetreeMessageUpsert s ->
+      let (_, i) = hd in
+      let* v = betree_upsert_update_fwd (Some i) s in
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      let* bindings2 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings2
+    end
+  else
+    begin match new_msg with
+    | BetreeMessageInsert v ->
+      let* bindings1 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    | BetreeMessageDelete ->
+      betree_node_lookup_mut_in_bindings_back key bindings bindings0
+    | BetreeMessageUpsert s ->
+      let* v = betree_upsert_update_fwd None s in
+      let* bindings1 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    end
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+let rec betree_node_apply_messages_to_leaf_fwd_back
+  (bindings : betree_list_t (u64 & u64))
+  (new_msgs : betree_list_t (u64 & betree_message_t)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
+  =
+  begin match new_msgs with
+  | BetreeListCons new_msg new_msgs_tl ->
+    let (i, m) = new_msg in
+    let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
+    betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
+  | BetreeListNil -> Return bindings
+  end
+
+(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+let rec betree_internal_flush_fwd
+  (self : betree_internal_t) (params : betree_params_t)
+  (node_id_cnt : betree_node_id_counter_t)
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
+  Tot (result (state & (betree_list_t (u64 & betree_message_t))))
+  (decreases (
+    betree_internal_flush_decreases self params node_id_cnt content st))
+  =
+  let* p =
+    betree_list_partition_at_pivot_fwd betree_message_t content
+      self.betree_internal_pivot in
+  let (msgs_left, msgs_right) = p in
+  let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
+  if len_left >= params.betree_params_min_flush_size
+  then
+    let* (st0, _) =
+      betree_node_apply_messages_fwd self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* (_, node_id_cnt0) =
+      betree_node_apply_messages_back self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
+    if len_right >= params.betree_params_min_flush_size
+    then
+      let* (st1, _) =
+        betree_node_apply_messages_fwd self.betree_internal_right params
+          node_id_cnt0 msgs_right st0 in
+      let* _ =
+        betree_node_apply_messages_back self.betree_internal_right params
+          node_id_cnt0 msgs_right st0 in
+      Return (st1, BetreeListNil)
+    else Return (st0, msgs_right)
+  else
+    let* (st0, _) =
+      betree_node_apply_messages_fwd self.betree_internal_right params
+        node_id_cnt msgs_right st in
+    let* _ =
+      betree_node_apply_messages_back self.betree_internal_right params
+        node_id_cnt msgs_right st in
+    Return (st0, msgs_left)
+
+(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+and betree_internal_flush_back
+  (self : betree_internal_t) (params : betree_params_t)
+  (node_id_cnt : betree_node_id_counter_t)
+  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
+  Tot (result (betree_internal_t & betree_node_id_counter_t))
+  (decreases (
+    betree_internal_flush_decreases self params node_id_cnt content st))
+  =
+  let* p =
+    betree_list_partition_at_pivot_fwd betree_message_t content
+      self.betree_internal_pivot in
+  let (msgs_left, msgs_right) = p in
+  let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
+  if len_left >= params.betree_params_min_flush_size
+  then
+    let* (st0, _) =
+      betree_node_apply_messages_fwd self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* (n, node_id_cnt0) =
+      betree_node_apply_messages_back self.betree_internal_left params
+        node_id_cnt msgs_left st in
+    let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
+    if len_right >= params.betree_params_min_flush_size
+    then
+      let* (n0, node_id_cnt1) =
+        betree_node_apply_messages_back self.betree_internal_right params
+          node_id_cnt0 msgs_right st0 in
+      Return
+        ({ self with betree_internal_left = n; betree_internal_right = n0 },
+        node_id_cnt1)
+    else Return ({ self with betree_internal_left = n }, node_id_cnt0)
+  else
+    let* (n, node_id_cnt0) =
+      betree_node_apply_messages_back self.betree_internal_right params
+        node_id_cnt msgs_right st in
+    Return ({ self with betree_internal_right = n }, node_id_cnt0)
+
 (** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
-let rec betree_node_apply_messages_fwd
+and betree_node_apply_messages_fwd
   (self : betree_node_t) (params : betree_params_t)
   (node_id_cnt : betree_node_id_counter_t)
   (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
@@ -794,86 +874,6 @@ and betree_node_apply_messages_back
       Return (BetreeNodeLeaf { node with betree_leaf_size = len }, node_id_cnt)
   end
 
-(** [betree_main::betree::Internal::{4}::flush]: forward function *)
-and betree_internal_flush_fwd
-  (self : betree_internal_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (state & (betree_list_t (u64 & betree_message_t))))
-  (decreases (
-    betree_internal_flush_decreases self params node_id_cnt content st))
-  =
-  let* p =
-    betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot in
-  let (msgs_left, msgs_right) = p in
-  let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
-  if len_left >= params.betree_params_min_flush_size
-  then
-    let* (st0, _) =
-      betree_node_apply_messages_fwd self.betree_internal_left params
-        node_id_cnt msgs_left st in
-    let* (_, node_id_cnt0) =
-      betree_node_apply_messages_back self.betree_internal_left params
-        node_id_cnt msgs_left st in
-    let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
-    if len_right >= params.betree_params_min_flush_size
-    then
-      let* (st1, _) =
-        betree_node_apply_messages_fwd self.betree_internal_right params
-          node_id_cnt0 msgs_right st0 in
-      let* _ =
-        betree_node_apply_messages_back self.betree_internal_right params
-          node_id_cnt0 msgs_right st0 in
-      Return (st1, BetreeListNil)
-    else Return (st0, msgs_right)
-  else
-    let* (st0, _) =
-      betree_node_apply_messages_fwd self.betree_internal_right params
-        node_id_cnt msgs_right st in
-    let* _ =
-      betree_node_apply_messages_back self.betree_internal_right params
-        node_id_cnt msgs_right st in
-    Return (st0, msgs_left)
-
-(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
-and betree_internal_flush_back
-  (self : betree_internal_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (betree_internal_t & betree_node_id_counter_t))
-  (decreases (
-    betree_internal_flush_decreases self params node_id_cnt content st))
-  =
-  let* p =
-    betree_list_partition_at_pivot_fwd betree_message_t content
-      self.betree_internal_pivot in
-  let (msgs_left, msgs_right) = p in
-  let* len_left = betree_list_len_fwd (u64 & betree_message_t) msgs_left in
-  if len_left >= params.betree_params_min_flush_size
-  then
-    let* (st0, _) =
-      betree_node_apply_messages_fwd self.betree_internal_left params
-        node_id_cnt msgs_left st in
-    let* (n, node_id_cnt0) =
-      betree_node_apply_messages_back self.betree_internal_left params
-        node_id_cnt msgs_left st in
-    let* len_right = betree_list_len_fwd (u64 & betree_message_t) msgs_right in
-    if len_right >= params.betree_params_min_flush_size
-    then
-      let* (n0, node_id_cnt1) =
-        betree_node_apply_messages_back self.betree_internal_right params
-          node_id_cnt0 msgs_right st0 in
-      Return
-        ({ self with betree_internal_left = n; betree_internal_right = n0 },
-        node_id_cnt1)
-    else Return ({ self with betree_internal_left = n }, node_id_cnt0)
-  else
-    let* (n, node_id_cnt0) =
-      betree_node_apply_messages_back self.betree_internal_right params
-        node_id_cnt msgs_right st in
-    Return ({ self with betree_internal_right = n }, node_id_cnt0)
-
 (** [betree_main::betree::Node::{5}::apply]: forward function *)
 let betree_node_apply_fwd
   (self : betree_node_t) (params : betree_params_t)
diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fsti
index aad9cb43..a937c726 100644
--- a/tests/fstar/betree/BetreeMain.Types.fsti
+++ b/tests/fstar/betree/BetreeMain.Types.fsti
@@ -24,13 +24,8 @@ type betree_message_t =
 (** [betree_main::betree::Leaf] *)
 type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; }
 
-(** [betree_main::betree::Node] *)
-type betree_node_t =
-| BetreeNodeInternal : betree_internal_t -> betree_node_t
-| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
-
 (** [betree_main::betree::Internal] *)
-and betree_internal_t =
+type betree_internal_t =
 {
   betree_internal_id : u64;
   betree_internal_pivot : u64;
@@ -38,6 +33,11 @@ and betree_internal_t =
   betree_internal_right : betree_node_t;
 }
 
+(** [betree_main::betree::Node] *)
+and betree_node_t =
+| BetreeNodeInternal : betree_internal_t -> betree_node_t
+| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
+
 (** [betree_main::betree::Params] *)
 type betree_params_t =
 {
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
index 5a9776ab..823df03a 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
@@ -23,12 +23,6 @@ let betree_list_partition_at_pivot_decreases (t : Type0)
   (self : betree_list_t (u64 & t)) (pivot : u64) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
-
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
 unfold
 let betree_node_lookup_first_message_for_key_decreases (key : u64)
@@ -42,10 +36,10 @@ let betree_node_apply_upserts_decreases
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
 unfold
-let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
-  (st : state) : nat =
+let betree_node_lookup_in_bindings_decreases (key : u64)
+  (bindings : betree_list_t (u64 & u64)) : nat =
   admit ()
 
 (** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
@@ -54,17 +48,10 @@ let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
-unfold
-let betree_node_lookup_mut_in_bindings_decreases (key : u64)
-  (bindings : betree_list_t (u64 & u64)) : nat =
-  admit ()
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
 unfold
-let betree_node_apply_messages_to_leaf_decreases
-  (bindings : betree_list_t (u64 & u64))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
+let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
+  (st : state) : nat =
   admit ()
 
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
@@ -86,11 +73,17 @@ let betree_node_apply_messages_to_internal_decreases
   (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
 unfold
-let betree_node_apply_messages_decreases (self : betree_node_t)
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
+let betree_node_lookup_mut_in_bindings_decreases (key : u64)
+  (bindings : betree_list_t (u64 & u64)) : nat =
+  admit ()
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases clause *)
+unfold
+let betree_node_apply_messages_to_leaf_decreases
+  (bindings : betree_list_t (u64 & u64))
+  (new_msgs : betree_list_t (u64 & betree_message_t)) : nat =
   admit ()
 
 (** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
@@ -100,3 +93,10 @@ let betree_internal_flush_decreases (self : betree_internal_t)
   (content : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
   admit ()
 
+(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+unfold
+let betree_node_apply_messages_decreases (self : betree_node_t)
+  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
+  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat =
+  admit ()
+
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 12402fb4..be8ac438 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -261,24 +261,6 @@ let betree_leaf_split_back2
   let* node_id_cnt1 = betree_node_id_counter_fresh_id_back node_id_cnt0 in
   Return (st0, node_id_cnt1)
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
-let rec betree_node_lookup_in_bindings_fwd
-  (key : u64) (bindings : betree_list_t (u64 & u64)) :
-  Tot (result (option u64))
-  (decreases (betree_node_lookup_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i = key
-    then Return (Some i0)
-    else
-      if i > key
-      then Return None
-      else betree_node_lookup_in_bindings_fwd key tl
-  | BetreeListNil -> Return None
-  end
-
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
 let rec betree_node_lookup_first_message_for_key_fwd
   (key : u64) (msgs : betree_list_t (u64 & betree_message_t)) :
@@ -367,8 +349,52 @@ let rec betree_node_apply_upserts_back
         BetreeMessageInsert v) in
     Return (st0, msgs0)
 
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+let rec betree_node_lookup_in_bindings_fwd
+  (key : u64) (bindings : betree_list_t (u64 & u64)) :
+  Tot (result (option u64))
+  (decreases (betree_node_lookup_in_bindings_decreases key bindings))
+  =
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i = key
+    then Return (Some i0)
+    else
+      if i > key
+      then Return None
+      else betree_node_lookup_in_bindings_fwd key tl
+  | BetreeListNil -> Return None
+  end
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+let rec betree_internal_lookup_in_children_fwd
+  (self : betree_internal_t) (key : u64) (st : state) :
+  Tot (result (state & (option u64)))
+  (decreases (betree_internal_lookup_in_children_decreases self key st))
+  =
+  if key < self.betree_internal_pivot
+  then betree_node_lookup_fwd self.betree_internal_left key st
+  else betree_node_lookup_fwd self.betree_internal_right key st
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+and betree_internal_lookup_in_children_back
+  (self : betree_internal_t) (key : u64) (st : state) (st0 : state) :
+  Tot (result (state & betree_internal_t))
+  (decreases (betree_internal_lookup_in_children_decreases self key st))
+  =
+  if key < self.betree_internal_pivot
+  then
+    let* (st1, n) =
+      betree_node_lookup_back self.betree_internal_left key st st0 in
+    Return (st1, { self with betree_internal_left = n })
+  else
+    let* (st1, n) =
+      betree_node_lookup_back self.betree_internal_right key st st0 in
+    Return (st1, { self with betree_internal_right = n })
+
 (** [betree_main::betree::Node::{5}::lookup]: forward function *)
-let rec betree_node_lookup_fwd
+and betree_node_lookup_fwd
   (self : betree_node_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
   (decreases (betree_node_lookup_decreases self key st))
@@ -496,125 +522,6 @@ and betree_node_lookup_back
     Return (st0, BetreeNodeLeaf node)
   end
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
-and betree_internal_lookup_in_children_fwd
-  (self : betree_internal_t) (key : u64) (st : state) :
-  Tot (result (state & (option u64)))
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then betree_node_lookup_fwd self.betree_internal_left key st
-  else betree_node_lookup_fwd self.betree_internal_right key st
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
-and betree_internal_lookup_in_children_back
-  (self : betree_internal_t) (key : u64) (st : state) (st0 : state) :
-  Tot (result (state & betree_internal_t))
-  (decreases (betree_internal_lookup_in_children_decreases self key st))
-  =
-  if key < self.betree_internal_pivot
-  then
-    let* (st1, n) =
-      betree_node_lookup_back self.betree_internal_left key st st0 in
-    Return (st1, { self with betree_internal_left = n })
-  else
-    let* (st1, n) =
-      betree_node_lookup_back self.betree_internal_right key st st0 in
-    Return (st1, { self with betree_internal_right = n })
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
-let rec betree_node_lookup_mut_in_bindings_fwd
-  (key : u64) (bindings : betree_list_t (u64 & u64)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return (BetreeListCons (i, i0) tl)
-    else betree_node_lookup_mut_in_bindings_fwd key tl
-  | BetreeListNil -> Return BetreeListNil
-  end
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
-let rec betree_node_lookup_mut_in_bindings_back
-  (key : u64) (bindings : betree_list_t (u64 & u64))
-  (ret : betree_list_t (u64 & u64)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | BetreeListCons hd tl ->
-    let (i, i0) = hd in
-    if i >= key
-    then Return ret
-    else
-      let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
-      Return (BetreeListCons (i, i0) tl0)
-  | BetreeListNil -> Return ret
-  end
-
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
-let betree_node_apply_to_leaf_fwd_back
-  (bindings : betree_list_t (u64 & u64)) (key : u64)
-  (new_msg : betree_message_t) :
-  result (betree_list_t (u64 & u64))
-  =
-  let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
-  let* b = betree_list_head_has_key_fwd u64 bindings0 key in
-  if b
-  then
-    let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
-    begin match new_msg with
-    | BetreeMessageInsert v ->
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      let* bindings2 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    | BetreeMessageDelete ->
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    | BetreeMessageUpsert s ->
-      let (_, i) = hd in
-      let* v = betree_upsert_update_fwd (Some i) s in
-      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
-      let* bindings2 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings2
-    end
-  else
-    begin match new_msg with
-    | BetreeMessageInsert v ->
-      let* bindings1 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    | BetreeMessageDelete ->
-      betree_node_lookup_mut_in_bindings_back key bindings bindings0
-    | BetreeMessageUpsert s ->
-      let* v = betree_upsert_update_fwd None s in
-      let* bindings1 =
-        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
-      betree_node_lookup_mut_in_bindings_back key bindings bindings1
-    end
-
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
-let rec betree_node_apply_messages_to_leaf_fwd_back
-  (bindings : betree_list_t (u64 & u64))
-  (new_msgs : betree_list_t (u64 & betree_message_t)) :
-  Tot (result (betree_list_t (u64 & u64)))
-  (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
-  =
-  begin match new_msgs with
-  | BetreeListCons new_msg new_msgs_tl ->
-    let (i, m) = new_msg in
-    let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
-    betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
-  | BetreeListNil -> Return bindings
-  end
-
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec betree_node_filter_messages_for_key_fwd_back
@@ -746,157 +653,101 @@ let rec betree_node_apply_messages_to_internal_fwd_back
   | BetreeListNil -> Return msgs
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
-let rec betree_node_apply_messages_fwd
-  (self : betree_node_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
-  Tot (result (state & unit))
-  (decreases (
-    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+let rec betree_node_lookup_mut_in_bindings_fwd
+  (key : u64) (bindings : betree_list_t (u64 & u64)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
   =
-  begin match self with
-  | BetreeNodeInternal node ->
-    let* (st0, content) =
-      betree_load_internal_node_fwd node.betree_internal_id st in
-    let* content0 =
-      betree_node_apply_messages_to_internal_fwd_back content msgs in
-    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
-    if num_msgs >= params.betree_params_min_flush_size
-    then
-      let* (st1, content1) =
-        betree_internal_flush_fwd node params node_id_cnt content0 st0 in
-      let* (st2, (node0, _)) =
-        betree_internal_flush_back'a node params node_id_cnt content0 st0 st1
-        in
-      let* (st3, _) =
-        betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in
-      Return (st3, ())
-    else
-      let* (st1, _) =
-        betree_store_internal_node_fwd node.betree_internal_id content0 st0 in
-      Return (st1, ())
-  | BetreeNodeLeaf node ->
-    let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
-    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
-    let* len = betree_list_len_fwd (u64 & u64) content0 in
-    let* i = u64_mul 2 params.betree_params_split_size in
-    if len >= i
-    then
-      let* (st1, _) =
-        betree_leaf_split_fwd node content0 params node_id_cnt st0 in
-      let* (st2, _) =
-        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in
-      betree_leaf_split_back0 node content0 params node_id_cnt st0 st2
-    else
-      let* (st1, _) =
-        betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
-      Return (st1, ())
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i >= key
+    then Return (BetreeListCons (i, i0) tl)
+    else betree_node_lookup_mut_in_bindings_fwd key tl
+  | BetreeListNil -> Return BetreeListNil
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
-and betree_node_apply_messages_back'a
-  (self : betree_node_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
-  Tot (result (state & (betree_node_t & betree_node_id_counter_t)))
-  (decreases (
-    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+let rec betree_node_lookup_mut_in_bindings_back
+  (key : u64) (bindings : betree_list_t (u64 & u64))
+  (ret : betree_list_t (u64 & u64)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_lookup_mut_in_bindings_decreases key bindings))
   =
-  begin match self with
-  | BetreeNodeInternal node ->
-    let* (st1, content) =
-      betree_load_internal_node_fwd node.betree_internal_id st in
-    let* content0 =
-      betree_node_apply_messages_to_internal_fwd_back content msgs in
-    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
-    if num_msgs >= params.betree_params_min_flush_size
-    then
-      let* (st2, content1) =
-        betree_internal_flush_fwd node params node_id_cnt content0 st1 in
-      let* (st3, (node0, node_id_cnt0)) =
-        betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
-        in
-      let* _ =
-        betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
-      Return (st0, (BetreeNodeInternal node0, node_id_cnt0))
-    else
-      let* _ =
-        betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
-      Return (st0, (BetreeNodeInternal node, node_id_cnt))
-  | BetreeNodeLeaf node ->
-    let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
-    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
-    let* len = betree_list_len_fwd (u64 & u64) content0 in
-    let* i = u64_mul 2 params.betree_params_split_size in
-    if len >= i
-    then
-      let* (st2, new_node) =
-        betree_leaf_split_fwd node content0 params node_id_cnt st1 in
-      let* (st3, _) =
-        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
-      let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
-        in
-      let* (st4, node_id_cnt0) =
-        betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in
-      Return (st4, (BetreeNodeInternal new_node, node_id_cnt0))
+  begin match bindings with
+  | BetreeListCons hd tl ->
+    let (i, i0) = hd in
+    if i >= key
+    then Return ret
     else
-      let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
-      Return (st0, (BetreeNodeLeaf { node with betree_leaf_size = len },
-        node_id_cnt))
+      let* tl0 = betree_node_lookup_mut_in_bindings_back key tl ret in
+      Return (BetreeListCons (i, i0) tl0)
+  | BetreeListNil -> Return ret
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 1 *)
-and betree_node_apply_messages_back1
-  (self : betree_node_t) (params : betree_params_t)
-  (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
-  Tot (result (state & unit))
-  (decreases (
-    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+let betree_node_apply_to_leaf_fwd_back
+  (bindings : betree_list_t (u64 & u64)) (key : u64)
+  (new_msg : betree_message_t) :
+  result (betree_list_t (u64 & u64))
   =
-  begin match self with
-  | BetreeNodeInternal node ->
-    let* (st1, content) =
-      betree_load_internal_node_fwd node.betree_internal_id st in
-    let* content0 =
-      betree_node_apply_messages_to_internal_fwd_back content msgs in
-    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
-    if num_msgs >= params.betree_params_min_flush_size
-    then
-      let* (st2, content1) =
-        betree_internal_flush_fwd node params node_id_cnt content0 st1 in
-      let* (st3, (node0, _)) =
-        betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
-        in
-      let* _ =
-        betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
-      betree_internal_flush_back1 node params node_id_cnt content0 st1 st0
-    else
-      let* _ =
-        betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
-      Return (st0, ())
-  | BetreeNodeLeaf node ->
-    let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
-    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
-    let* len = betree_list_len_fwd (u64 & u64) content0 in
-    let* i = u64_mul 2 params.betree_params_split_size in
-    if len >= i
-    then
-      let* (st2, _) =
-        betree_leaf_split_fwd node content0 params node_id_cnt st1 in
-      let* (st3, _) =
-        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
-      let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
-        in
-      betree_leaf_split_back1 node content0 params node_id_cnt st1 st0
-    else
-      let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
-      Return (st0, ())
+  let* bindings0 = betree_node_lookup_mut_in_bindings_fwd key bindings in
+  let* b = betree_list_head_has_key_fwd u64 bindings0 key in
+  if b
+  then
+    let* hd = betree_list_pop_front_fwd (u64 & u64) bindings0 in
+    begin match new_msg with
+    | BetreeMessageInsert v ->
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      let* bindings2 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings2
+    | BetreeMessageDelete ->
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    | BetreeMessageUpsert s ->
+      let (_, i) = hd in
+      let* v = betree_upsert_update_fwd (Some i) s in
+      let* bindings1 = betree_list_pop_front_back (u64 & u64) bindings0 in
+      let* bindings2 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings2
+    end
+  else
+    begin match new_msg with
+    | BetreeMessageInsert v ->
+      let* bindings1 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    | BetreeMessageDelete ->
+      betree_node_lookup_mut_in_bindings_back key bindings bindings0
+    | BetreeMessageUpsert s ->
+      let* v = betree_upsert_update_fwd None s in
+      let* bindings1 =
+        betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) in
+      betree_node_lookup_mut_in_bindings_back key bindings bindings1
+    end
+
+(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ()) *)
+let rec betree_node_apply_messages_to_leaf_fwd_back
+  (bindings : betree_list_t (u64 & u64))
+  (new_msgs : betree_list_t (u64 & betree_message_t)) :
+  Tot (result (betree_list_t (u64 & u64)))
+  (decreases (betree_node_apply_messages_to_leaf_decreases bindings new_msgs))
+  =
+  begin match new_msgs with
+  | BetreeListCons new_msg new_msgs_tl ->
+    let (i, m) = new_msg in
+    let* bindings0 = betree_node_apply_to_leaf_fwd_back bindings i m in
+    betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
+  | BetreeListNil -> Return bindings
   end
 
 (** [betree_main::betree::Internal::{4}::flush]: forward function *)
-and betree_internal_flush_fwd
+let rec betree_internal_flush_fwd
   (self : betree_internal_t) (params : betree_params_t)
   (node_id_cnt : betree_node_id_counter_t)
   (content : betree_list_t (u64 & betree_message_t)) (st : state) :
@@ -1052,6 +903,155 @@ and betree_internal_flush_back1
         node_id_cnt msgs_right st st2 in
     Return (st0, ())
 
+(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
+and betree_node_apply_messages_fwd
+  (self : betree_node_t) (params : betree_params_t)
+  (node_id_cnt : betree_node_id_counter_t)
+  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
+  Tot (result (state & unit))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+  =
+  begin match self with
+  | BetreeNodeInternal node ->
+    let* (st0, content) =
+      betree_load_internal_node_fwd node.betree_internal_id st in
+    let* content0 =
+      betree_node_apply_messages_to_internal_fwd_back content msgs in
+    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
+    if num_msgs >= params.betree_params_min_flush_size
+    then
+      let* (st1, content1) =
+        betree_internal_flush_fwd node params node_id_cnt content0 st0 in
+      let* (st2, (node0, _)) =
+        betree_internal_flush_back'a node params node_id_cnt content0 st0 st1
+        in
+      let* (st3, _) =
+        betree_store_internal_node_fwd node0.betree_internal_id content1 st2 in
+      Return (st3, ())
+    else
+      let* (st1, _) =
+        betree_store_internal_node_fwd node.betree_internal_id content0 st0 in
+      Return (st1, ())
+  | BetreeNodeLeaf node ->
+    let* (st0, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
+    let* len = betree_list_len_fwd (u64 & u64) content0 in
+    let* i = u64_mul 2 params.betree_params_split_size in
+    if len >= i
+    then
+      let* (st1, _) =
+        betree_leaf_split_fwd node content0 params node_id_cnt st0 in
+      let* (st2, _) =
+        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st1 in
+      betree_leaf_split_back0 node content0 params node_id_cnt st0 st2
+    else
+      let* (st1, _) =
+        betree_store_leaf_node_fwd node.betree_leaf_id content0 st0 in
+      Return (st1, ())
+  end
+
+(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
+and betree_node_apply_messages_back'a
+  (self : betree_node_t) (params : betree_params_t)
+  (node_id_cnt : betree_node_id_counter_t)
+  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
+  Tot (result (state & (betree_node_t & betree_node_id_counter_t)))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+  =
+  begin match self with
+  | BetreeNodeInternal node ->
+    let* (st1, content) =
+      betree_load_internal_node_fwd node.betree_internal_id st in
+    let* content0 =
+      betree_node_apply_messages_to_internal_fwd_back content msgs in
+    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
+    if num_msgs >= params.betree_params_min_flush_size
+    then
+      let* (st2, content1) =
+        betree_internal_flush_fwd node params node_id_cnt content0 st1 in
+      let* (st3, (node0, node_id_cnt0)) =
+        betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
+        in
+      let* _ =
+        betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
+      Return (st0, (BetreeNodeInternal node0, node_id_cnt0))
+    else
+      let* _ =
+        betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
+      Return (st0, (BetreeNodeInternal node, node_id_cnt))
+  | BetreeNodeLeaf node ->
+    let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
+    let* len = betree_list_len_fwd (u64 & u64) content0 in
+    let* i = u64_mul 2 params.betree_params_split_size in
+    if len >= i
+    then
+      let* (st2, new_node) =
+        betree_leaf_split_fwd node content0 params node_id_cnt st1 in
+      let* (st3, _) =
+        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
+      let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
+        in
+      let* (st4, node_id_cnt0) =
+        betree_leaf_split_back2 node content0 params node_id_cnt st1 st0 in
+      Return (st4, (BetreeNodeInternal new_node, node_id_cnt0))
+    else
+      let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
+      Return (st0, (BetreeNodeLeaf { node with betree_leaf_size = len },
+        node_id_cnt))
+  end
+
+(** [betree_main::betree::Node::{5}::apply_messages]: backward function 1 *)
+and betree_node_apply_messages_back1
+  (self : betree_node_t) (params : betree_params_t)
+  (node_id_cnt : betree_node_id_counter_t)
+  (msgs : betree_list_t (u64 & betree_message_t)) (st : state) (st0 : state) :
+  Tot (result (state & unit))
+  (decreases (
+    betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+  =
+  begin match self with
+  | BetreeNodeInternal node ->
+    let* (st1, content) =
+      betree_load_internal_node_fwd node.betree_internal_id st in
+    let* content0 =
+      betree_node_apply_messages_to_internal_fwd_back content msgs in
+    let* num_msgs = betree_list_len_fwd (u64 & betree_message_t) content0 in
+    if num_msgs >= params.betree_params_min_flush_size
+    then
+      let* (st2, content1) =
+        betree_internal_flush_fwd node params node_id_cnt content0 st1 in
+      let* (st3, (node0, _)) =
+        betree_internal_flush_back'a node params node_id_cnt content0 st1 st2
+        in
+      let* _ =
+        betree_store_internal_node_fwd node0.betree_internal_id content1 st3 in
+      betree_internal_flush_back1 node params node_id_cnt content0 st1 st0
+    else
+      let* _ =
+        betree_store_internal_node_fwd node.betree_internal_id content0 st1 in
+      Return (st0, ())
+  | BetreeNodeLeaf node ->
+    let* (st1, content) = betree_load_leaf_node_fwd node.betree_leaf_id st in
+    let* content0 = betree_node_apply_messages_to_leaf_fwd_back content msgs in
+    let* len = betree_list_len_fwd (u64 & u64) content0 in
+    let* i = u64_mul 2 params.betree_params_split_size in
+    if len >= i
+    then
+      let* (st2, _) =
+        betree_leaf_split_fwd node content0 params node_id_cnt st1 in
+      let* (st3, _) =
+        betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil st2 in
+      let* _ = betree_leaf_split_back0 node content0 params node_id_cnt st1 st3
+        in
+      betree_leaf_split_back1 node content0 params node_id_cnt st1 st0
+    else
+      let* _ = betree_store_leaf_node_fwd node.betree_leaf_id content0 st1 in
+      Return (st0, ())
+  end
+
 (** [betree_main::betree::Node::{5}::apply]: forward function *)
 let betree_node_apply_fwd
   (self : betree_node_t) (params : betree_params_t)
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
index aad9cb43..a937c726 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti
@@ -24,13 +24,8 @@ type betree_message_t =
 (** [betree_main::betree::Leaf] *)
 type betree_leaf_t = { betree_leaf_id : u64; betree_leaf_size : u64; }
 
-(** [betree_main::betree::Node] *)
-type betree_node_t =
-| BetreeNodeInternal : betree_internal_t -> betree_node_t
-| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
-
 (** [betree_main::betree::Internal] *)
-and betree_internal_t =
+type betree_internal_t =
 {
   betree_internal_id : u64;
   betree_internal_pivot : u64;
@@ -38,6 +33,11 @@ and betree_internal_t =
   betree_internal_right : betree_node_t;
 }
 
+(** [betree_main::betree::Node] *)
+and betree_node_t =
+| BetreeNodeInternal : betree_internal_t -> betree_node_t
+| BetreeNodeLeaf : betree_leaf_t -> betree_node_t
+
 (** [betree_main::betree::Params] *)
 type betree_params_t =
 {
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index d790bfa9..2cdd6e21 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -202,16 +202,16 @@ let _ = assert_norm (choose_test_fwd = Return ())
 let test_char_fwd : result char =
   Return 'a'
 
-(** [no_nested_borrows::NodeElem] *)
-type node_elem_t (t : Type0) =
-| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
-| NodeElemNil : node_elem_t t
-
 (** [no_nested_borrows::Tree] *)
-and tree_t (t : Type0) =
+type tree_t (t : Type0) =
 | TreeLeaf : t -> tree_t t
 | TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t
 
+(** [no_nested_borrows::NodeElem] *)
+and node_elem_t (t : Type0) =
+| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
+| NodeElemNil : node_elem_t t
+
 (** [no_nested_borrows::list_length]: forward function *)
 let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
   begin match l with
diff --git a/tests/hol4/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betreeMain_FunsScript.sml
index 03ff2671..b53c7b8d 100644
--- a/tests/hol4/betree/betreeMain_FunsScript.sml
+++ b/tests/hol4/betree/betreeMain_FunsScript.sml
@@ -279,22 +279,6 @@ val betree_leaf_split_back_def = Define ‘
     od
 ’
 
-val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘
-  (** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
-  betree_node_lookup_in_bindings_fwd
-    (key : u64) (bindings : (u64 # u64) betree_list_t) : u64 option result =
-    (case bindings of
-    | BetreeListCons hd tl =>
-      let (i, i0) = hd in
-      if i = key
-      then Return (SOME i0)
-      else
-        if u64_gt i key
-        then Return NONE
-        else betree_node_lookup_in_bindings_fwd key tl
-    | BetreeListNil => Return NONE)
-’
-
 val [betree_node_lookup_first_message_for_key_fwd_def] = DefineDiv ‘
   (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
   betree_node_lookup_first_message_for_key_fwd
@@ -396,7 +380,51 @@ val [betree_node_apply_upserts_back_def] = DefineDiv ‘
     od
 ’
 
-val [betree_node_lookup_fwd_def, betree_node_lookup_back_def, betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_children_back_def] = DefineDiv ‘
+val [betree_node_lookup_in_bindings_fwd_def] = DefineDiv ‘
+  (** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+  betree_node_lookup_in_bindings_fwd
+    (key : u64) (bindings : (u64 # u64) betree_list_t) : u64 option result =
+    (case bindings of
+    | BetreeListCons hd tl =>
+      let (i, i0) = hd in
+      if i = key
+      then Return (SOME i0)
+      else
+        if u64_gt i key
+        then Return NONE
+        else betree_node_lookup_in_bindings_fwd key tl
+    | BetreeListNil => Return NONE)
+’
+
+val [betree_internal_lookup_in_children_fwd_def, betree_internal_lookup_in_children_back_def, betree_node_lookup_fwd_def, betree_node_lookup_back_def] = DefineDiv ‘
+  (** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+  (betree_internal_lookup_in_children_fwd
+     (self : betree_internal_t) (key : u64) (st : state) :
+     (state # u64 option) result
+     =
+    if u64_lt key self.betree_internal_pivot
+    then betree_node_lookup_fwd self.betree_internal_left key st
+    else betree_node_lookup_fwd self.betree_internal_right key st)
+  /\
+  
+  (** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+  (betree_internal_lookup_in_children_back
+     (self : betree_internal_t) (key : u64) (st : state) :
+     betree_internal_t result
+     =
+    if u64_lt key self.betree_internal_pivot
+    then (
+      do
+      n <- betree_node_lookup_back self.betree_internal_left key st;
+      Return (self with <| betree_internal_left := n |>)
+      od)
+    else (
+      do
+      n <- betree_node_lookup_back self.betree_internal_right key st;
+      Return (self with <| betree_internal_right := n |>)
+      od))
+  /\
+  
   (** [betree_main::betree::Node::{5}::lookup]: forward function *)
   (betree_node_lookup_fwd
      (self : betree_node_t) (key : u64) (st : state) :
@@ -468,8 +496,8 @@ val [betree_node_lookup_fwd_def, betree_node_lookup_back_def, betree_internal_lo
   /\
   
   (** [betree_main::betree::Node::{5}::lookup]: backward function 0 *)
-  (betree_node_lookup_back
-     (self : betree_node_t) (key : u64) (st : state) : betree_node_t result =
+  betree_node_lookup_back
+    (self : betree_node_t) (key : u64) (st : state) : betree_node_t result =
     (case self of
     | BetreeNodeInternal node =>
       do
@@ -532,142 +560,7 @@ val [betree_node_lookup_fwd_def, betree_node_lookup_back_def, betree_internal_lo
       (_, bindings) <- betree_load_leaf_node_fwd node.betree_leaf_id st;
       _ <- betree_node_lookup_in_bindings_fwd key bindings;
       Return (BetreeNodeLeaf node)
-      od))
-  /\
-  
-  (** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
-  (betree_internal_lookup_in_children_fwd
-     (self : betree_internal_t) (key : u64) (st : state) :
-     (state # u64 option) result
-     =
-    if u64_lt key self.betree_internal_pivot
-    then betree_node_lookup_fwd self.betree_internal_left key st
-    else betree_node_lookup_fwd self.betree_internal_right key st)
-  /\
-  
-  (** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
-  betree_internal_lookup_in_children_back
-    (self : betree_internal_t) (key : u64) (st : state) :
-    betree_internal_t result
-    =
-    if u64_lt key self.betree_internal_pivot
-    then (
-      do
-      n <- betree_node_lookup_back self.betree_internal_left key st;
-      Return (self with <| betree_internal_left := n |>)
       od)
-    else (
-      do
-      n <- betree_node_lookup_back self.betree_internal_right key st;
-      Return (self with <| betree_internal_right := n |>)
-      od)
-’
-
-val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘
-  (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
-  betree_node_lookup_mut_in_bindings_fwd
-    (key : u64) (bindings : (u64 # u64) betree_list_t) :
-    (u64 # u64) betree_list_t result
-    =
-    (case bindings of
-    | BetreeListCons hd tl =>
-      let (i, i0) = hd in
-      if u64_ge i key
-      then Return (BetreeListCons (i, i0) tl)
-      else betree_node_lookup_mut_in_bindings_fwd key tl
-    | BetreeListNil => Return BetreeListNil)
-’
-
-val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘
-  (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
-  betree_node_lookup_mut_in_bindings_back
-    (key : u64) (bindings : (u64 # u64) betree_list_t)
-    (ret : (u64 # u64) betree_list_t) :
-    (u64 # u64) betree_list_t result
-    =
-    (case bindings of
-    | BetreeListCons hd tl =>
-      let (i, i0) = hd in
-      if u64_ge i key
-      then Return ret
-      else (
-        do
-        tl0 <- betree_node_lookup_mut_in_bindings_back key tl ret;
-        Return (BetreeListCons (i, i0) tl0)
-        od)
-    | BetreeListNil => Return ret)
-’
-
-val betree_node_apply_to_leaf_fwd_back_def = Define ‘
-  (** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  betree_node_apply_to_leaf_fwd_back
-    (bindings : (u64 # u64) betree_list_t) (key : u64)
-    (new_msg : betree_message_t) :
-    (u64 # u64) betree_list_t result
-    =
-    do
-    bindings0 <- betree_node_lookup_mut_in_bindings_fwd key bindings;
-    b <- betree_list_head_has_key_fwd bindings0 key;
-    if b
-    then (
-      do
-      hd <- betree_list_pop_front_fwd bindings0;
-      (case new_msg of
-      | BetreeMessageInsert v =>
-        do
-        bindings1 <- betree_list_pop_front_back bindings0;
-        bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v);
-        betree_node_lookup_mut_in_bindings_back key bindings bindings2
-        od
-      | BetreeMessageDelete =>
-        do
-        bindings1 <- betree_list_pop_front_back bindings0;
-        betree_node_lookup_mut_in_bindings_back key bindings bindings1
-        od
-      | BetreeMessageUpsert s =>
-        let (_, i) = hd in
-        do
-        v <- betree_upsert_update_fwd (SOME i) s;
-        bindings1 <- betree_list_pop_front_back bindings0;
-        bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v);
-        betree_node_lookup_mut_in_bindings_back key bindings bindings2
-        od)
-      od)
-    else
-      (case new_msg of
-      | BetreeMessageInsert v =>
-        do
-        bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v);
-        betree_node_lookup_mut_in_bindings_back key bindings bindings1
-        od
-      | BetreeMessageDelete =>
-        betree_node_lookup_mut_in_bindings_back key bindings bindings0
-      | BetreeMessageUpsert s =>
-        do
-        v <- betree_upsert_update_fwd NONE s;
-        bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v);
-        betree_node_lookup_mut_in_bindings_back key bindings bindings1
-        od)
-    od
-’
-
-val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘
-  (** [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_node_apply_messages_to_leaf_fwd_back
-    (bindings : (u64 # u64) betree_list_t)
-    (new_msgs : (u64 # betree_message_t) betree_list_t) :
-    (u64 # u64) betree_list_t result
-    =
-    (case new_msgs of
-    | BetreeListCons new_msg new_msgs_tl =>
-      let (i, m) = new_msg in
-      do
-      bindings0 <- betree_node_apply_to_leaf_fwd_back bindings i m;
-      betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
-      od
-    | BetreeListNil => Return bindings)
 ’
 
 val [betree_node_filter_messages_for_key_fwd_back_def] = DefineDiv ‘
@@ -811,7 +704,211 @@ val [betree_node_apply_messages_to_internal_fwd_back_def] = DefineDiv ‘
     | BetreeListNil => Return msgs)
 ’
 
-val [betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def, betree_internal_flush_fwd_def, betree_internal_flush_back_def] = DefineDiv ‘
+val [betree_node_lookup_mut_in_bindings_fwd_def] = DefineDiv ‘
+  (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+  betree_node_lookup_mut_in_bindings_fwd
+    (key : u64) (bindings : (u64 # u64) betree_list_t) :
+    (u64 # u64) betree_list_t result
+    =
+    (case bindings of
+    | BetreeListCons hd tl =>
+      let (i, i0) = hd in
+      if u64_ge i key
+      then Return (BetreeListCons (i, i0) tl)
+      else betree_node_lookup_mut_in_bindings_fwd key tl
+    | BetreeListNil => Return BetreeListNil)
+’
+
+val [betree_node_lookup_mut_in_bindings_back_def] = DefineDiv ‘
+  (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+  betree_node_lookup_mut_in_bindings_back
+    (key : u64) (bindings : (u64 # u64) betree_list_t)
+    (ret : (u64 # u64) betree_list_t) :
+    (u64 # u64) betree_list_t result
+    =
+    (case bindings of
+    | BetreeListCons hd tl =>
+      let (i, i0) = hd in
+      if u64_ge i key
+      then Return ret
+      else (
+        do
+        tl0 <- betree_node_lookup_mut_in_bindings_back key tl ret;
+        Return (BetreeListCons (i, i0) tl0)
+        od)
+    | BetreeListNil => Return ret)
+’
+
+val betree_node_apply_to_leaf_fwd_back_def = Define ‘
+  (** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+      (there is a single backward function, and the forward function returns ()) *)
+  betree_node_apply_to_leaf_fwd_back
+    (bindings : (u64 # u64) betree_list_t) (key : u64)
+    (new_msg : betree_message_t) :
+    (u64 # u64) betree_list_t result
+    =
+    do
+    bindings0 <- betree_node_lookup_mut_in_bindings_fwd key bindings;
+    b <- betree_list_head_has_key_fwd bindings0 key;
+    if b
+    then (
+      do
+      hd <- betree_list_pop_front_fwd bindings0;
+      (case new_msg of
+      | BetreeMessageInsert v =>
+        do
+        bindings1 <- betree_list_pop_front_back bindings0;
+        bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v);
+        betree_node_lookup_mut_in_bindings_back key bindings bindings2
+        od
+      | BetreeMessageDelete =>
+        do
+        bindings1 <- betree_list_pop_front_back bindings0;
+        betree_node_lookup_mut_in_bindings_back key bindings bindings1
+        od
+      | BetreeMessageUpsert s =>
+        let (_, i) = hd in
+        do
+        v <- betree_upsert_update_fwd (SOME i) s;
+        bindings1 <- betree_list_pop_front_back bindings0;
+        bindings2 <- betree_list_push_front_fwd_back bindings1 (key, v);
+        betree_node_lookup_mut_in_bindings_back key bindings bindings2
+        od)
+      od)
+    else
+      (case new_msg of
+      | BetreeMessageInsert v =>
+        do
+        bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v);
+        betree_node_lookup_mut_in_bindings_back key bindings bindings1
+        od
+      | BetreeMessageDelete =>
+        betree_node_lookup_mut_in_bindings_back key bindings bindings0
+      | BetreeMessageUpsert s =>
+        do
+        v <- betree_upsert_update_fwd NONE s;
+        bindings1 <- betree_list_push_front_fwd_back bindings0 (key, v);
+        betree_node_lookup_mut_in_bindings_back key bindings bindings1
+        od)
+    od
+’
+
+val [betree_node_apply_messages_to_leaf_fwd_back_def] = DefineDiv ‘
+  (** [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_node_apply_messages_to_leaf_fwd_back
+    (bindings : (u64 # u64) betree_list_t)
+    (new_msgs : (u64 # betree_message_t) betree_list_t) :
+    (u64 # u64) betree_list_t result
+    =
+    (case new_msgs of
+    | BetreeListCons new_msg new_msgs_tl =>
+      let (i, m) = new_msg in
+      do
+      bindings0 <- betree_node_apply_to_leaf_fwd_back bindings i m;
+      betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl
+      od
+    | BetreeListNil => Return bindings)
+’
+
+val [betree_internal_flush_fwd_def, betree_internal_flush_back_def, betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def] = DefineDiv ‘
+  (** [betree_main::betree::Internal::{4}::flush]: forward function *)
+  (betree_internal_flush_fwd
+     (self : betree_internal_t) (params : betree_params_t)
+     (node_id_cnt : betree_node_id_counter_t)
+     (content : (u64 # betree_message_t) betree_list_t) (st : state) :
+     (state # (u64 # betree_message_t) betree_list_t) result
+     =
+    do
+    p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot;
+    let (msgs_left, msgs_right) = p in
+    do
+    len_left <- betree_list_len_fwd msgs_left;
+    if u64_ge len_left params.betree_params_min_flush_size
+    then (
+      do
+      (st0, _) <-
+        betree_node_apply_messages_fwd self.betree_internal_left params
+          node_id_cnt msgs_left st;
+      (_, node_id_cnt0) <-
+        betree_node_apply_messages_back self.betree_internal_left params
+          node_id_cnt msgs_left st;
+      len_right <- betree_list_len_fwd msgs_right;
+      if u64_ge len_right params.betree_params_min_flush_size
+      then (
+        do
+        (st1, _) <-
+          betree_node_apply_messages_fwd self.betree_internal_right params
+            node_id_cnt0 msgs_right st0;
+        _ <-
+          betree_node_apply_messages_back self.betree_internal_right params
+            node_id_cnt0 msgs_right st0;
+        Return (st1, BetreeListNil)
+        od)
+      else Return (st0, msgs_right)
+      od)
+    else (
+      do
+      (st0, _) <-
+        betree_node_apply_messages_fwd self.betree_internal_right params
+          node_id_cnt msgs_right st;
+      _ <-
+        betree_node_apply_messages_back self.betree_internal_right params
+          node_id_cnt msgs_right st;
+      Return (st0, msgs_left)
+      od)
+    od
+    od)
+  /\
+  
+  (** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+  (betree_internal_flush_back
+     (self : betree_internal_t) (params : betree_params_t)
+     (node_id_cnt : betree_node_id_counter_t)
+     (content : (u64 # betree_message_t) betree_list_t) (st : state) :
+     (betree_internal_t # betree_node_id_counter_t) result
+     =
+    do
+    p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot;
+    let (msgs_left, msgs_right) = p in
+    do
+    len_left <- betree_list_len_fwd msgs_left;
+    if u64_ge len_left params.betree_params_min_flush_size
+    then (
+      do
+      (st0, _) <-
+        betree_node_apply_messages_fwd self.betree_internal_left params
+          node_id_cnt msgs_left st;
+      (n, node_id_cnt0) <-
+        betree_node_apply_messages_back self.betree_internal_left params
+          node_id_cnt msgs_left st;
+      len_right <- betree_list_len_fwd msgs_right;
+      if u64_ge len_right params.betree_params_min_flush_size
+      then (
+        do
+        (n0, node_id_cnt1) <-
+          betree_node_apply_messages_back self.betree_internal_right params
+            node_id_cnt0 msgs_right st0;
+        Return
+          (self
+             with
+             <|
+             betree_internal_left := n; betree_internal_right := n0
+             |>, node_id_cnt1)
+        od)
+      else Return (self with <| betree_internal_left := n |>, node_id_cnt0)
+      od)
+    else (
+      do
+      (n, node_id_cnt0) <-
+        betree_node_apply_messages_back self.betree_internal_right params
+          node_id_cnt msgs_right st;
+      Return (self with <| betree_internal_right := n |>, node_id_cnt0)
+      od)
+    od
+    od)
+  /\
+  
   (** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
   (betree_node_apply_messages_fwd
      (self : betree_node_t) (params : betree_params_t)
@@ -868,12 +965,12 @@ val [betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def, be
   /\
   
   (** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
-  (betree_node_apply_messages_back
-     (self : betree_node_t) (params : betree_params_t)
-     (node_id_cnt : betree_node_id_counter_t)
-     (msgs : (u64 # betree_message_t) betree_list_t) (st : state) :
-     (betree_node_t # betree_node_id_counter_t) result
-     =
+  betree_node_apply_messages_back
+    (self : betree_node_t) (params : betree_params_t)
+    (node_id_cnt : betree_node_id_counter_t)
+    (msgs : (u64 # betree_message_t) betree_list_t) (st : state) :
+    (betree_node_t # betree_node_id_counter_t) result
+    =
     (case self of
     | BetreeNodeInternal node =>
       do
@@ -921,104 +1018,7 @@ val [betree_node_apply_messages_fwd_def, betree_node_apply_messages_back_def, be
         Return (BetreeNodeLeaf (node with <| betree_leaf_size := len |>),
           node_id_cnt)
         od)
-      od))
-  /\
-  
-  (** [betree_main::betree::Internal::{4}::flush]: forward function *)
-  (betree_internal_flush_fwd
-     (self : betree_internal_t) (params : betree_params_t)
-     (node_id_cnt : betree_node_id_counter_t)
-     (content : (u64 # betree_message_t) betree_list_t) (st : state) :
-     (state # (u64 # betree_message_t) betree_list_t) result
-     =
-    do
-    p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot;
-    let (msgs_left, msgs_right) = p in
-    do
-    len_left <- betree_list_len_fwd msgs_left;
-    if u64_ge len_left params.betree_params_min_flush_size
-    then (
-      do
-      (st0, _) <-
-        betree_node_apply_messages_fwd self.betree_internal_left params
-          node_id_cnt msgs_left st;
-      (_, node_id_cnt0) <-
-        betree_node_apply_messages_back self.betree_internal_left params
-          node_id_cnt msgs_left st;
-      len_right <- betree_list_len_fwd msgs_right;
-      if u64_ge len_right params.betree_params_min_flush_size
-      then (
-        do
-        (st1, _) <-
-          betree_node_apply_messages_fwd self.betree_internal_right params
-            node_id_cnt0 msgs_right st0;
-        _ <-
-          betree_node_apply_messages_back self.betree_internal_right params
-            node_id_cnt0 msgs_right st0;
-        Return (st1, BetreeListNil)
-        od)
-      else Return (st0, msgs_right)
-      od)
-    else (
-      do
-      (st0, _) <-
-        betree_node_apply_messages_fwd self.betree_internal_right params
-          node_id_cnt msgs_right st;
-      _ <-
-        betree_node_apply_messages_back self.betree_internal_right params
-          node_id_cnt msgs_right st;
-      Return (st0, msgs_left)
       od)
-    od
-    od)
-  /\
-  
-  (** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
-  betree_internal_flush_back
-    (self : betree_internal_t) (params : betree_params_t)
-    (node_id_cnt : betree_node_id_counter_t)
-    (content : (u64 # betree_message_t) betree_list_t) (st : state) :
-    (betree_internal_t # betree_node_id_counter_t) result
-    =
-    do
-    p <- betree_list_partition_at_pivot_fwd content self.betree_internal_pivot;
-    let (msgs_left, msgs_right) = p in
-    do
-    len_left <- betree_list_len_fwd msgs_left;
-    if u64_ge len_left params.betree_params_min_flush_size
-    then (
-      do
-      (st0, _) <-
-        betree_node_apply_messages_fwd self.betree_internal_left params
-          node_id_cnt msgs_left st;
-      (n, node_id_cnt0) <-
-        betree_node_apply_messages_back self.betree_internal_left params
-          node_id_cnt msgs_left st;
-      len_right <- betree_list_len_fwd msgs_right;
-      if u64_ge len_right params.betree_params_min_flush_size
-      then (
-        do
-        (n0, node_id_cnt1) <-
-          betree_node_apply_messages_back self.betree_internal_right params
-            node_id_cnt0 msgs_right st0;
-        Return
-          (self
-             with
-             <|
-             betree_internal_left := n; betree_internal_right := n0
-             |>, node_id_cnt1)
-        od)
-      else Return (self with <| betree_internal_left := n |>, node_id_cnt0)
-      od)
-    else (
-      do
-      (n, node_id_cnt0) <-
-        betree_node_apply_messages_back self.betree_internal_right params
-          node_id_cnt msgs_right st;
-      Return (self with <| betree_internal_right := n |>, node_id_cnt0)
-      od)
-    od
-    od
 ’
 
 val betree_node_apply_fwd_def = Define ‘
diff --git a/tests/hol4/betree/betreeMain_TypesScript.sml b/tests/hol4/betree/betreeMain_TypesScript.sml
index c43421c2..779f6abb 100644
--- a/tests/hol4/betree/betreeMain_TypesScript.sml
+++ b/tests/hol4/betree/betreeMain_TypesScript.sml
@@ -31,12 +31,6 @@ Datatype:
 End
 
 Datatype:
-  (** [betree_main::betree::Node] *)
-  betree_node_t =
-  | BetreeNodeInternal betree_internal_t
-  | BetreeNodeLeaf betree_leaf_t
-  ;
-  
   (** [betree_main::betree::Internal] *)
   betree_internal_t =
   <|
@@ -45,6 +39,12 @@ Datatype:
     betree_internal_left : betree_node_t;
     betree_internal_right : betree_node_t;
   |>
+  ;
+  
+  (** [betree_main::betree::Node] *)
+  betree_node_t =
+  | BetreeNodeInternal betree_internal_t
+  | BetreeNodeLeaf betree_leaf_t
 End
 
 Datatype:
diff --git a/tests/hol4/betree/betreeMain_TypesTheory.sig b/tests/hol4/betree/betreeMain_TypesTheory.sig
index a451eae9..cffe6afb 100644
--- a/tests/hol4/betree/betreeMain_TypesTheory.sig
+++ b/tests/hol4/betree/betreeMain_TypesTheory.sig
@@ -22,6 +22,7 @@ sig
     val betree_internal_t_betree_internal_right : thm
     val betree_internal_t_betree_internal_right_fupd : thm
     val betree_internal_t_case_def : thm
+    val betree_internal_t_size_def : thm
     val betree_leaf_t_TY_DEF : thm
     val betree_leaf_t_betree_leaf_id : thm
     val betree_leaf_t_betree_leaf_id_fupd : thm
@@ -42,7 +43,6 @@ sig
     val betree_node_id_counter_t_size_def : thm
     val betree_node_t_TY_DEF : thm
     val betree_node_t_case_def : thm
-    val betree_node_t_size_def : thm
     val betree_params_t_TY_DEF : thm
     val betree_params_t_betree_params_min_flush_size : thm
     val betree_params_t_betree_params_min_flush_size_fupd : thm
@@ -177,11 +177,11 @@ sig
     val betree_upsert_fun_state_t_induction : thm
     val betree_upsert_fun_state_t_nchotomy : thm
     val datatype_betree_be_tree_t : thm
+    val datatype_betree_internal_t : thm
     val datatype_betree_leaf_t : thm
     val datatype_betree_list_t : thm
     val datatype_betree_message_t : thm
     val datatype_betree_node_id_counter_t : thm
-    val datatype_betree_node_t : thm
     val datatype_betree_params_t : thm
     val datatype_betree_upsert_fun_state_t : thm
   
@@ -253,30 +253,30 @@ sig
       
       ⊢ ∃rep.
           TYPE_DEFINITION
-            (λa1'.
-                 ∀ $var$('betree_node_t') $var$('betree_internal_t').
+            (λa0'.
+                 ∀ $var$('betree_internal_t') $var$('betree_node_t').
                    (∀a0'.
-                      (∃a. a0' =
-                           (λa.
-                                ind_type$CONSTR 0 (ARB,ARB,ARB)
-                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
-                             a ∧ $var$('betree_internal_t') a) ∨
-                      (∃a. a0' =
-                           (λa.
-                                ind_type$CONSTR (SUC 0) (a,ARB,ARB)
-                                  (λn. ind_type$BOTTOM)) a) ⇒
-                      $var$('betree_node_t') a0') ∧
-                   (∀a1'.
                       (∃a0 a1 a2 a3.
-                         a1' =
+                         a0' =
                          (λa0 a1 a2 a3.
-                              ind_type$CONSTR (SUC (SUC 0)) (ARB,a0,a1)
+                              ind_type$CONSTR 0 (a0,a1,ARB)
                                 (ind_type$FCONS a2
                                    (ind_type$FCONS a3 (λn. ind_type$BOTTOM))))
                            a0 a1 a2 a3 ∧ $var$('betree_node_t') a2 ∧
                          $var$('betree_node_t') a3) ⇒
-                      $var$('betree_internal_t') a1') ⇒
-                   $var$('betree_internal_t') a1') rep
+                      $var$('betree_internal_t') a0') ∧
+                   (∀a1'.
+                      (∃a. a1' =
+                           (λa.
+                                ind_type$CONSTR (SUC 0) (ARB,ARB,ARB)
+                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
+                             a ∧ $var$('betree_internal_t') a) ∨
+                      (∃a. a1' =
+                           (λa.
+                                ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB,a)
+                                  (λn. ind_type$BOTTOM)) a) ⇒
+                      $var$('betree_node_t') a1') ⇒
+                   $var$('betree_internal_t') a0') rep
    
    [betree_internal_t_betree_internal_id]  Definition
       
@@ -329,6 +329,16 @@ sig
           betree_internal_t_CASE (betree_internal_t a0 a1 a2 a3) f =
           f a0 a1 a2 a3
    
+   [betree_internal_t_size_def]  Definition
+      
+      ⊢ (∀a0 a1 a2 a3.
+           betree_internal_t_size (betree_internal_t a0 a1 a2 a3) =
+           1 + (betree_node_t_size a2 + betree_node_t_size a3)) ∧
+        (∀a. betree_node_t_size (BetreeNodeInternal a) =
+             1 + betree_internal_t_size a) ∧
+        ∀a. betree_node_t_size (BetreeNodeLeaf a) =
+            1 + betree_leaf_t_size a
+   
    [betree_leaf_t_TY_DEF]  Definition
       
       ⊢ ∃rep.
@@ -479,46 +489,36 @@ sig
       
       ⊢ ∃rep.
           TYPE_DEFINITION
-            (λa0'.
-                 ∀ $var$('betree_node_t') $var$('betree_internal_t').
+            (λa1'.
+                 ∀ $var$('betree_internal_t') $var$('betree_node_t').
                    (∀a0'.
-                      (∃a. a0' =
-                           (λa.
-                                ind_type$CONSTR 0 (ARB,ARB,ARB)
-                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
-                             a ∧ $var$('betree_internal_t') a) ∨
-                      (∃a. a0' =
-                           (λa.
-                                ind_type$CONSTR (SUC 0) (a,ARB,ARB)
-                                  (λn. ind_type$BOTTOM)) a) ⇒
-                      $var$('betree_node_t') a0') ∧
-                   (∀a1'.
                       (∃a0 a1 a2 a3.
-                         a1' =
+                         a0' =
                          (λa0 a1 a2 a3.
-                              ind_type$CONSTR (SUC (SUC 0)) (ARB,a0,a1)
+                              ind_type$CONSTR 0 (a0,a1,ARB)
                                 (ind_type$FCONS a2
                                    (ind_type$FCONS a3 (λn. ind_type$BOTTOM))))
                            a0 a1 a2 a3 ∧ $var$('betree_node_t') a2 ∧
                          $var$('betree_node_t') a3) ⇒
-                      $var$('betree_internal_t') a1') ⇒
-                   $var$('betree_node_t') a0') rep
+                      $var$('betree_internal_t') a0') ∧
+                   (∀a1'.
+                      (∃a. a1' =
+                           (λa.
+                                ind_type$CONSTR (SUC 0) (ARB,ARB,ARB)
+                                  (ind_type$FCONS a (λn. ind_type$BOTTOM)))
+                             a ∧ $var$('betree_internal_t') a) ∨
+                      (∃a. a1' =
+                           (λa.
+                                ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB,a)
+                                  (λn. ind_type$BOTTOM)) a) ⇒
+                      $var$('betree_node_t') a1') ⇒
+                   $var$('betree_node_t') a1') rep
    
    [betree_node_t_case_def]  Definition
       
       ⊢ (∀a f f1. betree_node_t_CASE (BetreeNodeInternal a) f f1 = f a) ∧
         ∀a f f1. betree_node_t_CASE (BetreeNodeLeaf a) f f1 = f1 a
    
-   [betree_node_t_size_def]  Definition
-      
-      ⊢ (∀a. betree_node_t_size (BetreeNodeInternal a) =
-             1 + betree_internal_t_size a) ∧
-        (∀a. betree_node_t_size (BetreeNodeLeaf a) =
-             1 + betree_leaf_t_size a) ∧
-        ∀a0 a1 a2 a3.
-          betree_internal_t_size (betree_internal_t a0 a1 a2 a3) =
-          1 + (betree_node_t_size a2 + betree_node_t_size a3)
-   
    [betree_params_t_TY_DEF]  Definition
       
       ⊢ ∃rep.
@@ -883,11 +883,11 @@ sig
    [betree_internal_t_Axiom]  Theorem
       
       ⊢ ∀f0 f1 f2. ∃fn0 fn1.
-          (∀a. fn0 (BetreeNodeInternal a) = f0 a (fn1 a)) ∧
-          (∀a. fn0 (BetreeNodeLeaf a) = f1 a) ∧
-          ∀a0 a1 a2 a3.
-            fn1 (betree_internal_t a0 a1 a2 a3) =
-            f2 a0 a1 a2 a3 (fn0 a2) (fn0 a3)
+          (∀a0 a1 a2 a3.
+             fn0 (betree_internal_t a0 a1 a2 a3) =
+             f0 a0 a1 a2 a3 (fn1 a2) (fn1 a3)) ∧
+          (∀a. fn1 (BetreeNodeInternal a) = f1 a (fn0 a)) ∧
+          ∀a. fn1 (BetreeNodeLeaf a) = f2 a
    
    [betree_internal_t_accessors]  Theorem
       
@@ -1130,9 +1130,9 @@ sig
    [betree_internal_t_induction]  Theorem
       
       ⊢ ∀P0 P1.
-          (∀b. P1 b ⇒ P0 (BetreeNodeInternal b)) ∧
-          (∀b. P0 (BetreeNodeLeaf b)) ∧
-          (∀b b0. P0 b ∧ P0 b0 ⇒ ∀u u0. P1 (betree_internal_t u0 u b b0)) ⇒
+          (∀b b0. P1 b ∧ P1 b0 ⇒ ∀u u0. P0 (betree_internal_t u0 u b b0)) ∧
+          (∀b. P0 b ⇒ P1 (BetreeNodeInternal b)) ∧
+          (∀b. P1 (BetreeNodeLeaf b)) ⇒
           (∀b. P0 b) ∧ ∀b. P1 b
    
    [betree_internal_t_literal_11]  Theorem
@@ -1472,11 +1472,11 @@ sig
    [betree_node_t_Axiom]  Theorem
       
       ⊢ ∀f0 f1 f2. ∃fn0 fn1.
-          (∀a. fn0 (BetreeNodeInternal a) = f0 a (fn1 a)) ∧
-          (∀a. fn0 (BetreeNodeLeaf a) = f1 a) ∧
-          ∀a0 a1 a2 a3.
-            fn1 (betree_internal_t a0 a1 a2 a3) =
-            f2 a0 a1 a2 a3 (fn0 a2) (fn0 a3)
+          (∀a0 a1 a2 a3.
+             fn0 (betree_internal_t a0 a1 a2 a3) =
+             f0 a0 a1 a2 a3 (fn1 a2) (fn1 a3)) ∧
+          (∀a. fn1 (BetreeNodeInternal a) = f1 a (fn0 a)) ∧
+          ∀a. fn1 (BetreeNodeLeaf a) = f2 a
    
    [betree_node_t_case_cong]  Theorem
       
@@ -1498,9 +1498,9 @@ sig
    [betree_node_t_induction]  Theorem
       
       ⊢ ∀P0 P1.
-          (∀b. P1 b ⇒ P0 (BetreeNodeInternal b)) ∧
-          (∀b. P0 (BetreeNodeLeaf b)) ∧
-          (∀b b0. P0 b ∧ P0 b0 ⇒ ∀u u0. P1 (betree_internal_t u0 u b b0)) ⇒
+          (∀b b0. P1 b ∧ P1 b0 ⇒ ∀u u0. P0 (betree_internal_t u0 u b b0)) ∧
+          (∀b. P0 b ⇒ P1 (BetreeNodeInternal b)) ∧
+          (∀b. P1 (BetreeNodeLeaf b)) ⇒
           (∀b. P0 b) ∧ ∀b. P1 b
    
    [betree_node_t_nchotomy]  Theorem
@@ -1706,6 +1706,14 @@ sig
           (record betree_be_tree_t betree_be_tree_params
              betree_be_tree_node_id_cnt betree_be_tree_root)
    
+   [datatype_betree_internal_t]  Theorem
+      
+      ⊢ DATATYPE
+          (record betree_internal_t betree_internal_id
+             betree_internal_pivot betree_internal_left
+             betree_internal_right ∧
+           betree_node_t BetreeNodeInternal BetreeNodeLeaf)
+   
    [datatype_betree_leaf_t]  Theorem
       
       ⊢ DATATYPE (record betree_leaf_t betree_leaf_id betree_leaf_size)
@@ -1726,14 +1734,6 @@ sig
           (record betree_node_id_counter_t
              betree_node_id_counter_next_node_id)
    
-   [datatype_betree_node_t]  Theorem
-      
-      ⊢ DATATYPE
-          (betree_node_t BetreeNodeInternal BetreeNodeLeaf ∧
-           record betree_internal_t betree_internal_id
-             betree_internal_pivot betree_internal_left
-             betree_internal_right)
-   
    [datatype_betree_params_t]  Theorem
       
       ⊢ DATATYPE
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml
index 66614c3f..1b2d6121 100644
--- a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml
+++ b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml
@@ -279,11 +279,11 @@ val test_char_fwd_def = Define ‘
 ’
 
 Datatype:
-  (** [no_nested_borrows::NodeElem] *)
-  node_elem_t = | NodeElemCons tree_t node_elem_t | NodeElemNil ;
-  
   (** [no_nested_borrows::Tree] *)
-  tree_t = | TreeLeaf 't | TreeNode 't node_elem_t tree_t
+  tree_t = | TreeLeaf 't | TreeNode 't node_elem_t tree_t ;
+  
+  (** [no_nested_borrows::NodeElem] *)
+  node_elem_t = | NodeElemCons tree_t node_elem_t | NodeElemNil
 End
 
 val [list_length_fwd_def] = DefineDiv ‘
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
index c0ff4e09..67368e38 100644
--- a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
+++ b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
@@ -47,7 +47,6 @@ sig
     val new_tuple3_fwd_def : thm
     val node_elem_t_TY_DEF : thm
     val node_elem_t_case_def : thm
-    val node_elem_t_size_def : thm
     val one_t_TY_DEF : thm
     val one_t_case_def : thm
     val one_t_size_def : thm
@@ -97,6 +96,7 @@ sig
     val test_weird_borrows1_fwd_def : thm
     val tree_t_TY_DEF : thm
     val tree_t_case_def : thm
+    val tree_t_size_def : thm
   
   (*  Theorems  *)
     val EXISTS_pair_t : thm
@@ -108,12 +108,12 @@ sig
     val datatype_empty_enum_t : thm
     val datatype_enum_t : thm
     val datatype_list_t : thm
-    val datatype_node_elem_t : thm
     val datatype_one_t : thm
     val datatype_pair_t : thm
     val datatype_struct_with_pair_t : thm
     val datatype_struct_with_tuple_t : thm
     val datatype_sum_t : thm
+    val datatype_tree_t : thm
     val empty_enum_t2num_11 : thm
     val empty_enum_t2num_ONTO : thm
     val empty_enum_t2num_num2empty_enum_t : thm
@@ -491,52 +491,41 @@ sig
       
       ⊢ ∃rep.
           TYPE_DEFINITION
-            (λa0'.
-                 ∀ $var$('node_elem_t') $var$('tree_t').
+            (λa1'.
+                 ∀ $var$('tree_t') $var$('node_elem_t').
                    (∀a0'.
-                      (∃a0 a1.
-                         a0' =
-                         (λa0 a1.
-                              ind_type$CONSTR 0 ARB
-                                (ind_type$FCONS a0
-                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
-                           a0 a1 ∧ $var$('tree_t') a0 ∧
-                         $var$('node_elem_t') a1) ∨
-                      a0' =
-                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
-                      $var$('node_elem_t') a0') ∧
-                   (∀a1'.
-                      (∃a. a1' =
-                           (λa.
-                                ind_type$CONSTR (SUC (SUC 0)) a
-                                  (λn. ind_type$BOTTOM)) a) ∨
+                      (∃a. a0' =
+                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+                             a) ∨
                       (∃a0 a1 a2.
-                         a1' =
+                         a0' =
                          (λa0 a1 a2.
-                              ind_type$CONSTR (SUC (SUC (SUC 0))) a0
+                              ind_type$CONSTR (SUC 0) a0
                                 (ind_type$FCONS a1
                                    (ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
                            a0 a1 a2 ∧ $var$('node_elem_t') a1 ∧
                          $var$('tree_t') a2) ⇒
-                      $var$('tree_t') a1') ⇒
-                   $var$('node_elem_t') a0') rep
+                      $var$('tree_t') a0') ∧
+                   (∀a1'.
+                      (∃a0 a1.
+                         a1' =
+                         (λa0 a1.
+                              ind_type$CONSTR (SUC (SUC 0)) ARB
+                                (ind_type$FCONS a0
+                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+                           a0 a1 ∧ $var$('tree_t') a0 ∧
+                         $var$('node_elem_t') a1) ∨
+                      a1' =
+                      ind_type$CONSTR (SUC (SUC (SUC 0))) ARB
+                        (λn. ind_type$BOTTOM) ⇒
+                      $var$('node_elem_t') a1') ⇒
+                   $var$('node_elem_t') a1') rep
    
    [node_elem_t_case_def]  Definition
       
       ⊢ (∀a0 a1 f v. node_elem_t_CASE (NodeElemCons a0 a1) f v = f a0 a1) ∧
         ∀f v. node_elem_t_CASE NodeElemNil f v = v
    
-   [node_elem_t_size_def]  Definition
-      
-      ⊢ (∀f a0 a1.
-           node_elem_t_size f (NodeElemCons a0 a1) =
-           1 + (tree_t_size f a0 + node_elem_t_size f a1)) ∧
-        (∀f. node_elem_t_size f NodeElemNil = 0) ∧
-        (∀f a. tree_t_size f (TreeLeaf a) = 1 + f a) ∧
-        ∀f a0 a1 a2.
-          tree_t_size f (TreeNode a0 a1 a2) =
-          1 + (f a0 + (node_elem_t_size f a1 + tree_t_size f a2))
-   
    [one_t_TY_DEF]  Definition
       
       ⊢ ∃rep.
@@ -923,41 +912,52 @@ sig
       
       ⊢ ∃rep.
           TYPE_DEFINITION
-            (λa1'.
-                 ∀ $var$('node_elem_t') $var$('tree_t').
+            (λa0'.
+                 ∀ $var$('tree_t') $var$('node_elem_t').
                    (∀a0'.
-                      (∃a0 a1.
-                         a0' =
-                         (λa0 a1.
-                              ind_type$CONSTR 0 ARB
-                                (ind_type$FCONS a0
-                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
-                           a0 a1 ∧ $var$('tree_t') a0 ∧
-                         $var$('node_elem_t') a1) ∨
-                      a0' =
-                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
-                      $var$('node_elem_t') a0') ∧
-                   (∀a1'.
-                      (∃a. a1' =
-                           (λa.
-                                ind_type$CONSTR (SUC (SUC 0)) a
-                                  (λn. ind_type$BOTTOM)) a) ∨
+                      (∃a. a0' =
+                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
+                             a) ∨
                       (∃a0 a1 a2.
-                         a1' =
+                         a0' =
                          (λa0 a1 a2.
-                              ind_type$CONSTR (SUC (SUC (SUC 0))) a0
+                              ind_type$CONSTR (SUC 0) a0
                                 (ind_type$FCONS a1
                                    (ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
                            a0 a1 a2 ∧ $var$('node_elem_t') a1 ∧
                          $var$('tree_t') a2) ⇒
-                      $var$('tree_t') a1') ⇒
-                   $var$('tree_t') a1') rep
+                      $var$('tree_t') a0') ∧
+                   (∀a1'.
+                      (∃a0 a1.
+                         a1' =
+                         (λa0 a1.
+                              ind_type$CONSTR (SUC (SUC 0)) ARB
+                                (ind_type$FCONS a0
+                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
+                           a0 a1 ∧ $var$('tree_t') a0 ∧
+                         $var$('node_elem_t') a1) ∨
+                      a1' =
+                      ind_type$CONSTR (SUC (SUC (SUC 0))) ARB
+                        (λn. ind_type$BOTTOM) ⇒
+                      $var$('node_elem_t') a1') ⇒
+                   $var$('tree_t') a0') rep
    
    [tree_t_case_def]  Definition
       
       ⊢ (∀a f f1. tree_t_CASE (TreeLeaf a) f f1 = f a) ∧
         ∀a0 a1 a2 f f1. tree_t_CASE (TreeNode a0 a1 a2) f f1 = f1 a0 a1 a2
    
+   [tree_t_size_def]  Definition
+      
+      ⊢ (∀f a. tree_t_size f (TreeLeaf a) = 1 + f a) ∧
+        (∀f a0 a1 a2.
+           tree_t_size f (TreeNode a0 a1 a2) =
+           1 + (f a0 + (node_elem_t_size f a1 + tree_t_size f a2))) ∧
+        (∀f a0 a1.
+           node_elem_t_size f (NodeElemCons a0 a1) =
+           1 + (tree_t_size f a0 + node_elem_t_size f a1)) ∧
+        ∀f. node_elem_t_size f NodeElemNil = 0
+   
    [EXISTS_pair_t]  Theorem
       
       ⊢ ∀P. (∃p. P p) ⇔ ∃t0 t. P <|pair_x := t0; pair_y := t|>
@@ -994,11 +994,6 @@ sig
       
       ⊢ DATATYPE (list_t ListCons ListNil)
    
-   [datatype_node_elem_t]  Theorem
-      
-      ⊢ DATATYPE
-          (node_elem_t NodeElemCons NodeElemNil ∧ tree_t TreeLeaf TreeNode)
-   
    [datatype_one_t]  Theorem
       
       ⊢ DATATYPE (one_t OneOne)
@@ -1019,6 +1014,11 @@ sig
       
       ⊢ DATATYPE (sum_t SumLeft SumRight)
    
+   [datatype_tree_t]  Theorem
+      
+      ⊢ DATATYPE
+          (tree_t TreeLeaf TreeNode ∧ node_elem_t NodeElemCons NodeElemNil)
+   
    [empty_enum_t2num_11]  Theorem
       
       ⊢ ∀a a'. empty_enum_t2num a = empty_enum_t2num a' ⇔ a = a'
@@ -1167,10 +1167,11 @@ sig
    [node_elem_t_Axiom]  Theorem
       
       ⊢ ∀f0 f1 f2 f3. ∃fn0 fn1.
-          (∀a0 a1. fn0 (NodeElemCons a0 a1) = f0 a0 a1 (fn1 a0) (fn0 a1)) ∧
-          fn0 NodeElemNil = f1 ∧ (∀a. fn1 (TreeLeaf a) = f2 a) ∧
-          ∀a0 a1 a2.
-            fn1 (TreeNode a0 a1 a2) = f3 a0 a1 a2 (fn0 a1) (fn1 a2)
+          (∀a. fn0 (TreeLeaf a) = f0 a) ∧
+          (∀a0 a1 a2.
+             fn0 (TreeNode a0 a1 a2) = f1 a0 a1 a2 (fn1 a1) (fn0 a2)) ∧
+          (∀a0 a1. fn1 (NodeElemCons a0 a1) = f2 a0 a1 (fn0 a0) (fn1 a1)) ∧
+          fn1 NodeElemNil = f3
    
    [node_elem_t_case_cong]  Theorem
       
@@ -1192,10 +1193,10 @@ sig
    [node_elem_t_induction]  Theorem
       
       ⊢ ∀P0 P1.
-          (∀t n. P1 t ∧ P0 n ⇒ P0 (NodeElemCons t n)) ∧ P0 NodeElemNil ∧
-          (∀t. P1 (TreeLeaf t)) ∧
-          (∀n t. P0 n ∧ P1 t ⇒ ∀t0. P1 (TreeNode t0 n t)) ⇒
-          (∀n. P0 n) ∧ ∀t. P1 t
+          (∀t. P0 (TreeLeaf t)) ∧
+          (∀n t. P1 n ∧ P0 t ⇒ ∀t0. P0 (TreeNode t0 n t)) ∧
+          (∀t n. P0 t ∧ P1 n ⇒ P1 (NodeElemCons t n)) ∧ P1 NodeElemNil ⇒
+          (∀t. P0 t) ∧ ∀n. P1 n
    
    [node_elem_t_nchotomy]  Theorem
       
@@ -1557,10 +1558,11 @@ sig
    [tree_t_Axiom]  Theorem
       
       ⊢ ∀f0 f1 f2 f3. ∃fn0 fn1.
-          (∀a0 a1. fn0 (NodeElemCons a0 a1) = f0 a0 a1 (fn1 a0) (fn0 a1)) ∧
-          fn0 NodeElemNil = f1 ∧ (∀a. fn1 (TreeLeaf a) = f2 a) ∧
-          ∀a0 a1 a2.
-            fn1 (TreeNode a0 a1 a2) = f3 a0 a1 a2 (fn0 a1) (fn1 a2)
+          (∀a. fn0 (TreeLeaf a) = f0 a) ∧
+          (∀a0 a1 a2.
+             fn0 (TreeNode a0 a1 a2) = f1 a0 a1 a2 (fn1 a1) (fn0 a2)) ∧
+          (∀a0 a1. fn1 (NodeElemCons a0 a1) = f2 a0 a1 (fn0 a0) (fn1 a1)) ∧
+          fn1 NodeElemNil = f3
    
    [tree_t_case_cong]  Theorem
       
@@ -1582,10 +1584,10 @@ sig
    [tree_t_induction]  Theorem
       
       ⊢ ∀P0 P1.
-          (∀t n. P1 t ∧ P0 n ⇒ P0 (NodeElemCons t n)) ∧ P0 NodeElemNil ∧
-          (∀t. P1 (TreeLeaf t)) ∧
-          (∀n t. P0 n ∧ P1 t ⇒ ∀t0. P1 (TreeNode t0 n t)) ⇒
-          (∀n. P0 n) ∧ ∀t. P1 t
+          (∀t. P0 (TreeLeaf t)) ∧
+          (∀n t. P1 n ∧ P0 t ⇒ ∀t0. P0 (TreeNode t0 n t)) ∧
+          (∀t n. P0 t ∧ P1 n ⇒ P1 (NodeElemCons t n)) ∧ P1 NodeElemNil ⇒
+          (∀t. P0 t) ∧ ∀n. P1 n
    
    [tree_t_nchotomy]  Theorem
       
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index a6c6f496..933aac88 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -209,20 +209,6 @@ def betree.Leaf.split_back
     let _ ← betree.store_leaf_node id1 content1 st0
     betree.NodeIdCounter.fresh_id_back node_id_cnt0
 
-/- [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function -/
-divergent def betree.Node.lookup_in_bindings
-  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
-  match bindings with
-  | betree.List.Cons hd tl =>
-    let (i, i0) := hd
-    if i = key
-    then Result.ret (Option.some i0)
-    else
-      if i > key
-      then Result.ret Option.none
-      else betree.Node.lookup_in_bindings key tl
-  | betree.List.Nil => Result.ret Option.none
-
 /- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function -/
 divergent def betree.Node.lookup_first_message_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -312,8 +298,46 @@ divergent def betree.Node.apply_upserts_back
         betree.List.push_front (U64 × betree.Message) msgs (key,
           betree.Message.Insert v)
 
+/- [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function -/
+divergent def betree.Node.lookup_in_bindings
+  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
+  match bindings with
+  | betree.List.Cons hd tl =>
+    let (i, i0) := hd
+    if i = key
+    then Result.ret (Option.some i0)
+    else
+      if i > key
+      then Result.ret Option.none
+      else betree.Node.lookup_in_bindings key tl
+  | betree.List.Nil => Result.ret Option.none
+
+/- [betree_main::betree::Internal::{4}::lookup_in_children]: forward function -/
+mutual divergent def betree.Internal.lookup_in_children
+  (self : betree.Internal) (key : U64) (st : State) :
+  Result (State × (Option U64))
+  :=
+  let ⟨ _, i, n, n0 ⟩ := self
+  if key < i
+  then betree.Node.lookup n key st
+  else betree.Node.lookup n0 key st
+
+/- [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 -/
+divergent def betree.Internal.lookup_in_children_back
+  (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal :=
+  let ⟨ i, i0, n, n0 ⟩ := self
+  if key < i0
+  then
+    do
+      let n1 ← betree.Node.lookup_back n key st
+      Result.ret (betree.Internal.mk i i0 n1 n0)
+  else
+    do
+      let n1 ← betree.Node.lookup_back n0 key st
+      Result.ret (betree.Internal.mk i i0 n n1)
+
 /- [betree_main::betree::Node::{5}::lookup]: forward function -/
-mutual divergent def betree.Node.lookup
+divergent def betree.Node.lookup
   (self : betree.Node) (key : U64) (st : State) :
   Result (State × (Option U64))
   :=
@@ -455,126 +479,8 @@ divergent def betree.Node.lookup_back
       let _ ← betree.Node.lookup_in_bindings key bindings
       Result.ret (betree.Node.Leaf node)
 
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: forward function -/
-divergent def betree.Internal.lookup_in_children
-  (self : betree.Internal) (key : U64) (st : State) :
-  Result (State × (Option U64))
-  :=
-  let ⟨ _, i, n, n0 ⟩ := self
-  if key < i
-  then betree.Node.lookup n key st
-  else betree.Node.lookup n0 key st
-
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 -/
-divergent def betree.Internal.lookup_in_children_back
-  (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal :=
-  let ⟨ i, i0, n, n0 ⟩ := self
-  if key < i0
-  then
-    do
-      let n1 ← betree.Node.lookup_back n key st
-      Result.ret (betree.Internal.mk i i0 n1 n0)
-  else
-    do
-      let n1 ← betree.Node.lookup_back n0 key st
-      Result.ret (betree.Internal.mk i i0 n n1)
-
 end
 
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function -/
-divergent def betree.Node.lookup_mut_in_bindings
-  (key : U64) (bindings : betree.List (U64 × U64)) :
-  Result (betree.List (U64 × U64))
-  :=
-  match bindings with
-  | betree.List.Cons hd tl =>
-    let (i, i0) := hd
-    if i >= key
-    then Result.ret (betree.List.Cons (i, i0) tl)
-    else betree.Node.lookup_mut_in_bindings key tl
-  | betree.List.Nil => Result.ret betree.List.Nil
-
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 -/
-divergent def betree.Node.lookup_mut_in_bindings_back
-  (key : U64) (bindings : betree.List (U64 × U64))
-  (ret0 : betree.List (U64 × U64)) :
-  Result (betree.List (U64 × U64))
-  :=
-  match bindings with
-  | betree.List.Cons hd tl =>
-    let (i, i0) := hd
-    if i >= key
-    then Result.ret ret0
-    else
-      do
-        let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0
-        Result.ret (betree.List.Cons (i, i0) tl0)
-  | betree.List.Nil => Result.ret ret0
-
-/- [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
-def betree.Node.apply_to_leaf
-  (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
-  :
-  Result (betree.List (U64 × U64))
-  :=
-  do
-    let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings
-    let b ← betree.List.head_has_key U64 bindings0 key
-    if b
-    then
-      do
-        let hd ← betree.List.pop_front (U64 × U64) bindings0
-        match new_msg with
-        | betree.Message.Insert v =>
-          do
-            let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
-            let bindings2 ←
-              betree.List.push_front (U64 × U64) bindings1 (key, v)
-            betree.Node.lookup_mut_in_bindings_back key bindings bindings2
-        | betree.Message.Delete =>
-          do
-            let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
-            betree.Node.lookup_mut_in_bindings_back key bindings bindings1
-        | betree.Message.Upsert s =>
-          do
-            let (_, i) := hd
-            let v ← betree.upsert_update (Option.some i) s
-            let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
-            let bindings2 ←
-              betree.List.push_front (U64 × U64) bindings1 (key, v)
-            betree.Node.lookup_mut_in_bindings_back key bindings bindings2
-    else
-      match new_msg with
-      | betree.Message.Insert v =>
-        do
-          let bindings1 ←
-            betree.List.push_front (U64 × U64) bindings0 (key, v)
-          betree.Node.lookup_mut_in_bindings_back key bindings bindings1
-      | betree.Message.Delete =>
-        betree.Node.lookup_mut_in_bindings_back key bindings bindings0
-      | betree.Message.Upsert s =>
-        do
-          let v ← betree.upsert_update Option.none s
-          let bindings1 ←
-            betree.List.push_front (U64 × U64) bindings0 (key, v)
-          betree.Node.lookup_mut_in_bindings_back key bindings bindings1
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
-divergent def betree.Node.apply_messages_to_leaf
-  (bindings : betree.List (U64 × U64))
-  (new_msgs : betree.List (U64 × betree.Message)) :
-  Result (betree.List (U64 × U64))
-  :=
-  match new_msgs with
-  | betree.List.Cons new_msg new_msgs_tl =>
-    do
-      let (i, m) := new_msg
-      let bindings0 ← betree.Node.apply_to_leaf bindings i m
-      betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl
-  | betree.List.Nil => Result.ret bindings
-
 /- [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 divergent def betree.Node.filter_messages_for_key
@@ -706,8 +612,174 @@ divergent def betree.Node.apply_messages_to_internal
       betree.Node.apply_messages_to_internal msgs0 new_msgs_tl
   | betree.List.Nil => Result.ret msgs
 
+/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function -/
+divergent def betree.Node.lookup_mut_in_bindings
+  (key : U64) (bindings : betree.List (U64 × U64)) :
+  Result (betree.List (U64 × U64))
+  :=
+  match bindings with
+  | betree.List.Cons hd tl =>
+    let (i, i0) := hd
+    if i >= key
+    then Result.ret (betree.List.Cons (i, i0) tl)
+    else betree.Node.lookup_mut_in_bindings key tl
+  | betree.List.Nil => Result.ret betree.List.Nil
+
+/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 -/
+divergent def betree.Node.lookup_mut_in_bindings_back
+  (key : U64) (bindings : betree.List (U64 × U64))
+  (ret0 : betree.List (U64 × U64)) :
+  Result (betree.List (U64 × U64))
+  :=
+  match bindings with
+  | betree.List.Cons hd tl =>
+    let (i, i0) := hd
+    if i >= key
+    then Result.ret ret0
+    else
+      do
+        let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0
+        Result.ret (betree.List.Cons (i, i0) tl0)
+  | betree.List.Nil => Result.ret ret0
+
+/- [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+def betree.Node.apply_to_leaf
+  (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
+  :
+  Result (betree.List (U64 × U64))
+  :=
+  do
+    let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings
+    let b ← betree.List.head_has_key U64 bindings0 key
+    if b
+    then
+      do
+        let hd ← betree.List.pop_front (U64 × U64) bindings0
+        match new_msg with
+        | betree.Message.Insert v =>
+          do
+            let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
+            let bindings2 ←
+              betree.List.push_front (U64 × U64) bindings1 (key, v)
+            betree.Node.lookup_mut_in_bindings_back key bindings bindings2
+        | betree.Message.Delete =>
+          do
+            let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
+            betree.Node.lookup_mut_in_bindings_back key bindings bindings1
+        | betree.Message.Upsert s =>
+          do
+            let (_, i) := hd
+            let v ← betree.upsert_update (Option.some i) s
+            let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
+            let bindings2 ←
+              betree.List.push_front (U64 × U64) bindings1 (key, v)
+            betree.Node.lookup_mut_in_bindings_back key bindings bindings2
+    else
+      match new_msg with
+      | betree.Message.Insert v =>
+        do
+          let bindings1 ←
+            betree.List.push_front (U64 × U64) bindings0 (key, v)
+          betree.Node.lookup_mut_in_bindings_back key bindings bindings1
+      | betree.Message.Delete =>
+        betree.Node.lookup_mut_in_bindings_back key bindings bindings0
+      | betree.Message.Upsert s =>
+        do
+          let v ← betree.upsert_update Option.none s
+          let bindings1 ←
+            betree.List.push_front (U64 × U64) bindings0 (key, v)
+          betree.Node.lookup_mut_in_bindings_back key bindings bindings1
+
+/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+   (there is a single backward function, and the forward function returns ()) -/
+divergent def betree.Node.apply_messages_to_leaf
+  (bindings : betree.List (U64 × U64))
+  (new_msgs : betree.List (U64 × betree.Message)) :
+  Result (betree.List (U64 × U64))
+  :=
+  match new_msgs with
+  | betree.List.Cons new_msg new_msgs_tl =>
+    do
+      let (i, m) := new_msg
+      let bindings0 ← betree.Node.apply_to_leaf bindings i m
+      betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl
+  | betree.List.Nil => Result.ret bindings
+
+/- [betree_main::betree::Internal::{4}::flush]: forward function -/
+mutual divergent def betree.Internal.flush
+  (self : betree.Internal) (params : betree.Params)
+  (node_id_cnt : betree.NodeIdCounter)
+  (content : betree.List (U64 × betree.Message)) (st : State) :
+  Result (State × (betree.List (U64 × betree.Message)))
+  :=
+  do
+    let ⟨ _, i, n, n0 ⟩ := self
+    let p ← betree.List.partition_at_pivot betree.Message content i
+    let (msgs_left, msgs_right) := p
+    let len_left ← betree.List.len (U64 × betree.Message) msgs_left
+    if len_left >= params.min_flush_size
+    then
+      do
+        let (st0, _) ←
+          betree.Node.apply_messages n params node_id_cnt msgs_left st
+        let (_, node_id_cnt0) ←
+          betree.Node.apply_messages_back n params node_id_cnt msgs_left st
+        let len_right ← betree.List.len (U64 × betree.Message) msgs_right
+        if len_right >= params.min_flush_size
+        then
+          do
+            let (st1, _) ←
+              betree.Node.apply_messages n0 params node_id_cnt0 msgs_right st0
+            let _ ←
+              betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
+                st0
+            Result.ret (st1, betree.List.Nil)
+        else Result.ret (st0, msgs_right)
+    else
+      do
+        let (st0, _) ←
+          betree.Node.apply_messages n0 params node_id_cnt msgs_right st
+        let _ ←
+          betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
+        Result.ret (st0, msgs_left)
+
+/- [betree_main::betree::Internal::{4}::flush]: backward function 0 -/
+divergent def betree.Internal.flush_back
+  (self : betree.Internal) (params : betree.Params)
+  (node_id_cnt : betree.NodeIdCounter)
+  (content : betree.List (U64 × betree.Message)) (st : State) :
+  Result (betree.Internal × betree.NodeIdCounter)
+  :=
+  do
+    let ⟨ i, i0, n, n0 ⟩ := self
+    let p ← betree.List.partition_at_pivot betree.Message content i0
+    let (msgs_left, msgs_right) := p
+    let len_left ← betree.List.len (U64 × betree.Message) msgs_left
+    if len_left >= params.min_flush_size
+    then
+      do
+        let (st0, _) ←
+          betree.Node.apply_messages n params node_id_cnt msgs_left st
+        let (n1, node_id_cnt0) ←
+          betree.Node.apply_messages_back n params node_id_cnt msgs_left st
+        let len_right ← betree.List.len (U64 × betree.Message) msgs_right
+        if len_right >= params.min_flush_size
+        then
+          do
+            let (n2, node_id_cnt1) ←
+              betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
+                st0
+            Result.ret (betree.Internal.mk i i0 n1 n2, node_id_cnt1)
+        else Result.ret (betree.Internal.mk i i0 n1 n0, node_id_cnt0)
+    else
+      do
+        let (n1, node_id_cnt0) ←
+          betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
+        Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0)
+
 /- [betree_main::betree::Node::{5}::apply_messages]: forward function -/
-mutual divergent def betree.Node.apply_messages
+divergent def betree.Node.apply_messages
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
   (msgs : betree.List (U64 × betree.Message)) (st : State) :
@@ -806,78 +878,6 @@ divergent def betree.Node.apply_messages_back
           let _ ← betree.store_leaf_node node.id content0 st0
           Result.ret (betree.Node.Leaf { node with size := len }, node_id_cnt)
 
-/- [betree_main::betree::Internal::{4}::flush]: forward function -/
-divergent def betree.Internal.flush
-  (self : betree.Internal) (params : betree.Params)
-  (node_id_cnt : betree.NodeIdCounter)
-  (content : betree.List (U64 × betree.Message)) (st : State) :
-  Result (State × (betree.List (U64 × betree.Message)))
-  :=
-  do
-    let ⟨ _, i, n, n0 ⟩ := self
-    let p ← betree.List.partition_at_pivot betree.Message content i
-    let (msgs_left, msgs_right) := p
-    let len_left ← betree.List.len (U64 × betree.Message) msgs_left
-    if len_left >= params.min_flush_size
-    then
-      do
-        let (st0, _) ←
-          betree.Node.apply_messages n params node_id_cnt msgs_left st
-        let (_, node_id_cnt0) ←
-          betree.Node.apply_messages_back n params node_id_cnt msgs_left st
-        let len_right ← betree.List.len (U64 × betree.Message) msgs_right
-        if len_right >= params.min_flush_size
-        then
-          do
-            let (st1, _) ←
-              betree.Node.apply_messages n0 params node_id_cnt0 msgs_right st0
-            let _ ←
-              betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
-                st0
-            Result.ret (st1, betree.List.Nil)
-        else Result.ret (st0, msgs_right)
-    else
-      do
-        let (st0, _) ←
-          betree.Node.apply_messages n0 params node_id_cnt msgs_right st
-        let _ ←
-          betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
-        Result.ret (st0, msgs_left)
-
-/- [betree_main::betree::Internal::{4}::flush]: backward function 0 -/
-divergent def betree.Internal.flush_back
-  (self : betree.Internal) (params : betree.Params)
-  (node_id_cnt : betree.NodeIdCounter)
-  (content : betree.List (U64 × betree.Message)) (st : State) :
-  Result (betree.Internal × betree.NodeIdCounter)
-  :=
-  do
-    let ⟨ i, i0, n, n0 ⟩ := self
-    let p ← betree.List.partition_at_pivot betree.Message content i0
-    let (msgs_left, msgs_right) := p
-    let len_left ← betree.List.len (U64 × betree.Message) msgs_left
-    if len_left >= params.min_flush_size
-    then
-      do
-        let (st0, _) ←
-          betree.Node.apply_messages n params node_id_cnt msgs_left st
-        let (n1, node_id_cnt0) ←
-          betree.Node.apply_messages_back n params node_id_cnt msgs_left st
-        let len_right ← betree.List.len (U64 × betree.Message) msgs_right
-        if len_right >= params.min_flush_size
-        then
-          do
-            let (n2, node_id_cnt1) ←
-              betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
-                st0
-            Result.ret (betree.Internal.mk i i0 n1 n2, node_id_cnt1)
-        else Result.ret (betree.Internal.mk i i0 n1 n0, node_id_cnt0)
-    else
-      do
-        let (n1, node_id_cnt0) ←
-          betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
-        Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0)
-
 end
 
 /- [betree_main::betree::Node::{5}::apply]: forward function -/
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index c02c148a..2f5de6a0 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -28,15 +28,15 @@ structure betree.Leaf where
 
 mutual
 
+/- [betree_main::betree::Internal] -/
+inductive betree.Internal :=
+| mk : U64 → U64 → betree.Node → betree.Node → betree.Internal
+
 /- [betree_main::betree::Node] -/
 inductive betree.Node :=
 | Internal : betree.Internal → betree.Node
 | Leaf : betree.Leaf → betree.Node
 
-/- [betree_main::betree::Internal] -/
-inductive betree.Internal :=
-| mk : U64 → U64 → betree.Node → betree.Node → betree.Internal
-
 end
 
 /- [betree_main::betree::Params] -/
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 1a180c60..884e62c4 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -251,16 +251,16 @@ def test_char : Result Char :=
 
 mutual
 
-/- [no_nested_borrows::NodeElem] -/
-inductive NodeElem (T : Type) :=
-| Cons : Tree T → NodeElem T → NodeElem T
-| Nil : NodeElem T
-
 /- [no_nested_borrows::Tree] -/
 inductive Tree (T : Type) :=
 | Leaf : T → Tree T
 | Node : T → NodeElem T → Tree T → Tree T
 
+/- [no_nested_borrows::NodeElem] -/
+inductive NodeElem (T : Type) :=
+| Cons : Tree T → NodeElem T → NodeElem T
+| Nil : NodeElem T
+
 end
 
 /- [no_nested_borrows::list_length]: forward function -/