Merge pull request #45 from AeneasVerif/son_merge_types

Big cleanup

4 files changed, 203 insertions, 125 deletions

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 261e8270..8e48b17d 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -12,7 +12,8 @@ Require Export BetreeMain_Opaque.
 Import BetreeMain_Opaque.
 Module BetreeMain_Funs.
 
-(** [betree_main::betree::load_internal_node]: forward function *)
+(** [betree_main::betree::load_internal_node]: forward function
+    Source: 'src/betree.rs', lines 36:0-36:52 *)
 Definition betree_load_internal_node
   (id : u64) (st : state) :
   result (state * (betree_List_t (u64 * betree_Message_t)))
@@ -20,7 +21,8 @@ Definition betree_load_internal_node
   betree_utils_load_internal_node id st
 .
 
-(** [betree_main::betree::store_internal_node]: forward function *)
+(** [betree_main::betree::store_internal_node]: forward function
+    Source: 'src/betree.rs', lines 41:0-41:60 *)
 Definition betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) :
   result (state * unit)
@@ -30,13 +32,15 @@ Definition betree_store_internal_node
   Return (st0, tt)
 .
 
-(** [betree_main::betree::load_leaf_node]: forward function *)
+(** [betree_main::betree::load_leaf_node]: forward function
+    Source: 'src/betree.rs', lines 46:0-46:44 *)
 Definition betree_load_leaf_node
   (id : u64) (st : state) : result (state * (betree_List_t (u64 * u64))) :=
   betree_utils_load_leaf_node id st
 .
 
-(** [betree_main::betree::store_leaf_node]: forward function *)
+(** [betree_main::betree::store_leaf_node]: forward function
+    Source: 'src/betree.rs', lines 51:0-51:52 *)
 Definition betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 * u64)) (st : state) :
   result (state * unit)
@@ -46,36 +50,42 @@ Definition betree_store_leaf_node
   Return (st0, tt)
 .
 
-(** [betree_main::betree::fresh_node_id]: forward function *)
+(** [betree_main::betree::fresh_node_id]: forward function
+    Source: 'src/betree.rs', lines 55:0-55:48 *)
 Definition betree_fresh_node_id (counter : u64) : result u64 :=
   _ <- u64_add counter 1%u64; Return counter
 .
 
-(** [betree_main::betree::fresh_node_id]: backward function 0 *)
+(** [betree_main::betree::fresh_node_id]: backward function 0
+    Source: 'src/betree.rs', lines 55:0-55:48 *)
 Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
   u64_add counter 1%u64
 .
 
-(** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function
+    Source: 'src/betree.rs', lines 206:4-206:20 *)
 Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
   Return {| betree_NodeIdCounter_next_node_id := 0%u64 |}
 .
 
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function
+    Source: 'src/betree.rs', lines 210:4-210:36 *)
 Definition betree_NodeIdCounter_fresh_id
   (self : betree_NodeIdCounter_t) : result u64 :=
   _ <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
   Return self.(betree_NodeIdCounter_next_node_id)
 .
 
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0
+    Source: 'src/betree.rs', lines 210:4-210:36 *)
 Definition betree_NodeIdCounter_fresh_id_back
   (self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t :=
   i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
   Return {| betree_NodeIdCounter_next_node_id := i |}
 .
 
-(** [betree_main::betree::upsert_update]: forward function *)
+(** [betree_main::betree::upsert_update]: forward function
+    Source: 'src/betree.rs', lines 234:0-234:70 *)
 Definition betree_upsert_update
   (prev : option u64) (st : betree_UpsertFunState_t) : result u64 :=
   match prev with
@@ -95,7 +105,8 @@ 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
+    Source: 'src/betree.rs', lines 276:4-276:24 *)
 Fixpoint betree_List_len
   (T : Type) (n : nat) (self : betree_List_t T) : result u64 :=
   match n with
@@ -108,7 +119,8 @@ 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
+    Source: 'src/betree.rs', lines 284:4-284:51 *)
 Fixpoint betree_List_split_at
   (T : Type) (n : nat) (self : betree_List_t T) (n0 : u64) :
   result ((betree_List_t T) * (betree_List_t T))
@@ -131,8 +143,9 @@ Fixpoint betree_List_split_at
   end
 .
 
