Regenerate the betree files

12 files changed, 279 insertions, 274 deletions

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 261e8270..d7428744 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -56,19 +56,19 @@ Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
   u64_add counter 1%u64
 .
 
-(** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function *)
 Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
   Return {| betree_NodeIdCounter_next_node_id := 0%u64 |}
 .
 
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function *)
 Definition betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result u64 :=
   _ <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
   Return self.(betree_NodeIdCounter_next_node_id)
 .
 
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 *)
 Definition betree_NodeIdCounter_fresh_id_back
   (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t :=
   i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
@@ -95,7 +95,7 @@ Definition betree_upsert_update
   end
 .
 
-(** [betree_main::betree::List::{1}::len]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function *)
 Fixpoint betree_List_len
   (T : Type) (n : nat) (self : betree_List_t T) : result u64 :=
   match n with
@@ -108,7 +108,7 @@ Fixpoint betree_List_len
   end
 .
 
-(** [betree_main::betree::List::{1}::split_at]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function *)
 Fixpoint betree_List_split_at
   (T : Type) (n : nat) (self : betree_List_t T) (n0 : u64) :
   result ((betree_List_t T) * (betree_List_t T))
@@ -131,7 +131,7 @@ Fixpoint betree_List_split_at
   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 ()) *)
 Definition betree_List_push_front
   (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
@@ -140,7 +140,7 @@ Definition betree_List_push_front
   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 *)
 Definition betree_List_pop_front
   (T : Type) (self : betree_List_t T) : result T :=
   let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -150,7 +150,7 @@ Definition betree_List_pop_front
   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 *)
 Definition betree_List_pop_front_back
   (T : Type) (self : betree_List_t T) : result (betree_List_t T) :=
   let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -160,7 +160,7 @@ Definition betree_List_pop_front_back
   end
 .
 
-(** [betree_main::betree::List::{1}::hd]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function *)
 Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
   match self with
   | Betree_List_Cons hd l => Return hd
@@ -168,8 +168,8 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
   end
 .
 
-(** [betree_main::betree::List::{2}::head_has_key]: forward function *)
-Definition betree_List_head_has_key
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function *)
+Definition betree_ListTupleU64T_head_has_key
   (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
   match self with
   | Betree_List_Cons hd l => let (i, _) := hd in Return (i s= key)
@@ -177,8 +177,8 @@ Definition betree_List_head_has_key
   end
 .
 
-(** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *)
-Fixpoint betree_List_partition_at_pivot
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function *)
+Fixpoint betree_ListTupleU64T_partition_at_pivot
   (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
   result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T)))
   :=
@@ -191,7 +191,7 @@ Fixpoint betree_List_partition_at_pivot
       if i s>= pivot
       then Return (Betree_List_Nil, Betree_List_Cons (i, t) tl)
       else (
-        p <- betree_List_partition_at_pivot T n0 tl pivot;
+        p <- betree_ListTupleU64T_partition_at_pivot T n0 tl pivot;
         let (ls0, ls1) := p in
         let l := ls0 in
         Return (Betree_List_Cons (i, t) l, ls1))
@@ -200,7 +200,7 @@ Fixpoint betree_List_partition_at_pivot
   end
 .
 
-(** [betree_main::betree::Leaf::{3}::split]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function *)
 Definition betree_Leaf_split
   (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -233,7 +233,7 @@ Definition betree_Leaf_split
   Return (st1, mkbetree_Internal_t self.(betree_Leaf_id) pivot n0 n1)
 .
 
-(** [betree_main::betree::Leaf::{3}::split]: backward function 2 *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 *)
 Definition betree_Leaf_split_back
   (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -254,7 +254,7 @@ Definition betree_Leaf_split_back
   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 *)
 Fixpoint betree_Node_lookup_first_message_for_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
@@ -273,7 +273,7 @@ Fixpoint betree_Node_lookup_first_message_for_key
   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 *)
 Fixpoint betree_Node_lookup_first_message_for_key_back
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t))
   (ret : betree_List_t (u64 * betree_Message_t)) :
