Regenerate the betree files

8 files changed, 163 insertions, 158 deletions

diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
index 8722f0bf..4d16d8d3 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
@@ -6,94 +6,94 @@ open BetreeMain.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::List::{1}::len]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause *)
 unfold
 let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat =
   admit ()
 
-(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause *)
 unfold
 let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
   (n : u64) : nat =
   admit ()
 
-(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause *)
 unfold
-let betree_List_partition_at_pivot_decreases (t : Type0)
+let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
   (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause *)
 unfold
 let betree_Node_lookup_first_message_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause *)
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
+(** [betree_main::betree::{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::Internal::{4}::lookup_in_children]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause *)
 unfold
 let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause *)
 unfold
 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 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause *)
 unfold
 let betree_Node_filter_messages_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause *)
 unfold
 let betree_Node_lookup_first_message_after_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause *)
 unfold
 let betree_Node_apply_messages_to_internal_decreases
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
+(** [betree_main::betree::{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::{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 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause *)
 unfold
 let betree_Internal_flush_decreases (self : betree_Internal_t)
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
   (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::{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_NodeIdCounter_t)
diff --git a/tests/fstar/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/BetreeMain.Clauses.fst
index cda7b920..21f953d1 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.fst
@@ -114,7 +114,7 @@ let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
 
 (** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
 unfold
-let betree_List_partition_at_pivot_decreases (t : Type0)
+let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
   (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) =
   self
 
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index d2bf5c7c..2ccbac60 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -44,16 +44,16 @@ let betree_fresh_node_id (counter : u64) : result u64 =
 let betree_fresh_node_id_back (counter : u64) : result u64 =
   u64_add counter 1
 
-(** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function *)
 let betree_NodeIdCounter_new : result betree_NodeIdCounter_t =
   Return { next_node_id = 0 }
 
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function *)
 let betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result u64 =
   let* _ = u64_add self.next_node_id 1 in Return self.next_node_id
 
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 *)
 let betree_NodeIdCounter_fresh_id_back
   (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t =
   let* i = u64_add self.next_node_id 1 in Return { next_node_id = i }
@@ -77,7 +77,7 @@ let betree_upsert_update
     end
   end
 
-(** [betree_main::betree::List::{1}::len]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function *)
 let rec betree_List_len
   (t : Type0) (self : betree_List_t t) :
   Tot (result u64) (decreases (betree_List_len_decreases t self))
@@ -87,7 +87,7 @@ let rec betree_List_len
   | Betree_List_Nil -> Return 0
   end
 
-(** [betree_main::betree::List::{1}::split_at]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function *)
 let rec betree_List_split_at
   (t : Type0) (self : betree_List_t t) (n : u64) :
   Tot (result ((betree_List_t t) & (betree_List_t t)))
@@ -106,7 +106,7 @@ let rec betree_List_split_at
     | Betree_List_Nil -> Fail Failure
     end
 
-(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let betree_List_push_front
   (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
@@ -114,7 +114,7 @@ let betree_List_push_front
   let l = tl in
   Return (Betree_List_Cons x l)
 
-(** [betree_main::betree::List::{1}::pop_front]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function *)
 let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t =
   let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in
   begin match ls with
@@ -122,7 +122,7 @@ let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t =
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::List::{1}::pop_front]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 *)
 let betree_List_pop_front_back
   (t : Type0) (self : betree_List_t t) : result (betree_List_t t) =
   let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in
@@ -131,26 +131,26 @@ let betree_List_pop_front_back
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::List::{1}::hd]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function *)
 let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   begin match self with
   | Betree_List_Cons hd l -> Return hd
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::List::{2}::head_has_key]: forward function *)
-let betree_List_head_has_key
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function *)
+let betree_ListTupleU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
   begin match self with
   | Betree_List_Cons hd l -> let (i, _) = hd in Return (i = key)
   | Betree_List_Nil -> Return false
   end
 
-(** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *)
-let rec betree_List_partition_at_pivot
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function *)
+let rec betree_ListTupleU64T_partition_at_pivot
   (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
   Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t))))
-  (decreases (betree_List_partition_at_pivot_decreases t self pivot))
+  (decreases (betree_ListTupleU64T_partition_at_pivot_decreases t self pivot))
   =
   begin match self with
   | Betree_List_Cons hd tl ->