-(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 299:4-299:34 *)
 Definition betree_List_push_front
   (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
   let tl := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -140,7 +153,8 @@ 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
+    Source: 'src/betree.rs', lines 306:4-306:32 *)
 Definition betree_List_pop_front
   (T : Type) (self : betree_List_t T) : result T :=
   let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -150,7 +164,8 @@ 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
+    Source: 'src/betree.rs', lines 306:4-306:32 *)
 Definition betree_List_pop_front_back
   (T : Type) (self : betree_List_t T) : result (betree_List_t T) :=
   let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -160,7 +175,8 @@ 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
+    Source: 'src/betree.rs', lines 318:4-318:22 *)
 Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
   match self with
   | Betree_List_Cons hd l => Return hd
@@ -168,8 +184,9 @@ 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
+    Source: 'src/betree.rs', lines 327:4-327:44 *)
+Definition betree_ListTupleU64T_head_has_key
   (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
   match self with
   | Betree_List_Cons hd l => let (i, _) := hd in Return (i s= key)
@@ -177,8 +194,9 @@ 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
+    Source: 'src/betree.rs', lines 339:4-339:73 *)
+Fixpoint betree_ListTupleU64T_partition_at_pivot
   (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
   result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T)))
   :=
@@ -191,7 +209,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 +218,8 @@ 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
+    Source: 'src/betree.rs', lines 359:4-364:17 *)
 Definition betree_Leaf_split
   (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -233,7 +252,8 @@ 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
+    Source: 'src/betree.rs', lines 359:4-364:17 *)
 Definition betree_Leaf_split_back
   (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -254,7 +274,8 @@ 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
+    Source: 'src/betree.rs', lines 789:4-792:34 *)
 Fixpoint betree_Node_lookup_first_message_for_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
@@ -273,7 +294,8 @@ 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
+    Source: 'src/betree.rs', lines 789:4-792:34 *)
 Fixpoint betree_Node_lookup_first_message_for_key_back
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t))
   (ret : betree_List_t (u64 * betree_Message_t)) :
@@ -296,7 +318,8 @@ 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
+    Source: 'src/betree.rs', lines 819:4-819:90 *)
 Fixpoint betree_Node_apply_upserts
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
@@ -305,7 +328,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 +351,8 @@ 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
+    Source: 'src/betree.rs', lines 819:4-819:90 *)
 Fixpoint betree_Node_apply_upserts_back
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
   (key : u64) (st : state) :
@@ -337,7 +361,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 +382,8 @@ 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
+    Source: 'src/betree.rs', lines 636:4-636:80 *)
 Fixpoint betree_Node_lookup_in_bindings
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result (option u64)
@@ -380,7 +405,8 @@ 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
+    Source: 'src/betree.rs', lines 395:4-395:63 *)
 Fixpoint betree_Internal_lookup_in_children
   (n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
   result (state * (option u64))
@@ -393,7 +419,8 @@ 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
+    Source: 'src/betree.rs', lines 395:4-395:63 *)
 with betree_Internal_lookup_in_children_back
   (n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
   result betree_Internal_t
@@ -412,7 +439,8 @@ 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
+    Source: 'src/betree.rs', lines 709:4-709:58 *)
 with betree_Node_lookup
   (n : nat) (self : betree_Node_t) (key : u64) (st : state) :
   result (state * (option u64))
@@ -483,7 +511,8 @@ 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
+    Source: 'src/betree.rs', lines 709:4-709:58 *)
 with betree_Node_lookup_back
   (n : nat) (self : betree_Node_t) (key : u64) (st : state) :
   result betree_Node_t
@@ -552,8 +581,9 @@ with betree_Node_lookup_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+(** [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 ())
+    Source: 'src/betree.rs', lines 674:4-674:77 *)
 Fixpoint betree_Node_filter_messages_for_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
@@ -576,7 +606,8 @@ 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
+    Source: 'src/betree.rs', lines 689:4-692:34 *)
 Fixpoint betree_Node_lookup_first_message_after_key
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
@@ -595,7 +626,8 @@ 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
+    Source: 'src/betree.rs', lines 689:4-692:34 *)
 Fixpoint betree_Node_lookup_first_message_after_key_back
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t))
   (ret : betree_List_t (u64 * betree_Message_t)) :