@@ -296,7 +296,7 @@ Fixpoint betree_Node_lookup_first_message_for_key_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply_upserts]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function *)
 Fixpoint betree_Node_apply_upserts
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
@@ -305,7 +305,7 @@ Fixpoint betree_Node_apply_upserts
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    b <- betree_List_head_has_key betree_Message_t msgs key;
+    b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key;
     if b
     then (
       msg <- betree_List_pop_front (u64 * betree_Message_t) msgs;
@@ -328,7 +328,7 @@ Fixpoint betree_Node_apply_upserts
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 *)
 Fixpoint betree_Node_apply_upserts_back
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
@@ -337,7 +337,7 @@ Fixpoint betree_Node_apply_upserts_back
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    b <- betree_List_head_has_key betree_Message_t msgs key;
+    b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key;
     if b
     then (
       msg <- betree_List_pop_front (u64 * betree_Message_t) msgs;
@@ -358,7 +358,7 @@ Fixpoint betree_Node_apply_upserts_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function *)
 Fixpoint betree_Node_lookup_in_bindings
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result (option u64)
@@ -380,7 +380,7 @@ Fixpoint betree_Node_lookup_in_bindings
   end
 .
 
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function *)
 Fixpoint betree_Internal_lookup_in_children
   (n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
   result (state * (option u64))
@@ -393,7 +393,7 @@ Fixpoint betree_Internal_lookup_in_children
     else betree_Node_lookup n0 self.(betree_Internal_right) key st
   end
 
-(** [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 *)
 with betree_Internal_lookup_in_children_back
   (n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
   result betree_Internal_t
@@ -412,7 +412,7 @@ with betree_Internal_lookup_in_children_back
         self.(betree_Internal_pivot) self.(betree_Internal_left) n1))
   end
 
-(** [betree_main::betree::Node::{5}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function *)
 with betree_Node_lookup
   (n : nat) (self : betree_Node_t) (key : u64) (st : state) :
   result (state * (option u64))
@@ -483,7 +483,7 @@ with betree_Node_lookup
     end
   end
 
-(** [betree_main::betree::Node::{5}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 *)
 with betree_Node_lookup_back
   (n : nat) (self : betree_Node_t) (key : u64) (st : state) :
   result betree_Node_t
@@ -552,7 +552,7 @@ with betree_Node_lookup_back
   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 ()) *)
 Fixpoint betree_Node_filter_messages_for_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
@@ -576,7 +576,7 @@ Fixpoint betree_Node_filter_messages_for_key
   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 *)
 Fixpoint betree_Node_lookup_first_message_after_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
@@ -595,7 +595,7 @@ Fixpoint betree_Node_lookup_first_message_after_key
   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 *)
 Fixpoint betree_Node_lookup_first_message_after_key_back
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t))
   (ret : betree_List_t (u64 * betree_Message_t)) :
@@ -618,7 +618,7 @@ Fixpoint betree_Node_lookup_first_message_after_key_back
   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 ()) *)
 Definition betree_Node_apply_to_internal
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64)
@@ -626,7 +626,7 @@ Definition betree_Node_apply_to_internal
   result (betree_List_t (u64 * betree_Message_t))
   :=
   msgs0 <- betree_Node_lookup_first_message_for_key n key msgs;
-  b <- betree_List_head_has_key betree_Message_t msgs0 key;
+  b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs0 key;
   if b
   then
     match new_msg with
@@ -676,7 +676,7 @@ Definition betree_Node_apply_to_internal
     betree_Node_lookup_first_message_for_key_back n 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 ()) *)
 Fixpoint betree_Node_apply_messages_to_internal
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t))
@@ -696,7 +696,7 @@ Fixpoint betree_Node_apply_messages_to_internal
   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 *)
 Fixpoint betree_Node_lookup_mut_in_bindings
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result (betree_List_t (u64 * u64))
@@ -715,7 +715,7 @@ Fixpoint betree_Node_lookup_mut_in_bindings
   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 *)
 Fixpoint betree_Node_lookup_mut_in_bindings_back
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64))
   (ret : betree_List_t (u64 * u64)) :