@@ -158,14 +158,14 @@ let rec betree_List_partition_at_pivot
     if i >= pivot
     then Return (Betree_List_Nil, Betree_List_Cons (i, x) tl)
     else
-      let* p = betree_List_partition_at_pivot t tl pivot in
+      let* p = betree_ListTupleU64T_partition_at_pivot t tl pivot in
       let (ls0, ls1) = p in
       let l = ls0 in
       Return (Betree_List_Cons (i, x) l, ls1)
   | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil)
   end
 
-(** [betree_main::betree::Leaf::{3}::split]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function *)
 let betree_Leaf_split
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -185,7 +185,7 @@ let betree_Leaf_split
   let n0 = Betree_Node_Leaf { id = id1; size = params.split_size } in
   Return (st1, { id = self.id; pivot = pivot; left = n; right = n0 })
 
-(** [betree_main::betree::Leaf::{3}::split]: backward function 2 *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 *)
 let betree_Leaf_split_back
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -202,7 +202,7 @@ let betree_Leaf_split_back
   let* _ = betree_store_leaf_node id1 content1 st0 in
   betree_NodeIdCounter_fresh_id_back node_id_cnt0
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function *)
 let rec betree_Node_lookup_first_message_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
@@ -217,7 +217,7 @@ let rec betree_Node_lookup_first_message_for_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 *)
 let rec betree_Node_lookup_first_message_for_key_back
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t))
   (ret : betree_List_t (u64 & betree_Message_t)) :
@@ -236,14 +236,14 @@ let rec betree_Node_lookup_first_message_for_key_back
   | Betree_List_Nil -> Return ret
   end
 
-(** [betree_main::betree::Node::{5}::apply_upserts]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function *)
 let rec betree_Node_apply_upserts
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
   Tot (result (state & u64))
   (decreases (betree_Node_apply_upserts_decreases msgs prev key st))
   =
-  let* b = betree_List_head_has_key betree_Message_t msgs key in
+  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in
   if b
   then
     let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in
@@ -263,14 +263,14 @@ let rec betree_Node_apply_upserts
         Betree_Message_Insert v) in
     Return (st0, v)
 
-(** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 *)
 let rec betree_Node_apply_upserts_back
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
   (decreases (betree_Node_apply_upserts_decreases msgs prev key st))
   =
-  let* b = betree_List_head_has_key betree_Message_t msgs key in
+  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in
   if b
   then
     let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in
@@ -288,7 +288,7 @@ let rec betree_Node_apply_upserts_back
     betree_List_push_front (u64 & betree_Message_t) msgs (key,
       Betree_Message_Insert v)
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function *)
 let rec betree_Node_lookup_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (option u64))
@@ -303,7 +303,7 @@ let rec betree_Node_lookup_in_bindings
   | Betree_List_Nil -> Return None
   end
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function *)
 let rec betree_Internal_lookup_in_children
   (self : betree_Internal_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
@@ -313,7 +313,7 @@ let rec betree_Internal_lookup_in_children
   then betree_Node_lookup self.left key st
   else betree_Node_lookup self.right key st
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+(** [betree_main::betree::{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)
@@ -327,7 +327,7 @@ and betree_Internal_lookup_in_children_back
     let* n = betree_Node_lookup_back self.right key st in
     Return { self with right = n }
 
-(** [betree_main::betree::Node::{5}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function *)
 and betree_Node_lookup
   (self : betree_Node_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
@@ -386,7 +386,7 @@ and betree_Node_lookup
     Return (st0, o)
   end
 
-(** [betree_main::betree::Node::{5}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 *)
 and betree_Node_lookup_back
   (self : betree_Node_t) (key : u64) (st : state) :
   Tot (result betree_Node_t)
@@ -445,7 +445,7 @@ and betree_Node_lookup_back
     Return (Betree_Node_Leaf node)
   end
 
-(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec betree_Node_filter_messages_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
@@ -465,7 +465,7 @@ let rec betree_Node_filter_messages_for_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function *)
 let rec betree_Node_lookup_first_message_after_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
@@ -480,7 +480,7 @@ let rec betree_Node_lookup_first_message_after_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 *)
 let rec betree_Node_lookup_first_message_after_key_back
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t))
   (ret : betree_List_t (u64 & betree_Message_t)) :
@@ -499,7 +499,7 @@ let rec betree_Node_lookup_first_message_after_key_back
   | Betree_List_Nil -> Return ret
   end
 
-(** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let betree_Node_apply_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64)
@@ -507,7 +507,7 @@ let betree_Node_apply_to_internal
   result (betree_List_t (u64 & betree_Message_t))
   =
   let* msgs0 = betree_Node_lookup_first_message_for_key key msgs in
-  let* b = betree_List_head_has_key betree_Message_t msgs0 key in
+  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs0 key in
   if b
   then
     begin match new_msg with
@@ -558,7 +558,7 @@ let betree_Node_apply_to_internal
       betree_List_push_front (u64 & betree_Message_t) msgs0 (key, new_msg) in
     betree_Node_lookup_first_message_for_key_back key msgs msgs1
 
-(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec betree_Node_apply_messages_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t))
@@ -574,7 +574,7 @@ let rec betree_Node_apply_messages_to_internal
   | Betree_List_Nil -> Return msgs
   end
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function *)
 let rec betree_Node_lookup_mut_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (betree_List_t (u64 & u64)))