@@ -618,15 +650,16 @@ Fixpoint betree_Node_lookup_first_message_after_key_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 521:4-521:89 *)
 Definition betree_Node_apply_to_internal
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64)
   (new_msg : betree_Message_t) :
   result (betree_List_t (u64 * betree_Message_t))
   :=
   msgs0 <- betree_Node_lookup_first_message_for_key n key msgs;
-  b <- betree_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,8 +709,9 @@ 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
-    (there is a single backward function, and the forward function returns ()) *)
+(** [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 ())
+    Source: 'src/betree.rs', lines 502:4-505:5 *)
 Fixpoint betree_Node_apply_messages_to_internal
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t))
   (new_msgs : betree_List_t (u64 * betree_Message_t)) :
@@ -696,7 +730,8 @@ 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
+    Source: 'src/betree.rs', lines 653:4-656:32 *)
 Fixpoint betree_Node_lookup_mut_in_bindings
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result (betree_List_t (u64 * u64))
@@ -715,7 +750,8 @@ 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
+    Source: 'src/betree.rs', lines 653:4-656:32 *)
 Fixpoint betree_Node_lookup_mut_in_bindings_back
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64))
   (ret : betree_List_t (u64 * u64)) :
@@ -737,15 +773,16 @@ Fixpoint betree_Node_lookup_mut_in_bindings_back
   end
 .
 
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
+    (there is a single backward function, and the forward function returns ())
+    Source: 'src/betree.rs', lines 460:4-460:87 *)
 Definition betree_Node_apply_to_leaf
   (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64)
   (new_msg : betree_Message_t) :
   result (betree_List_t (u64 * u64))
   :=
   bindings0 <- betree_Node_lookup_mut_in_bindings n key bindings;
-  b <- betree_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,8 +815,9 @@ Definition betree_Node_apply_to_leaf
     end
 .
 
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ()) *)
+(** [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 ())
+    Source: 'src/betree.rs', lines 444:4-447:5 *)
 Fixpoint betree_Node_apply_messages_to_leaf
   (n : nat) (bindings : betree_List_t (u64 * u64))
   (new_msgs : betree_List_t (u64 * betree_Message_t)) :
@@ -798,7 +836,8 @@ 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
+    Source: 'src/betree.rs', lines 410:4-415:26 *)
 Fixpoint betree_Internal_flush
   (n : nat) (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -809,7 +848,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 +885,8 @@ 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
+    Source: 'src/betree.rs', lines 410:4-415:26 *)
 with betree_Internal_flush_back
   (n : nat) (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -857,7 +897,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 +934,8 @@ 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
+    Source: 'src/betree.rs', lines 588:4-593:5 *)
 with betree_Node_apply_messages
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -946,7 +987,8 @@ 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
+    Source: 'src/betree.rs', lines 588:4-593:5 *)
 with betree_Node_apply_messages_back
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -998,7 +1040,8 @@ 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
+    Source: 'src/betree.rs', lines 576:4-582:5 *)
 Definition betree_Node_apply
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -1016,7 +1059,8 @@ 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
+    Source: 'src/betree.rs', lines 576:4-582:5 *)
 Definition betree_Node_apply_back
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -1028,7 +1072,8 @@ 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
+    Source: 'src/betree.rs', lines 849:4-849:60 *)
 Definition betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state * betree_BeTree_t)
@@ -1052,7 +1097,8 @@ Definition betree_BeTree_new
     |})
 .
 
-(** [betree_main::betree::BeTree::{6}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function
+    Source: 'src/betree.rs', lines 868:4-868:47 *)
 Definition betree_BeTree_apply
   (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
   (st : state) :
@@ -1068,7 +1114,8 @@ 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
+    Source: 'src/betree.rs', lines 868:4-868:47 *)
 Definition betree_BeTree_apply_back
   (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
   (st : state) :
@@ -1086,7 +1133,8 @@ Definition betree_BeTree_apply_back
     |}
 .
 
-(** [betree_main::betree::BeTree::{6}::insert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function
+    Source: 'src/betree.rs', lines 874:4-874:52 *)
 Definition betree_BeTree_insert
   (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result (state * unit)
@@ -1097,7 +1145,8 @@ 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
+    Source: 'src/betree.rs', lines 874:4-874:52 *)
 Definition betree_BeTree_insert_back
   (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result betree_BeTree_t
@@ -1105,7 +1154,8 @@ 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
+    Source: 'src/betree.rs', lines 880:4-880:38 *)
 Definition betree_BeTree_delete
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state * unit)
@@ -1116,7 +1166,8 @@ 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
+    Source: 'src/betree.rs', lines 880:4-880:38 *)
 Definition betree_BeTree_delete_back
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result betree_BeTree_t
@@ -1124,7 +1175,8 @@ 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
+    Source: 'src/betree.rs', lines 886:4-886:59 *)
 Definition betree_BeTree_upsert
   (n : nat) (self : betree_BeTree_t) (key : u64)
   (upd : betree_UpsertFunState_t) (st : state) :