@@ -737,7 +737,7 @@ Fixpoint betree_Node_lookup_mut_in_bindings_back
   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 ()) *)
 Definition betree_Node_apply_to_leaf
   (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64)
@@ -745,7 +745,7 @@ Definition betree_Node_apply_to_leaf
   result (betree_List_t (u64 * u64))
   :=
   bindings0 <- betree_Node_lookup_mut_in_bindings n key bindings;
-  b <- betree_List_head_has_key u64 bindings0 key;
+  b <- betree_ListTupleU64T_head_has_key u64 bindings0 key;
   if b
   then (
     hd <- betree_List_pop_front (u64 * u64) bindings0;
@@ -778,7 +778,7 @@ Definition betree_Node_apply_to_leaf
     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 ()) *)
 Fixpoint betree_Node_apply_messages_to_leaf
   (n : nat) (bindings : betree_List_t (u64 * u64))
@@ -798,7 +798,7 @@ Fixpoint betree_Node_apply_messages_to_leaf
   end
 .
 
-(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function *)
 Fixpoint betree_Internal_flush
   (n : nat) (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -809,7 +809,7 @@ Fixpoint betree_Internal_flush
   | O => Fail_ OutOfFuel
   | S n0 =>
     p <-
-      betree_List_partition_at_pivot betree_Message_t n0 content
+      betree_ListTupleU64T_partition_at_pivot betree_Message_t n0 content
         self.(betree_Internal_pivot);
     let (msgs_left, msgs_right) := p in
     len_left <- betree_List_len (u64 * betree_Message_t) n0 msgs_left;
@@ -846,7 +846,7 @@ Fixpoint betree_Internal_flush
       Return (st0, msgs_left))
   end
 
-(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+(** [betree_main::betree::{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_NodeIdCounter_t)
@@ -857,7 +857,7 @@ with betree_Internal_flush_back
   | O => Fail_ OutOfFuel
   | S n0 =>
     p <-
-      betree_List_partition_at_pivot betree_Message_t n0 content
+      betree_ListTupleU64T_partition_at_pivot betree_Message_t n0 content
         self.(betree_Internal_pivot);
     let (msgs_left, msgs_right) := p in
     len_left <- betree_List_len (u64 * betree_Message_t) n0 msgs_left;
@@ -894,7 +894,7 @@ with betree_Internal_flush_back
         node_id_cnt0))
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function *)
 with betree_Node_apply_messages
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -946,7 +946,7 @@ with betree_Node_apply_messages
     end
   end
 
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 *)
 with betree_Node_apply_messages_back
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -998,7 +998,7 @@ with betree_Node_apply_messages_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function *)
 Definition betree_Node_apply
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -1016,7 +1016,7 @@ Definition betree_Node_apply
   Return (st0, tt)
 .
 
-(** [betree_main::betree::Node::{5}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 *)
 Definition betree_Node_apply_back
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -1028,7 +1028,7 @@ Definition betree_Node_apply_back
     (key, new_msg) l) st
 .
 
-(** [betree_main::betree::BeTree::{6}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function *)
 Definition betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state * betree_BeTree_t)
@@ -1052,7 +1052,7 @@ Definition betree_BeTree_new
     |})
 .
 