@@ -589,7 +589,7 @@ let rec betree_Node_lookup_mut_in_bindings
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+(** [betree_main::betree::{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)) :
@@ -607,7 +607,7 @@ let rec betree_Node_lookup_mut_in_bindings_back
   | Betree_List_Nil -> Return ret
   end
 
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let betree_Node_apply_to_leaf
   (bindings : betree_List_t (u64 & u64)) (key : u64)
@@ -615,7 +615,7 @@ let betree_Node_apply_to_leaf
   result (betree_List_t (u64 & u64))
   =
   let* bindings0 = betree_Node_lookup_mut_in_bindings key bindings in
-  let* b = betree_List_head_has_key u64 bindings0 key in
+  let* b = betree_ListTupleU64T_head_has_key u64 bindings0 key in
   if b
   then
     let* hd = betree_List_pop_front (u64 & u64) bindings0 in
@@ -647,7 +647,7 @@ let betree_Node_apply_to_leaf
       betree_Node_lookup_mut_in_bindings_back key bindings bindings1
     end
 
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec betree_Node_apply_messages_to_leaf
   (bindings : betree_List_t (u64 & u64))
@@ -663,7 +663,7 @@ let rec betree_Node_apply_messages_to_leaf
   | Betree_List_Nil -> Return bindings
   end
 
-(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function *)
 let rec betree_Internal_flush
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -672,7 +672,8 @@ let rec betree_Internal_flush
   (decreases (
     betree_Internal_flush_decreases self params node_id_cnt content st))
   =
-  let* p = betree_List_partition_at_pivot betree_Message_t content self.pivot
+  let* p =
+    betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot
     in
   let (msgs_left, msgs_right) = p in
   let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in
@@ -702,7 +703,7 @@ let rec betree_Internal_flush
         st in
     Return (st0, msgs_left)
 
-(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+(** [betree_main::betree::{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_NodeIdCounter_t)
@@ -711,7 +712,8 @@ and betree_Internal_flush_back
   (decreases (
     betree_Internal_flush_decreases self params node_id_cnt content st))
   =
-  let* p = betree_List_partition_at_pivot betree_Message_t content self.pivot
+  let* p =
+    betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot
     in
   let (msgs_left, msgs_right) = p in
   let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in
@@ -736,7 +738,7 @@ and betree_Internal_flush_back
         st in
     Return ({ self with right = n }, node_id_cnt0)
 
-(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function *)
 and betree_Node_apply_messages
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -776,7 +778,7 @@ and betree_Node_apply_messages
       Return (st1, ())
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 *)
 and betree_Node_apply_messages_back
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -819,7 +821,7 @@ and betree_Node_apply_messages_back
       Return (Betree_Node_Leaf { node with size = len }, node_id_cnt)
   end
 
-(** [betree_main::betree::Node::{5}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function *)
 let betree_Node_apply
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -835,7 +837,7 @@ let betree_Node_apply
       (key, new_msg) l) st in
   Return (st0, ())
 
-(** [betree_main::betree::Node::{5}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 *)
 let betree_Node_apply_back
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -846,7 +848,7 @@ let betree_Node_apply_back
   betree_Node_apply_messages_back self params node_id_cnt (Betree_List_Cons
     (key, new_msg) l) st
 
-(** [betree_main::betree::BeTree::{6}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function *)
 let betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state & betree_BeTree_t)
@@ -862,7 +864,7 @@ let betree_BeTree_new
       root = (Betree_Node_Leaf { id = id; size = 0 })
     })
 
-(** [betree_main::betree::BeTree::{6}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function *)
 let betree_BeTree_apply
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
   result (state & unit)
@@ -873,7 +875,7 @@ let betree_BeTree_apply
     betree_Node_apply_back self.root self.params self.node_id_cnt key msg st in
   Return (st0, ())
 
-(** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 *)
 let betree_BeTree_apply_back
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
   result betree_BeTree_t
@@ -882,7 +884,7 @@ let betree_BeTree_apply_back
     betree_Node_apply_back self.root self.params self.node_id_cnt key msg st in
   Return { self with node_id_cnt = nic; root = n }
 
-(** [betree_main::betree::BeTree::{6}::insert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function *)
 let betree_BeTree_insert
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result (state & unit)
@@ -893,26 +895,26 @@ let betree_BeTree_insert
     in
   Return (st0, ())
 
-(** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 *)
 let betree_BeTree_insert_back
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result betree_BeTree_t
   =
   betree_BeTree_apply_back self key (Betree_Message_Insert value) st
 
-(** [betree_main::betree::BeTree::{6}::delete]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function *)
 let betree_BeTree_delete
   (self : betree_BeTree_t) (key : u64) (st : state) : result (state & unit) =
   let* (st0, _) = betree_BeTree_apply self key Betree_Message_Delete st in
   let* _ = betree_BeTree_apply_back self key Betree_Message_Delete st in
   Return (st0, ())
 
-(** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 *)
 let betree_BeTree_delete_back
   (self : betree_BeTree_t) (key : u64) (st : state) : result betree_BeTree_t =
   betree_BeTree_apply_back self key Betree_Message_Delete st
 
-(** [betree_main::betree::BeTree::{6}::upsert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function *)
 let betree_BeTree_upsert
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) :
@@ -923,7 +925,7 @@ let betree_BeTree_upsert
   let* _ = betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st in
   Return (st0, ())
 
-(** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 *)
 let betree_BeTree_upsert_back
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) :
@@ -931,14 +933,14 @@ let betree_BeTree_upsert_back
   =
   betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st
 
-(** [betree_main::betree::BeTree::{6}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function *)
 let betree_BeTree_lookup
   (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state & (option u64))
   =
   betree_Node_lookup self.root key st
 
-(** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 *)
 let betree_BeTree_lookup_back
   (self : betree_BeTree_t) (key : u64) (st : state) : result betree_BeTree_t =
   let* n = betree_Node_lookup_back self.root key st in
diff --git a/tests/fstar/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.Opaque.fsti
index c5d0a814..23d2e60e 100644
--- a/tests/fstar/betree/BetreeMain.Opaque.fsti
+++ b/tests/fstar/betree/BetreeMain.Opaque.fsti
@@ -24,7 +24,7 @@ val betree_utils_load_leaf_node
 val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
 
-(** [core::option::Option::{0}::unwrap]: forward function *)
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function *)
 val core_option_Option_unwrap
   (t : Type0) : option t -> state -> result (state & t)
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
index 8722f0bf..4d16d8d3 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
@@ -6,94 +6,94 @@ open BetreeMain.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_main::betree::List::{1}::len]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause *)
 unfold
 let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat =
   admit ()
 
-(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause *)
 unfold
 let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
   (n : u64) : nat =
   admit ()
 
-(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause *)
 unfold
-let betree_List_partition_at_pivot_decreases (t : Type0)
+let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
   (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause *)
 unfold
 let betree_Node_lookup_first_message_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause *)
 unfold
 let betree_Node_apply_upserts_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