@@ -1136,7 +1188,8 @@ 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
+    Source: 'src/betree.rs', lines 886:4-886:59 *)
 Definition betree_BeTree_upsert_back
   (n : nat) (self : betree_BeTree_t) (key : u64)
   (upd : betree_UpsertFunState_t) (st : state) :
@@ -1145,7 +1198,8 @@ 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
+    Source: 'src/betree.rs', lines 895:4-895:62 *)
 Definition betree_BeTree_lookup
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state * (option u64))
@@ -1153,7 +1207,8 @@ 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
+    Source: 'src/betree.rs', lines 895:4-895:62 *)
 Definition betree_BeTree_lookup_back
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result betree_BeTree_t
@@ -1167,7 +1222,8 @@ Definition betree_BeTree_lookup_back
     |}
 .
 
-(** [betree_main::main]: forward function *)
+(** [betree_main::main]: forward function
+    Source: 'src/betree_main.rs', lines 5:0-5:9 *)
 Definition main : result unit :=
   Return tt.
 
diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v
index eade90de..a065c8a3 100644
--- a/tests/coq/betree/BetreeMain_Opaque.v
+++ b/tests/coq/betree/BetreeMain_Opaque.v
@@ -10,29 +10,34 @@ Require Export BetreeMain_Types.
 Import BetreeMain_Types.
 Module BetreeMain_Opaque.
 
-(** [betree_main::betree_utils::load_internal_node]: forward function *)
+(** [betree_main::betree_utils::load_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 98:0-98:63 *)
 Axiom betree_utils_load_internal_node
   : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t)))
 .
 
-(** [betree_main::betree_utils::store_internal_node]: forward function *)
+(** [betree_main::betree_utils::store_internal_node]: forward function
+    Source: 'src/betree_utils.rs', lines 115:0-115:71 *)
 Axiom betree_utils_store_internal_node
   :
   u64 -> betree_List_t (u64 * betree_Message_t) -> state -> result (state *
     unit)
 .
 
-(** [betree_main::betree_utils::load_leaf_node]: forward function *)
+(** [betree_main::betree_utils::load_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 132:0-132:55 *)
 Axiom betree_utils_load_leaf_node
   : u64 -> state -> result (state * (betree_List_t (u64 * u64)))
 .
 
-(** [betree_main::betree_utils::store_leaf_node]: forward function *)
+(** [betree_main::betree_utils::store_leaf_node]: forward function
+    Source: 'src/betree_utils.rs', lines 145:0-145:63 *)
 Axiom betree_utils_store_leaf_node
   : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit)
 .
 
-(** [core::option::Option::{0}::unwrap]: forward function *)
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
 Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
index 933a670c..b729d1c3 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -8,7 +8,8 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Module BetreeMain_Types.
 
-(** [betree_main::betree::List] *)
+(** [betree_main::betree::List]
+    Source: 'src/betree.rs', lines 17:0-17:23 *)
 Inductive betree_List_t (T : Type) :=
 | Betree_List_Cons : T -> betree_List_t T -> betree_List_t T
 | Betree_List_Nil : betree_List_t T
@@ -17,27 +18,31 @@ Inductive betree_List_t (T : Type) :=
 Arguments Betree_List_Cons { _ }.
 Arguments Betree_List_Nil { _ }.
 
-(** [betree_main::betree::UpsertFunState] *)
+(** [betree_main::betree::UpsertFunState]
+    Source: 'src/betree.rs', lines 63:0-63:23 *)
 Inductive betree_UpsertFunState_t :=
 | Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t
 | Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t
 .
 
-(** [betree_main::betree::Message] *)
+(** [betree_main::betree::Message]
+    Source: 'src/betree.rs', lines 69:0-69:23 *)
 Inductive betree_Message_t :=
 | Betree_Message_Insert : u64 -> betree_Message_t
 | Betree_Message_Delete : betree_Message_t
 | Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t
 .
 