-(** [betree_main::betree::BeTree::{6}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function *)
 Definition betree_BeTree_apply
   (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
   (st : state) :
@@ -1068,7 +1068,7 @@ Definition betree_BeTree_apply
   Return (st0, tt)
 .
 
-(** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 *)
 Definition betree_BeTree_apply_back
   (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
   (st : state) :
@@ -1086,7 +1086,7 @@ Definition betree_BeTree_apply_back
     |}
 .
 
-(** [betree_main::betree::BeTree::{6}::insert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function *)
 Definition betree_BeTree_insert
   (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result (state * unit)
@@ -1097,7 +1097,7 @@ Definition betree_BeTree_insert
   Return (st0, tt)
 .
 
-(** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 *)
 Definition betree_BeTree_insert_back
   (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result betree_BeTree_t
@@ -1105,7 +1105,7 @@ Definition betree_BeTree_insert_back
   betree_BeTree_apply_back n 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 *)
 Definition betree_BeTree_delete
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state * unit)
@@ -1116,7 +1116,7 @@ Definition betree_BeTree_delete
   Return (st0, tt)
 .
 
-(** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 *)
 Definition betree_BeTree_delete_back
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result betree_BeTree_t
@@ -1124,7 +1124,7 @@ Definition betree_BeTree_delete_back
   betree_BeTree_apply_back n 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 *)
 Definition betree_BeTree_upsert
   (n : nat) (self : betree_BeTree_t) (key : u64)
   (upd : betree_UpsertFunState_t) (st : state) :
@@ -1136,7 +1136,7 @@ Definition betree_BeTree_upsert
   Return (st0, tt)
 .
 
-(** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 *)
 Definition betree_BeTree_upsert_back
   (n : nat) (self : betree_BeTree_t) (key : u64)
   (upd : betree_UpsertFunState_t) (st : state) :
@@ -1145,7 +1145,7 @@ Definition betree_BeTree_upsert_back
   betree_BeTree_apply_back n 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 *)
 Definition betree_BeTree_lookup
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state * (option u64))
@@ -1153,7 +1153,7 @@ Definition betree_BeTree_lookup
   betree_Node_lookup n self.(betree_BeTree_root) key st
 .
 
-(** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 *)
 Definition betree_BeTree_lookup_back
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result betree_BeTree_t
diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v
index eade90de..bb798e71 100644
--- a/tests/coq/betree/BetreeMain_Opaque.v
+++ b/tests/coq/betree/BetreeMain_Opaque.v
@@ -32,7 +32,7 @@ Axiom 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 *)
 Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
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)
 
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 0901d449..441a3721 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -47,17 +47,17 @@ def betree.fresh_node_id (counter : U64) : Result U64 :=
 def betree.fresh_node_id_back (counter : U64) : Result U64 :=
   counter + 1#u64
 