+(** [betree_main::betree::{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::Internal::{4}::lookup_in_children]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause *)
 unfold
 let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t)
   (key : u64) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause *)
 unfold
 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 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause *)
 unfold
 let betree_Node_filter_messages_for_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause *)
 unfold
 let betree_Node_lookup_first_message_after_key_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases clause *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause *)
 unfold
 let betree_Node_apply_messages_to_internal_decreases
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
+(** [betree_main::betree::{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::{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 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause *)
 unfold
 let betree_Internal_flush_decreases (self : betree_Internal_t)
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
   (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat =
   admit ()
 
-(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
+(** [betree_main::betree::{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_NodeIdCounter_t)
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst
index cda7b920..21f953d1 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst
@@ -114,7 +114,7 @@ let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
 
 (** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
 unfold
-let betree_List_partition_at_pivot_decreases (t : Type0)
+let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
   (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) =
   self
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 08c4f615..b46ca0a0 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -44,16 +44,16 @@ let betree_fresh_node_id (counter : u64) : result u64 =
 let betree_fresh_node_id_back (counter : u64) : result u64 =
   u64_add counter 1
 
-(** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function *)
 let betree_NodeIdCounter_new : result betree_NodeIdCounter_t =
   Return { next_node_id = 0 }
 
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function *)
 let betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result u64 =
   let* _ = u64_add self.next_node_id 1 in Return self.next_node_id
 
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 *)
 let betree_NodeIdCounter_fresh_id_back
   (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t =
   let* i = u64_add self.next_node_id 1 in Return { next_node_id = i }
@@ -77,7 +77,7 @@ let betree_upsert_update
     end
   end
 
-(** [betree_main::betree::List::{1}::len]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function *)
 let rec betree_List_len
   (t : Type0) (self : betree_List_t t) :
   Tot (result u64) (decreases (betree_List_len_decreases t self))
@@ -87,7 +87,7 @@ let rec betree_List_len
   | Betree_List_Nil -> Return 0
   end
 
-(** [betree_main::betree::List::{1}::split_at]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function *)
 let rec betree_List_split_at
   (t : Type0) (self : betree_List_t t) (n : u64) :
   Tot (result ((betree_List_t t) & (betree_List_t t)))
@@ -106,7 +106,7 @@ let rec betree_List_split_at
     | Betree_List_Nil -> Fail Failure
     end
 
-(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let betree_List_push_front
   (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
@@ -114,7 +114,7 @@ let betree_List_push_front
   let l = tl in
   Return (Betree_List_Cons x l)
 
-(** [betree_main::betree::List::{1}::pop_front]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function *)
 let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t =
   let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in
   begin match ls with
@@ -122,7 +122,7 @@ let betree_List_pop_front (t : Type0) (self : betree_List_t t) : result t =
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::List::{1}::pop_front]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 *)
 let betree_List_pop_front_back
   (t : Type0) (self : betree_List_t t) : result (betree_List_t t) =
   let ls = core_mem_replace (betree_List_t t) self Betree_List_Nil in
@@ -131,26 +131,26 @@ let betree_List_pop_front_back
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::List::{1}::hd]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function *)
 let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   begin match self with
   | Betree_List_Cons hd l -> Return hd
   | Betree_List_Nil -> Fail Failure
   end
 
-(** [betree_main::betree::List::{2}::head_has_key]: forward function *)
-let betree_List_head_has_key
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function *)
+let betree_ListTupleU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
   begin match self with
   | Betree_List_Cons hd l -> let (i, _) = hd in Return (i = key)
   | Betree_List_Nil -> Return false
   end
 
-(** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *)
-let rec betree_List_partition_at_pivot
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function *)
+let rec betree_ListTupleU64T_partition_at_pivot
   (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
   Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t))))