-(** [betree_main::betree::Leaf] *)
+(** [betree_main::betree::Leaf]
+    Source: 'src/betree.rs', lines 167:0-167:11 *)
 Record betree_Leaf_t :=
 mkbetree_Leaf_t {
   betree_Leaf_id : u64; betree_Leaf_size : u64;
 }
 .
 
-(** [betree_main::betree::Internal] *)
+(** [betree_main::betree::Internal]
+    Source: 'src/betree.rs', lines 156:0-156:15 *)
 Inductive betree_Internal_t :=
 | mkbetree_Internal_t :
   u64 ->
@@ -46,7 +51,8 @@ Inductive betree_Internal_t :=
   betree_Node_t ->
   betree_Internal_t
 
-(** [betree_main::betree::Node] *)
+(** [betree_main::betree::Node]
+    Source: 'src/betree.rs', lines 179:0-179:9 *)
 with betree_Node_t :=
 | Betree_Node_Internal : betree_Internal_t -> betree_Node_t
 | Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t
@@ -81,21 +87,24 @@ Notation "x1 .(betree_Internal_right)" := (betree_Internal_right x1)
   (at level 9)
 .
 
-(** [betree_main::betree::Params] *)
+(** [betree_main::betree::Params]
+    Source: 'src/betree.rs', lines 187:0-187:13 *)
 Record betree_Params_t :=
 mkbetree_Params_t {
   betree_Params_min_flush_size : u64; betree_Params_split_size : u64;
 }
 .
 
-(** [betree_main::betree::NodeIdCounter] *)
+(** [betree_main::betree::NodeIdCounter]
+    Source: 'src/betree.rs', lines 201:0-201:20 *)
 Record betree_NodeIdCounter_t :=
 mkbetree_NodeIdCounter_t {
   betree_NodeIdCounter_next_node_id : u64;
 }
 .
 
-(** [betree_main::betree::BeTree] *)
+(** [betree_main::betree::BeTree]
+    Source: 'src/betree.rs', lines 218:0-218:17 *)
 Record betree_BeTree_t :=
 mkbetree_BeTree_t {
   betree_BeTree_params : betree_Params_t;
diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index 85e38f01..83f860b6 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -467,14 +467,14 @@ Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result T := Return x.
 Definition alloc_boxed_Box_deref_mut_back (T : Type) (_ : T) (x : T) : result T := Return x.
 
 (* Trait instance *)
-Definition alloc_boxed_Box_coreOpsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
+Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
   core_ops_deref_Deref_target := Self;
   core_ops_deref_Deref_deref := alloc_boxed_Box_deref Self;
 |}.
 
 (* Trait instance *)
-Definition alloc_boxed_Box_coreOpsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {|
-  core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreOpsDerefInst Self;
+Definition alloc_boxed_Box_coreopsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {|
+  core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreopsDerefInst Self;
   core_ops_deref_DerefMut_deref_mut := alloc_boxed_Box_deref_mut Self;
   core_ops_deref_DerefMut_deref_mut_back := alloc_boxed_Box_deref_mut_back Self;
 |}.
@@ -576,7 +576,7 @@ Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T)
     else Fail_ Failure).
 
 (* Helper *)
-Axiom alloc_vec_Vec_index_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result T.
+Axiom alloc_vec_Vec_index_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize), result T.
 
 (* Helper *)
 Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result (alloc_vec_Vec T).
@@ -620,18 +620,18 @@ Definition core_slice_index_Slice_index
   end.
 
 (* [core::slice::index::Range:::get]: forward function *)
-Axiom core_slice_index_Range_get : forall (T : Type) (i : core_ops_range_Range usize) (s : slice T), result (option (slice T)).
+Axiom core_slice_index_RangeUsize_get : forall (T : Type) (i : core_ops_range_Range usize) (s : slice T), result (option (slice T)).
 
 (* [core::slice::index::Range::get_mut]: forward function *)
-Axiom core_slice_index_Range_get_mut :
+Axiom core_slice_index_RangeUsize_get_mut :
   forall (T : Type), core_ops_range_Range usize -> slice T -> result (option (slice T)).
 
 (* [core::slice::index::Range::get_mut]: backward function 0 *)