-/- [betree_main::betree::NodeIdCounter::{0}::new]: forward function -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
   Result.ret { next_node_id := 0#u64 }
 
-/- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function -/
 def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 :=
   do
     let _ ← self.next_node_id + 1#u64
     Result.ret 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 -/
 def betree.NodeIdCounter.fresh_id_back
   (self : betree.NodeIdCounter) : Result betree.NodeIdCounter :=
   do
@@ -85,7 +85,7 @@ def betree.upsert_update
       then prev0 - v
       else Result.ret 0#u64
 
-/- [betree_main::betree::List::{1}::len]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function -/
 divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
   match self with
   | betree.List.Cons t tl => do
@@ -93,7 +93,7 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
                                1#u64 + i
   | betree.List.Nil => Result.ret 0#u64
 
-/- [betree_main::betree::List::{1}::split_at]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function -/
 divergent def betree.List.split_at
   (T : Type) (self : betree.List T) (n : U64) :
   Result ((betree.List T) × (betree.List T))
@@ -111,7 +111,7 @@ divergent def betree.List.split_at
         Result.ret (betree.List.Cons hd l, ls1)
     | betree.List.Nil => Result.fail Error.panic
 
-/- [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 ()) -/
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
@@ -119,14 +119,14 @@ def betree.List.push_front
   let l := tl
   Result.ret (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 -/
 def betree.List.pop_front (T : Type) (self : betree.List T) : Result T :=
   let ls := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret x
   | betree.List.Nil => Result.fail Error.panic
 
-/- [betree_main::betree::List::{1}::pop_front]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 -/
 def betree.List.pop_front_back
   (T : Type) (self : betree.List T) : Result (betree.List T) :=
   let ls := core.mem.replace (betree.List T) self betree.List.Nil
@@ -134,22 +134,22 @@ def betree.List.pop_front_back
   | betree.List.Cons x tl => Result.ret tl
   | betree.List.Nil => Result.fail Error.panic
 
-/- [betree_main::betree::List::{1}::hd]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function -/
 def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
   match self with
   | betree.List.Cons hd l => Result.ret hd
   | betree.List.Nil => Result.fail Error.panic
 
-/- [betree_main::betree::List::{2}::head_has_key]: forward function -/
-def betree.List.head_has_key
+/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function -/
+def betree.ListTupleU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
   match self with
   | betree.List.Cons hd l => let (i, _) := hd
                              Result.ret (i = key)
   | betree.List.Nil => Result.ret false
 
-/- [betree_main::betree::List::{2}::partition_at_pivot]: forward function -/
-divergent def betree.List.partition_at_pivot
+/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function -/
+divergent def betree.ListTupleU64T.partition_at_pivot
   (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
   Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
   :=
@@ -160,13 +160,13 @@ divergent def betree.List.partition_at_pivot
     then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl)
     else
       do
-        let p ← betree.List.partition_at_pivot T tl pivot
+        let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot
         let (ls0, ls1) := p
         let l := ls0
         Result.ret (betree.List.Cons (i, t) l, ls1)
   | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil)
 
-/- [betree_main::betree::Leaf::{3}::split]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function -/
 def betree.Leaf.split
   (self : betree.Leaf) (content : betree.List (U64 × U64))
   (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -186,7 +186,7 @@ def betree.Leaf.split
     let n0 := betree.Node.Leaf { id := id1, size := params.split_size }
     Result.ret (st1, betree.Internal.mk self.id pivot n n0)
 
-/- [betree_main::betree::Leaf::{3}::split]: backward function 2 -/
+/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 -/
 def betree.Leaf.split_back
   (self : betree.Leaf) (content : betree.List (U64 × U64))
   (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -203,7 +203,7 @@ 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_first_message_for_key]: forward function -/
+/- [betree_main::betree::{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)) :
   Result (betree.List (U64 × betree.Message))
@@ -216,7 +216,7 @@ divergent def betree.Node.lookup_first_message_for_key
     else betree.Node.lookup_first_message_for_key key next_msgs
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [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 -/
 divergent def betree.Node.lookup_first_message_for_key_back
   (key : U64) (msgs : betree.List (U64 × betree.Message))
   (ret0 : betree.List (U64 × betree.Message)) :
@@ -234,14 +234,14 @@ divergent def betree.Node.lookup_first_message_for_key_back
         Result.ret (betree.List.Cons (i, m) next_msgs0)
   | betree.List.Nil => Result.ret ret0
 
-/- [betree_main::betree::Node::{5}::apply_upserts]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function -/
 divergent def betree.Node.apply_upserts
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   (st : State) :
   Result (State × U64)
   :=
   do
-    let b ← betree.List.head_has_key betree.Message msgs key
+    let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
     if b
     then
       do
@@ -264,14 +264,14 @@ divergent def betree.Node.apply_upserts
             betree.Message.Insert v)
         Result.ret (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 -/
 divergent def betree.Node.apply_upserts_back
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   (st : State) :
   Result (betree.List (U64 × betree.Message))
   :=
   do
-    let b ← betree.List.head_has_key betree.Message msgs key
+    let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
     if b
     then
       do
@@ -292,7 +292,7 @@ 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 -/
+/- [betree_main::betree::{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
@@ -306,7 +306,7 @@ divergent def betree.Node.lookup_in_bindings
       else betree.Node.lookup_in_bindings key tl
   | betree.List.Nil => Result.ret none
 
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: forward function -/
+/- [betree_main::betree::{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))
@@ -316,7 +316,7 @@ mutual divergent def betree.Internal.lookup_in_children
   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 -/
+/- [betree_main::betree::{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
@@ -330,7 +330,7 @@ divergent def betree.Internal.lookup_in_children_back
       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 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function -/
 divergent def betree.Node.lookup
   (self : betree.Node) (key : U64) (st : State) :
   Result (State × (Option U64))
@@ -402,7 +402,7 @@ divergent def betree.Node.lookup
       let o ← betree.Node.lookup_in_bindings key bindings
       Result.ret (st0, o)
 
-/- [betree_main::betree::Node::{5}::lookup]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 -/
 divergent def betree.Node.lookup_back
   (self : betree.Node) (key : U64) (st : State) : Result betree.Node :=
   match self with
@@ -475,7 +475,7 @@ divergent def betree.Node.lookup_back
 
 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 ()) -/
 divergent def betree.Node.filter_messages_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -494,7 +494,7 @@ divergent def betree.Node.filter_messages_for_key
     else Result.ret (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [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 -/
 divergent def betree.Node.lookup_first_message_after_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
@@ -507,7 +507,7 @@ divergent def betree.Node.lookup_first_message_after_key
     else Result.ret (betree.List.Cons (k, m) next_msgs)
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [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 -/
 divergent def betree.Node.lookup_first_message_after_key_back
   (key : U64) (msgs : betree.List (U64 × betree.Message))
   (ret0 : betree.List (U64 × betree.Message)) :
@@ -525,7 +525,7 @@ divergent def betree.Node.lookup_first_message_after_key_back
     else Result.ret ret0
   | betree.List.Nil => Result.ret ret0
 
-/- [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 ()) -/
 def betree.Node.apply_to_internal
   (msgs : betree.List (U64 × betree.Message)) (key : U64)
@@ -534,7 +534,7 @@ def betree.Node.apply_to_internal
   :=
   do
     let msgs0 ← betree.Node.lookup_first_message_for_key key msgs
-    let b ← betree.List.head_has_key betree.Message msgs0 key
+    let b ← betree.ListTupleU64T.head_has_key betree.Message msgs0 key
     if b
     then
       match new_msg with
@@ -591,7 +591,7 @@ def betree.Node.apply_to_internal
           betree.List.push_front (U64 × betree.Message) msgs0 (key, new_msg)
         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 ()) -/
 divergent def betree.Node.apply_messages_to_internal
   (msgs : betree.List (U64 × betree.Message))
@@ -606,7 +606,7 @@ 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 -/
+/- [betree_main::betree::{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))
@@ -619,7 +619,7 @@ divergent def betree.Node.lookup_mut_in_bindings
     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 -/
+/- [betree_main::betree::{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)) :
@@ -636,7 +636,7 @@ divergent def betree.Node.lookup_mut_in_bindings_back
         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
+/- [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 ()) -/
 def betree.Node.apply_to_leaf
   (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
@@ -645,7 +645,7 @@ def betree.Node.apply_to_leaf
   :=
   do
     let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings
-    let b ← betree.List.head_has_key U64 bindings0 key
+    let b ← betree.ListTupleU64T.head_has_key U64 bindings0 key
     if b
     then
       do
@@ -685,7 +685,7 @@ def betree.Node.apply_to_leaf
             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
+/- [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 ()) -/
 divergent def betree.Node.apply_messages_to_leaf
   (bindings : betree.List (U64 × U64))
@@ -700,7 +700,7 @@ divergent def betree.Node.apply_messages_to_leaf
       betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl
   | betree.List.Nil => Result.ret bindings
 
-/- [betree_main::betree::Internal::{4}::flush]: forward function -/
+/- [betree_main::betree::{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)
@@ -709,7 +709,7 @@ mutual divergent def betree.Internal.flush
   :=
   do
     let ⟨ _, i, n, n0 ⟩ := self
-    let p ← betree.List.partition_at_pivot betree.Message content i
+    let p ← betree.ListTupleU64T.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
@@ -738,7 +738,7 @@ mutual divergent def betree.Internal.flush
           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 -/
+/- [betree_main::betree::{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)
@@ -747,7 +747,7 @@ divergent def betree.Internal.flush_back
   :=
   do
     let ⟨ i, i0, n, n0 ⟩ := self
-    let p ← betree.List.partition_at_pivot betree.Message content i0
+    let p ← betree.ListTupleU64T.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
@@ -772,7 +772,7 @@ divergent def betree.Internal.flush_back
           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 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function -/
 divergent def betree.Node.apply_messages
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -820,7 +820,7 @@ divergent def betree.Node.apply_messages
           let (st1, _) ← betree.store_leaf_node node.id content0 st0
           Result.ret (st1, ())
 
-/- [betree_main::betree::Node::{5}::apply_messages]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 -/
 divergent def betree.Node.apply_messages_back
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -874,7 +874,7 @@ divergent def betree.Node.apply_messages_back
 
 end
 
-/- [betree_main::betree::Node::{5}::apply]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function -/
 def betree.Node.apply
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -891,7 +891,7 @@ def betree.Node.apply
         (key, new_msg) l) st
     Result.ret (st0, ())
 
-/- [betree_main::betree::Node::{5}::apply]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 -/
 def betree.Node.apply_back
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -902,7 +902,7 @@ def 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 -/
 def betree.BeTree.new
   (min_flush_size : U64) (split_size : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -920,7 +920,7 @@ def betree.BeTree.new
         root := (betree.Node.Leaf { id := id, size := 0#u64 })
       })
 
-/- [betree_main::betree::BeTree::{6}::apply]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function -/
 def betree.BeTree.apply
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
   Result (State × Unit)
@@ -932,7 +932,7 @@ def betree.BeTree.apply
       betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
     Result.ret (st0, ())
 
-/- [betree_main::betree::BeTree::{6}::apply]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 -/
 def betree.BeTree.apply_back
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
   Result betree.BeTree
@@ -942,7 +942,7 @@ def betree.BeTree.apply_back
       betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
     Result.ret { 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 -/
 def betree.BeTree.insert
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
   Result (State × Unit)
@@ -954,14 +954,14 @@ def betree.BeTree.insert
       betree.BeTree.apply_back self key (betree.Message.Insert value) st
     Result.ret (st0, ())
 
-/- [betree_main::betree::BeTree::{6}::insert]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 -/
 def betree.BeTree.insert_back
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
   Result betree.BeTree
   :=
   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 -/
 def betree.BeTree.delete
   (self : betree.BeTree) (key : U64) (st : State) : Result (State × Unit) :=
   do
@@ -969,12 +969,12 @@ def betree.BeTree.delete
     let _ ← betree.BeTree.apply_back self key betree.Message.Delete st
     Result.ret (st0, ())
 
-/- [betree_main::betree::BeTree::{6}::delete]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 -/
 def betree.BeTree.delete_back
   (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
   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 -/
 def betree.BeTree.upsert
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
   :
@@ -986,7 +986,7 @@ def betree.BeTree.upsert
     let _ ← betree.BeTree.apply_back self key (betree.Message.Upsert upd) st
     Result.ret (st0, ())
 
-/- [betree_main::betree::BeTree::{6}::upsert]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 -/
 def betree.BeTree.upsert_back
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
   :
@@ -994,14 +994,14 @@ def 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 -/
 def betree.BeTree.lookup
   (self : betree.BeTree) (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 -/
 def betree.BeTree.lookup_back
   (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
   do
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean
index 430d2dda..1dc3af0e 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/BetreeMain/FunsExternal_Template.lean
@@ -24,7 +24,7 @@ axiom betree_utils.load_leaf_node
 axiom betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit)
 
-/- [core::option::Option::{0}::unwrap]: forward function -/
+/- [core::option::{core::option::Option<T>}::unwrap]: forward function -/
 axiom core.option.Option.unwrap
   (T : Type) : Option T → State → Result (State × T)