-  (decreases (betree_List_partition_at_pivot_decreases t self pivot))
+  (decreases (betree_ListTupleU64T_partition_at_pivot_decreases t self pivot))
   =
   begin match self with
   | Betree_List_Cons hd tl ->
@@ -158,14 +158,14 @@ let rec betree_List_partition_at_pivot
     if i >= pivot
     then Return (Betree_List_Nil, Betree_List_Cons (i, x) tl)
     else
-      let* p = betree_List_partition_at_pivot t tl pivot in
+      let* p = betree_ListTupleU64T_partition_at_pivot t tl pivot in
       let (ls0, ls1) = p in
       let l = ls0 in
       Return (Betree_List_Cons (i, x) l, ls1)
   | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil)
   end
 
-(** [betree_main::betree::Leaf::{3}::split]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function *)
 let betree_Leaf_split
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -185,7 +185,7 @@ let betree_Leaf_split
   let n0 = Betree_Node_Leaf { id = id1; size = params.split_size } in
   Return (st1, { id = self.id; pivot = pivot; left = n; right = n0 })
 
-(** [betree_main::betree::Leaf::{3}::split]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 0 *)
 let betree_Leaf_split_back0
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -202,7 +202,7 @@ let betree_Leaf_split_back0
   let* _ = betree_store_leaf_node id1 content1 st1 in
   Return (st0, ())
 