-Axiom core_slice_index_Range_get_mut_back :
+Axiom core_slice_index_RangeUsize_get_mut_back :
   forall (T : Type), core_ops_range_Range usize -> slice T -> option (slice T) -> result (slice T).
 
 (* [core::slice::index::Range::get_unchecked]: forward function *)
-Definition core_slice_index_Range_get_unchecked
+Definition core_slice_index_RangeUsize_get_unchecked
   (T : Type) :
   core_ops_range_Range usize -> const_raw_ptr (slice T) -> result (const_raw_ptr (slice T)) :=
   (* Don't know what the model should be - for now we always fail to make
@@ -639,7 +639,7 @@ Definition core_slice_index_Range_get_unchecked
   fun _ _ => Fail_ Failure.
 
 (* [core::slice::index::Range::get_unchecked_mut]: forward function *)
-Definition core_slice_index_Range_get_unchecked_mut
+Definition core_slice_index_RangeUsize_get_unchecked_mut
   (T : Type) :
   core_ops_range_Range usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr (slice T)) :=
   (* Don't know what the model should be - for now we always fail to make
@@ -647,15 +647,15 @@ Definition core_slice_index_Range_get_unchecked_mut
   fun _ _ => Fail_ Failure.
 
 (* [core::slice::index::Range::index]: forward function *)
-Axiom core_slice_index_Range_index :
+Axiom core_slice_index_RangeUsize_index :
   forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T).
 
 (* [core::slice::index::Range::index_mut]: forward function *)
-Axiom core_slice_index_Range_index_mut :
+Axiom core_slice_index_RangeUsize_index_mut :
   forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T).
 
 (* [core::slice::index::Range::index_mut]: backward function 0 *)
-Axiom core_slice_index_Range_index_mut_back :
+Axiom core_slice_index_RangeUsize_index_mut_back :
   forall (T : Type), core_ops_range_Range usize -> slice T -> slice T -> result (slice T).
 
 (* [core::slice::index::[T]::index_mut]: forward function *)
@@ -683,44 +683,44 @@ Axiom core_array_Array_index_mut_back :
   forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx)
   (a : array T N) (i : Idx) (x : inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output)), result (array T N).
 
-(* Trait implementation: [core::slice::index::[T]] *)
-Definition core_slice_index_Slice_coreopsindexIndexInst (T Idx : Type)
-  (inst : core_slice_index_SliceIndex Idx (slice T)) :
-  core_ops_index_Index (slice T) Idx := {|
-  core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output);
-  core_ops_index_Index_index := core_slice_index_Slice_index T Idx inst;
-|}.
-
 (* Trait implementation: [core::slice::index::private_slice_index::Range] *)
-Definition core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst
+Definition core_slice_index_private_slice_index_SealedRangeUsizeInst
   : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt.
 
 (* Trait implementation: [core::slice::index::Range] *)
-Definition core_slice_index_Range_coresliceindexSliceIndexInst (T : Type) :
+Definition core_slice_index_SliceIndexRangeUsizeSliceTInst (T : Type) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst;
+  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst;
   core_slice_index_SliceIndex_Output := slice T;
-  core_slice_index_SliceIndex_get := core_slice_index_Range_get T;
-  core_slice_index_SliceIndex_get_mut := core_slice_index_Range_get_mut T;
-  core_slice_index_SliceIndex_get_mut_back := core_slice_index_Range_get_mut_back T;
-  core_slice_index_SliceIndex_get_unchecked := core_slice_index_Range_get_unchecked T;
-  core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_Range_get_unchecked_mut T;
-  core_slice_index_SliceIndex_index := core_slice_index_Range_index T;
-  core_slice_index_SliceIndex_index_mut := core_slice_index_Range_index_mut T;
-  core_slice_index_SliceIndex_index_mut_back := core_slice_index_Range_index_mut_back T;
+  core_slice_index_SliceIndex_get := core_slice_index_RangeUsize_get T;
+  core_slice_index_SliceIndex_get_mut := core_slice_index_RangeUsize_get_mut T;
+  core_slice_index_SliceIndex_get_mut_back := core_slice_index_RangeUsize_get_mut_back T;
+  core_slice_index_SliceIndex_get_unchecked := core_slice_index_RangeUsize_get_unchecked T;
+  core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_RangeUsize_get_unchecked_mut T;
+  core_slice_index_SliceIndex_index := core_slice_index_RangeUsize_index T;
+  core_slice_index_SliceIndex_index_mut := core_slice_index_RangeUsize_index_mut T;
+  core_slice_index_SliceIndex_index_mut_back := core_slice_index_RangeUsize_index_mut_back T;
+|}.
+
+(* Trait implementation: [core::slice::index::[T]] *)
+Definition core_ops_index_IndexSliceTIInst (T Idx : Type)
+  (inst : core_slice_index_SliceIndex Idx (slice T)) :
+  core_ops_index_Index (slice T) Idx := {|
+  core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output);
+  core_ops_index_Index_index := core_slice_index_Slice_index T Idx inst;
 |}.
 
 (* Trait implementation: [core::slice::index::[T]] *)