-(** [betree_main::betree::Leaf::{3}::split]: backward function 1 *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 1 *)
 let betree_Leaf_split_back1
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -219,7 +219,7 @@ let betree_Leaf_split_back1
   let* _ = betree_store_leaf_node id1 content1 st1 in
   Return (st0, ())
 
-(** [betree_main::betree::Leaf::{3}::split]: backward function 2 *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 *)
 let betree_Leaf_split_back2
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -237,7 +237,7 @@ let betree_Leaf_split_back2
   let* node_id_cnt1 = betree_NodeIdCounter_fresh_id_back node_id_cnt0 in
   Return (st0, node_id_cnt1)
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function *)
 let rec betree_Node_lookup_first_message_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
@@ -252,7 +252,7 @@ let rec betree_Node_lookup_first_message_for_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 *)
 let rec betree_Node_lookup_first_message_for_key_back
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t))
   (ret : betree_List_t (u64 & betree_Message_t)) :
@@ -271,14 +271,14 @@ let rec betree_Node_lookup_first_message_for_key_back
   | Betree_List_Nil -> Return ret
   end
 
-(** [betree_main::betree::Node::{5}::apply_upserts]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function *)
 let rec betree_Node_apply_upserts
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
   Tot (result (state & u64))
   (decreases (betree_Node_apply_upserts_decreases msgs prev key st))
   =
-  let* b = betree_List_head_has_key betree_Message_t msgs key in
+  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in
   if b
   then
     let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in
@@ -298,14 +298,14 @@ let rec betree_Node_apply_upserts
         Betree_Message_Insert v) in
     Return (st0, v)
 
-(** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 *)
 let rec betree_Node_apply_upserts_back
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) (st0 : state) :
   Tot (result (state & (betree_List_t (u64 & betree_Message_t))))
   (decreases (betree_Node_apply_upserts_decreases msgs prev key st))
   =
-  let* b = betree_List_head_has_key betree_Message_t msgs key in
+  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in
   if b
   then
     let* msg = betree_List_pop_front (u64 & betree_Message_t) msgs in
@@ -325,7 +325,7 @@ let rec betree_Node_apply_upserts_back
         Betree_Message_Insert v) in
     Return (st0, msgs0)
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function *)
 let rec betree_Node_lookup_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (option u64))
@@ -340,7 +340,7 @@ let rec betree_Node_lookup_in_bindings
   | Betree_List_Nil -> Return None
   end
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function *)
 let rec betree_Internal_lookup_in_children
   (self : betree_Internal_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
@@ -350,7 +350,7 @@ let rec betree_Internal_lookup_in_children
   then betree_Node_lookup self.left key st
   else betree_Node_lookup self.right key st
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+(** [betree_main::betree::{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))
@@ -364,7 +364,7 @@ and betree_Internal_lookup_in_children_back
     let* (st1, n) = betree_Node_lookup_back self.right key st st0 in
     Return (st1, { self with right = n })
 
-(** [betree_main::betree::Node::{5}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function *)
 and betree_Node_lookup
   (self : betree_Node_t) (key : u64) (st : state) :
   Tot (result (state & (option u64)))
@@ -424,7 +424,7 @@ and betree_Node_lookup
     Return (st0, o)
   end
 
-(** [betree_main::betree::Node::{5}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 *)
 and betree_Node_lookup_back
   (self : betree_Node_t) (key : u64) (st : state) (st0 : state) :
   Tot (result (state & betree_Node_t))
@@ -486,7 +486,7 @@ and betree_Node_lookup_back
     Return (st0, Betree_Node_Leaf node)
   end
 
-(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec betree_Node_filter_messages_for_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
@@ -506,7 +506,7 @@ let rec betree_Node_filter_messages_for_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function *)
 let rec betree_Node_lookup_first_message_after_key
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
@@ -521,7 +521,7 @@ let rec betree_Node_lookup_first_message_after_key
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 *)
 let rec betree_Node_lookup_first_message_after_key_back
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t))
   (ret : betree_List_t (u64 & betree_Message_t)) :
@@ -540,7 +540,7 @@ let rec betree_Node_lookup_first_message_after_key_back
   | Betree_List_Nil -> Return ret
   end
 
-(** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let betree_Node_apply_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64)
@@ -548,7 +548,7 @@ let betree_Node_apply_to_internal
   result (betree_List_t (u64 & betree_Message_t))
   =
   let* msgs0 = betree_Node_lookup_first_message_for_key key msgs in
-  let* b = betree_List_head_has_key betree_Message_t msgs0 key in
+  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs0 key in
   if b
   then
     begin match new_msg with
@@ -599,7 +599,7 @@ let betree_Node_apply_to_internal
       betree_List_push_front (u64 & betree_Message_t) msgs0 (key, new_msg) in
     betree_Node_lookup_first_message_for_key_back key msgs msgs1
 
-(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec betree_Node_apply_messages_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t))
@@ -615,7 +615,7 @@ let rec betree_Node_apply_messages_to_internal
   | Betree_List_Nil -> Return msgs
   end
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function *)
 let rec betree_Node_lookup_mut_in_bindings
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (betree_List_t (u64 & u64)))
@@ -630,7 +630,7 @@ let rec betree_Node_lookup_mut_in_bindings
   | Betree_List_Nil -> Return Betree_List_Nil
   end
 
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+(** [betree_main::betree::{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)) :
@@ -648,7 +648,7 @@ let rec betree_Node_lookup_mut_in_bindings_back
   | Betree_List_Nil -> Return ret
   end
 
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let betree_Node_apply_to_leaf
   (bindings : betree_List_t (u64 & u64)) (key : u64)
@@ -656,7 +656,7 @@ let betree_Node_apply_to_leaf
   result (betree_List_t (u64 & u64))
   =
   let* bindings0 = betree_Node_lookup_mut_in_bindings key bindings in
-  let* b = betree_List_head_has_key u64 bindings0 key in
+  let* b = betree_ListTupleU64T_head_has_key u64 bindings0 key in
   if b
   then
     let* hd = betree_List_pop_front (u64 & u64) bindings0 in
@@ -688,7 +688,7 @@ let betree_Node_apply_to_leaf
       betree_Node_lookup_mut_in_bindings_back key bindings bindings1
     end
 
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec betree_Node_apply_messages_to_leaf
   (bindings : betree_List_t (u64 & u64))
@@ -704,7 +704,7 @@ let rec betree_Node_apply_messages_to_leaf
   | Betree_List_Nil -> Return bindings
   end
 
-(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function *)
 let rec betree_Internal_flush
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -713,7 +713,8 @@ let rec betree_Internal_flush
   (decreases (
     betree_Internal_flush_decreases self params node_id_cnt content st))
   =
-  let* p = betree_List_partition_at_pivot betree_Message_t content self.pivot
+  let* p =
+    betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot
     in
   let (msgs_left, msgs_right) = p in
   let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in
@@ -752,7 +753,7 @@ let rec betree_Internal_flush
         st st1 in
     Return (st2, msgs_left)
 
-(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 *)
 and betree_Internal_flush_back'a
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -762,7 +763,8 @@ and betree_Internal_flush_back'a
   (decreases (
     betree_Internal_flush_decreases self params node_id_cnt content st))
   =
-  let* p = betree_List_partition_at_pivot betree_Message_t content self.pivot
+  let* p =
+    betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot
     in
   let (msgs_left, msgs_right) = p in
   let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in
@@ -801,7 +803,7 @@ and betree_Internal_flush_back'a
         st st2 in
     Return (st0, ({ self with right = n }, node_id_cnt0))
 
-(** [betree_main::betree::Internal::{4}::flush]: backward function 1 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 1 *)
 and betree_Internal_flush_back1
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -811,7 +813,8 @@ and betree_Internal_flush_back1
   (decreases (
     betree_Internal_flush_decreases self params node_id_cnt content st))
   =
-  let* p = betree_List_partition_at_pivot betree_Message_t content self.pivot
+  let* p =
+    betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot
     in
   let (msgs_left, msgs_right) = p in
   let* len_left = betree_List_len (u64 & betree_Message_t) msgs_left in
@@ -850,7 +853,7 @@ and betree_Internal_flush_back1
         st st2 in
     Return (st0, ())
 
-(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function *)
 and betree_Node_apply_messages
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -891,7 +894,7 @@ and betree_Node_apply_messages
       Return (st1, ())
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
+(** [betree_main::betree::{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_NodeIdCounter_t)
@@ -937,7 +940,7 @@ and betree_Node_apply_messages_back'a
       Return (st0, (Betree_Node_Leaf { node with size = len }, node_id_cnt))
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 1 *)
+(** [betree_main::betree::{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_NodeIdCounter_t)
@@ -979,7 +982,7 @@ and betree_Node_apply_messages_back1
       let* _ = betree_store_leaf_node node.id content0 st1 in Return (st0, ())
   end
 
-(** [betree_main::betree::Node::{5}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function *)
 let betree_Node_apply
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -996,7 +999,7 @@ let betree_Node_apply
   betree_Node_apply_messages_back1 self params node_id_cnt (Betree_List_Cons
     (key, new_msg) l) st st1
 
-(** [betree_main::betree::Node::{5}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 *)
 let betree_Node_apply_back'a
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -1015,7 +1018,7 @@ let betree_Node_apply_back'a
       (key, new_msg) l) st st2 in
   Return (st0, (self0, node_id_cnt0))
 
-(** [betree_main::betree::Node::{5}::apply]: backward function 1 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 1 *)
 let betree_Node_apply_back1
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -1034,7 +1037,7 @@ let betree_Node_apply_back1
       (key, new_msg) l) st st2 in
   Return (st0, ())
 
-(** [betree_main::betree::BeTree::{6}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function *)
 let betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state & betree_BeTree_t)
@@ -1050,7 +1053,7 @@ let betree_BeTree_new
       root = (Betree_Node_Leaf { id = id; size = 0 })
     })
 
-(** [betree_main::betree::BeTree::{6}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function *)
 let betree_BeTree_apply
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
   result (state & unit)
@@ -1062,7 +1065,7 @@ let betree_BeTree_apply
       st0 in
   betree_Node_apply_back1 self.root self.params self.node_id_cnt key msg st st1
 
-(** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 *)
 let betree_BeTree_apply_back
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state)
   (st0 : state) :
@@ -1078,7 +1081,7 @@ let betree_BeTree_apply_back
       st2 in
   Return (st0, { self with node_id_cnt = nic; root = n })
 
-(** [betree_main::betree::BeTree::{6}::insert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function *)
 let betree_BeTree_insert
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result (state & unit)
@@ -1089,7 +1092,7 @@ let betree_BeTree_insert
     betree_BeTree_apply_back self key (Betree_Message_Insert value) st st0 in
   Return (st1, ())
 
-(** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 *)
 let betree_BeTree_insert_back
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) (st0 : state)
   :
@@ -1101,7 +1104,7 @@ let betree_BeTree_insert_back
     betree_BeTree_apply_back self key (Betree_Message_Insert value) st st1 in
   Return (st0, self0)
 
-(** [betree_main::betree::BeTree::{6}::delete]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function *)
 let betree_BeTree_delete
   (self : betree_BeTree_t) (key : u64) (st : state) : result (state & unit) =
   let* (st0, _) = betree_BeTree_apply self key Betree_Message_Delete st in
@@ -1109,7 +1112,7 @@ let betree_BeTree_delete
     betree_BeTree_apply_back self key Betree_Message_Delete st st0 in
   Return (st1, ())
 
-(** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 *)
 let betree_BeTree_delete_back
   (self : betree_BeTree_t) (key : u64) (st : state) (st0 : state) :
   result (state & betree_BeTree_t)
@@ -1119,7 +1122,7 @@ let betree_BeTree_delete_back
     betree_BeTree_apply_back self key Betree_Message_Delete st st1 in
   Return (st0, self0)
 
-(** [betree_main::betree::BeTree::{6}::upsert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function *)
 let betree_BeTree_upsert
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) :
@@ -1131,7 +1134,7 @@ let betree_BeTree_upsert
     betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st st0 in
   Return (st1, ())
 
-(** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 *)
 let betree_BeTree_upsert_back
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) (st0 : state) :
@@ -1143,14 +1146,14 @@ let betree_BeTree_upsert_back
     betree_BeTree_apply_back self key (Betree_Message_Upsert upd) st st1 in
   Return (st0, self0)
 
-(** [betree_main::betree::BeTree::{6}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function *)
 let betree_BeTree_lookup
   (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state & (option u64))
   =
   betree_Node_lookup self.root key st
 
-(** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 *)
 let betree_BeTree_lookup_back
   (self : betree_BeTree_t) (key : u64) (st : state) (st0 : state) :
   result (state & betree_BeTree_t)
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
index c5d0a814..23d2e60e 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti
@@ -24,7 +24,7 @@ val betree_utils_load_leaf_node
 val betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
 
-(** [core::option::Option::{0}::unwrap]: forward function *)
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function *)
 val core_option_Option_unwrap
   (t : Type0) : option t -> state -> result (state & t)