-Definition core_slice_index_Slice_coreopsindexIndexMutInst (T Idx : Type)
+Definition core_ops_index_IndexMutSliceTIInst (T Idx : Type)
   (inst : core_slice_index_SliceIndex Idx (slice T)) :
   core_ops_index_IndexMut (slice T) Idx := {|
-  core_ops_index_IndexMut_indexInst := core_slice_index_Slice_coreopsindexIndexInst T Idx inst;
+  core_ops_index_IndexMut_indexInst := core_ops_index_IndexSliceTIInst T Idx inst;
   core_ops_index_IndexMut_index_mut := core_slice_index_Slice_index_mut T Idx inst;
   core_ops_index_IndexMut_index_mut_back := core_slice_index_Slice_index_mut_back T Idx inst;
 |}.
 
 (* Trait implementation: [core::array::[T; N]] *)
-Definition core_array_Array_coreopsindexIndexInst (T Idx : Type) (N : usize)
+Definition core_ops_index_IndexArrayInst (T Idx : Type) (N : usize)
   (inst : core_ops_index_Index (slice T) Idx) :
   core_ops_index_Index (array T N) Idx := {|
   core_ops_index_Index_Output := inst.(core_ops_index_Index_Output);
@@ -728,10 +728,10 @@ Definition core_array_Array_coreopsindexIndexInst (T Idx : Type) (N : usize)
 |}.
 
 (* Trait implementation: [core::array::[T; N]] *)
-Definition core_array_Array_coreopsindexIndexMutInst (T Idx : Type) (N : usize)
+Definition core_ops_index_IndexMutArrayInst (T Idx : Type) (N : usize)
   (inst : core_ops_index_IndexMut (slice T) Idx) :
   core_ops_index_IndexMut (array T N) Idx := {|
-  core_ops_index_IndexMut_indexInst := core_array_Array_coreopsindexIndexInst T Idx N inst.(core_ops_index_IndexMut_indexInst);
+  core_ops_index_IndexMut_indexInst := core_ops_index_IndexArrayInst T Idx N inst.(core_ops_index_IndexMut_indexInst);
   core_ops_index_IndexMut_index_mut := core_array_Array_index_mut T Idx N inst;
   core_ops_index_IndexMut_index_mut_back := core_array_Array_index_mut_back T Idx N inst;
 |}.
@@ -765,13 +765,13 @@ Axiom core_slice_index_usize_index_mut_back :
   forall (T : Type), usize -> slice T -> T -> result (slice T).
 
 (* Trait implementation: [core::slice::index::private_slice_index::usize] *)
-Definition core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst
+Definition core_slice_index_private_slice_index_SealedUsizeInst
   : core_slice_index_private_slice_index_Sealed usize := tt.
 
 (* Trait implementation: [core::slice::index::usize] *)
-Definition core_slice_index_usize_coresliceindexSliceIndexInst (T : Type) :
+Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) :
   core_slice_index_SliceIndex usize (slice T) := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst;
+  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
   core_slice_index_SliceIndex_Output := T;
   core_slice_index_SliceIndex_get := core_slice_index_usize_get T;
   core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut T;
@@ -815,8 +815,16 @@ Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type)
 
 (*** Theorems *)
 
+Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
+  alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
+    alloc_vec_Vec_index_usize v i.
+
+Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
+  alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
+    alloc_vec_Vec_index_usize v i.
+
 Axiom alloc_vec_Vec_index_mut_back_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
-  alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x =
+  alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x =
     alloc_vec_Vec_update_usize v i x.
 
 End Primitives.