Merge pull request #88 from AeneasVerif/son/clashes

Improve the name generation for code extraction

37 files changed, 825 insertions, 703 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index af0e62d1..65aa7555 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -366,3 +366,6 @@ let backend_has_tuple_projectors () =
 (** We we use nested projectors for tuple (like: [(0, 1).snd.fst]) or do
     we use better projector syntax? *)
 let use_nested_tuple_projectors = ref false
+
+(** Generate name patterns for the external definitions we encounter *)
+let extract_external_name_patterns = ref false
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 794a1bfa..46f6a1ca 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -19,7 +19,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
      only use their type for the fields of the records we generate for the trait
      declarations *)
   match def.f.kind with
-  | TraitMethodDecl _ -> ctx
+  | TraitItemDecl _ -> ctx
   | _ -> (
       (* Check if the function is builtin *)
       let builtin =
@@ -48,6 +48,9 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
           ctx_add (FunId (FromLlbc fun_id)) fun_info.extract_name ctx
       | None ->
           (* Not builtin *)
+          (* If this is a trait method implementation, we prefix the name with the
+             name of the trait implementation. We need to do so because there
+             can be clashes otherwise. *)
           (* Register the decrease clauses, if necessary *)
           let register_decreases ctx def =
             if has_decreases_clause def then
@@ -1105,7 +1108,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
   *)
   let ctx, trait_decl =
     match def.kind with
-    | TraitMethodProvided (decl_id, _) ->
+    | TraitItemProvided (decl_id, _) ->
         let trait_decl = T.TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
         let ctx, _ = ctx_add_trait_self_clause ctx in
         let ctx = { ctx with is_provided_method = true } in
@@ -1204,9 +1207,14 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
-    def.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not def.is_local then
+       Some def.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
+     name def.meta.span);
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -1267,9 +1275,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
+  extract_comment_with_span ctx fmt
     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]
-    def.meta.span;
+    None def.meta.span;
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -1322,9 +1330,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   let def_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in
   (* syntax <def_name> term ... term : tactic *)
   F.pp_print_break fmt 0 0;
-  extract_comment_with_span fmt
+  extract_comment_with_span ctx fmt
     [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]
-    def.meta.span;
+    None def.meta.span;
   F.pp_print_space fmt ();
   F.pp_open_hvbox fmt 0;
   F.pp_print_string fmt "syntax \"";
@@ -1364,7 +1372,12 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
     in
     [ comment_pre ^ loop_comment ]
   in
-  extract_comment_with_span fmt comment def.meta.span
+  let name =
+    if !Config.extract_external_name_patterns && not def.is_local then
+      Some def.llbc_name
+    else None
+  in
+  extract_comment_with_span ctx fmt comment name def.meta.span
 
 (** Extract a function declaration.
 
@@ -1813,9 +1826,14 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
-  extract_comment_with_span fmt
+  let name =
+    if !Config.extract_external_name_patterns && not global.is_local then
+      Some global.name
+    else None
+  in
+  extract_comment_with_span ctx fmt
     [ "[" ^ name_to_string ctx global.name ^ "]" ]
-    global.meta.span;
+    name global.meta.span;
   F.pp_print_space fmt ();
 
   let decl_name = ctx_get_global global.def_id ctx in
@@ -2207,9 +2225,14 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
-    decl.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not decl.is_local then
+       Some decl.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
+     name decl.meta.span);
   F.pp_print_break fmt 0 0;
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
      one line and indents are correct.
@@ -2490,9 +2513,14 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
-    impl.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not impl.is_local then
+       Some impl.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
+     name impl.meta.span);
   F.pp_print_break fmt 0 0;
 
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 591e8aab..5e97cd21 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1266,13 +1266,11 @@ let name_last_elem_as_ident (n : llbc_name) : string =
     we remove it. We ignore disambiguators (there may be collisions, but we
     check if there are).
  *)
-let ctx_compute_simple_name (ctx : extraction_ctx) (name : llbc_name) :
-    string list =
+let ctx_prepare_name (ctx : extraction_ctx) (name : llbc_name) : llbc_name =
   (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
   match name with
   | (PeIdent (crate, _) as id) :: name ->
-      let name = if crate = ctx.crate.name then name else id :: name in
-      name_to_simple_name ctx.trans_ctx name
+      if crate = ctx.crate.name then name else id :: name
   | _ ->
       raise
         (Failure
@@ -1280,6 +1278,13 @@ let ctx_compute_simple_name (ctx : extraction_ctx) (name : llbc_name) :
            ^ TranslateCore.name_to_string ctx.trans_ctx name))
 
 (** Helper *)
+let ctx_compute_simple_name (ctx : extraction_ctx) (name : llbc_name) :
+    string list =
+  (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
+  let name = ctx_prepare_name ctx name in
+  name_to_simple_name ctx.trans_ctx name
+
+(** Helper *)
 let ctx_compute_simple_type_name = ctx_compute_simple_name
 
 (** Helper *)
@@ -1369,10 +1374,11 @@ let ctx_compute_fun_name_no_suffix (ctx : extraction_ctx) (fname : llbc_name) :
 
 (** Provided a basename, compute the name of a global declaration. *)
 let ctx_compute_global_name (ctx : extraction_ctx) (name : llbc_name) : string =
-  (* Converting to snake case also lowercases the letters (in Rust, global
-   * names are written in capital letters). *)
-  let parts = List.map to_snake_case (ctx_compute_simple_name ctx name) in
-  String.concat "_" parts
+  match !Config.backend with
+  | Coq | FStar | HOL4 ->
+      let parts = List.map to_snake_case (ctx_compute_simple_name ctx name) in
+      String.concat "_" parts
+  | Lean -> flatten_name (ctx_compute_simple_name ctx name)
 
 (** Helper function: generate a suffix for a function name, i.e., generates
     a suffix like "_loop", "loop1", etc. to append to a function name.
@@ -1426,8 +1432,8 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
   let name =
     let params = trait_impl.llbc_generics in
     let args = trait_impl.llbc_impl_trait.decl_generics in
-    trait_name_with_generics_to_simple_name ctx.trans_ctx trait_decl.llbc_name
-      params args
+    let name = ctx_prepare_name ctx trait_decl.llbc_name in
+    trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
   in
   let name = flatten_name name in
   match !backend with
@@ -1506,6 +1512,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
     if !Config.record_fields_short_names then clause
     else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause
   in
+  let clause = clause ^ "Inst" in
   match !backend with
   | FStar -> StringUtils.lowercase_first_letter clause
   | Coq | HOL4 | Lean -> clause
@@ -1715,6 +1722,7 @@ let ctx_compute_trait_clause_basename (ctx : extraction_ctx)
     ctx_compute_trait_clause_name ctx current_def_name params
       params.trait_clauses clause_id
   in
+  let clause = clause ^ "Inst" in
   match !backend with
   | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter clause
   | Lean -> clause
@@ -1882,8 +1890,15 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
       (* Not the case: "standard" registration *)
       let name = ctx_compute_global_name ctx def.name in
       let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in
-      let ctx = ctx_add decl (name ^ "_c") ctx in
-      let ctx = ctx_add body (name ^ "_body") ctx in
+      (* If this is a provided constant (i.e., the default value for a constant
+         in a trait declaration) we add a suffix. Otherwise there is a clash
+         between the name for the default constant and the name for the field
+         in the trait declaration *)
+      let suffix =
+        match def.kind with TraitItemProvided _ -> "_default" | _ -> ""
+      in
+      let ctx = ctx_add decl (name ^ suffix) ctx in
+      let ctx = ctx_add body (name ^ suffix ^ "_body") ctx in
       ctx
 
 let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 88de31fe..401d0137 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -253,35 +253,77 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
       (Some [ true; false ]);
     mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len" None
       (Some [ true; false ]);
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::index" None
+    mk_fun
+      "alloc::vec::{core::ops::index::Index<alloc::vec::Vec<@T, @A>, \
+       @I>}::index"
+      (Some "alloc.vec.Vec.index")
       (Some [ true; true; false ]);
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut" None
+    mk_fun
+      "alloc::vec::{core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, \
+       @I>}::index_mut"
+      (Some "alloc.vec.Vec.index_mut")
       (Some [ true; true; false ]);
-    mk_fun "alloc::boxed::{Box<@T>}::deref" None (Some [ true; false ]);
-    mk_fun "alloc::boxed::{Box<@T>}::deref_mut" None (Some [ true; false ]);
-    mk_fun "core::slice::index::{[@T]}::index" None None;
-    mk_fun "core::slice::index::{[@T]}::index_mut" None None;
-    mk_fun "core::array::{[@T; @C]}::index" None None;
-    mk_fun "core::array::{[@T; @C]}::index_mut" None None;
-    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get"
+    mk_fun "alloc::boxed::{core::ops::deref::Deref<Box<@T>>}::deref"
+      (Some "alloc.boxed.Box.deref")
+      (Some [ true; false ]);
+    mk_fun "alloc::boxed::{core::ops::deref::DerefMut<Box<@T>>}::deref_mut"
+      (Some "alloc.boxed.Box.deref_mut")
+      (Some [ true; false ]);
+    mk_fun "core::slice::index::{core::ops::index::Index<[@T], @I>}::index"
+      (Some "core.slice.index.Slice.index") None;
+    mk_fun
+      "core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut"
+      (Some "core.slice.index.Slice.index_mut") None;
+    mk_fun "core::array::{core::ops::index::Index<[@T; @N], @I>}::index"
+      (Some "core.array.Array.index") None;
+    mk_fun "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut"
+      (Some "core.array.Array.index_mut") None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::get"
       (Some "core::slice::index::RangeUsize::get") None;
-    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get_mut"
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::get_mut"
       (Some "core::slice::index::RangeUsize::get_mut") None;
-    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::index"
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::index"
       (Some "core::slice::index::RangeUsize::index") None;
-    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::index_mut"
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::index_mut"
       (Some "core::slice::index::RangeUsize::index_mut") None;
-    mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get_unchecked"
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::get_unchecked"
       (Some "core::slice::index::RangeUsize::get_unchecked") None;
     mk_fun
-      "core::slice::index::{core::ops::range::Range<usize>}::get_unchecked_mut"
+      "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
+       [@T]>}::get_unchecked_mut"
       (Some "core::slice::index::RangeUsize::get_unchecked_mut") None;
-    mk_fun "core::slice::index::{usize}::get" None None;
-    mk_fun "core::slice::index::{usize}::get_mut" None None;
-    mk_fun "core::slice::index::{usize}::get_unchecked" None None;
-    mk_fun "core::slice::index::{usize}::get_unchecked_mut" None None;
-    mk_fun "core::slice::index::{usize}::index" None None;
-    mk_fun "core::slice::index::{usize}::index_mut" None None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, [@T]>}::get"
+      None None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, \
+       [@T]>}::get_mut"
+      None None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, \
+       [@T]>}::get_unchecked"
+      None None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, \
+       [@T]>}::get_unchecked_mut"
+      None None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, [@T]>}::index"
+      (Some "core_slice_index_Slice_index") None;
+    mk_fun
+      "core::slice::index::{core::slice::index::SliceIndex<usize, \
+       [@T]>}::index_mut"
+      (Some "core_slice_index_Slice_index_mut") None;
   ]
 
 let mk_builtin_funs_map () =
@@ -351,9 +393,10 @@ let builtin_fun_effects =
     [
       (* TODO: redundancy with the funs information above *)
       "alloc::vec::{alloc::vec::Vec<@T, @A>}::push";
-      "alloc::vec::{alloc::vec::Vec<@T, @A>}::index";
-      "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut";
-      "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut_back";
+      "alloc::vec::{core::ops::index::Index<alloc::vec::Vec<@T, @A>, \
+       @I>}::index";
+      "alloc::vec::{core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, \
+       @I>}::index_mut";
     ]
   in
   let no_state_funs =
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 4c1ffb46..80ed2ca3 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -31,69 +31,82 @@ end
     For impl blocks, we simply use the name of the type (without its arguments)
     if all the arguments are variables.
  *)
-let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
-    string list =
+let pattern_to_extract_name (name : pattern) : string list =
   let c = { tgt = TkName } in
-  let is_var (g : generic_arg) : bool =
-    match g with
-    | GExpr (EVar _) -> true
-    | GRegion (RVar _) -> true
-    | _ -> false
+  let all_vars =
+    let check (g : generic_arg) : bool =
+      match g with GExpr (EVar _) | GRegion (RVar _) -> true | _ -> false
+    in
+    List.for_all check
   in
-  let all_vars = List.for_all is_var in
-  let elem_to_string (e : pattern_elem) : string =
-    match e with
-    | PIdent _ -> pattern_elem_to_string c e
-    | PImpl ty -> (
+
+  (* This is a bit of a hack: we want to simplify the occurrences of
+     tuples of two variables, arrays with only variables, slices with
+     only variables, etc.
+     We explore the pattern and replace such occurrences with a specific name.
+  *)
+  let replace_option_name (id : pattern) =
+    match id with
+    | [ PIdent ("core", []); PIdent ("option", []); PIdent ("Option", g) ] ->
+        (* Option *)
+        [ PIdent ("Option", g) ]
+    | _ -> id
+  in
+  let visitor =
+    object
+      inherit [_] map_pattern as super
+
+      method! visit_PIdent _ s g =
+        if all_vars g then super#visit_PIdent () s []
+        else super#visit_PIdent () s g
+
+      method! visit_EComp _ id =
+        (* Simplify if this is [Option] *)
+        super#visit_EComp () (replace_option_name id)
+
+      method! visit_PImpl _ ty =
         match ty with
         | EComp id -> (
-            (* Retrieve the last ident *)
+            (* Only keep the last ident *)
             let id = Collections.List.last id in
             match id with
-            | PIdent (s, g) ->
-                if all_vars g then s else pattern_elem_to_string c id
+            | PIdent (_, _) -> super#visit_PImpl () (EComp [ id ])
             | PImpl _ -> raise (Failure "Unreachable"))
-        | EPrimAdt (adt, g) ->
-            if all_vars g then
-              match adt with
-              | TTuple ->
-                  let l = List.length g in
-                  if l = 2 then "Pair" else expr_to_string c ty
-              | TArray -> "Array"
-              | TSlice -> "Slice"
-            else expr_to_string c ty
-        | ERef _ | EVar _ | EArrow _ | ERawPtr _ ->
-            (* We simply convert the pattern to a string. This is not very
-               satisfying but we should rarely get there. *)
-            expr_to_string c ty)
-  in
-  let rec pattern_to_string (n : pattern) : string list =
-    match n with
-    | [] -> raise (Failure "Unreachable")
-    | [ e ] ->
-        let e = elem_to_string e in
-        if is_trait_impl then [ e ^ "Inst" ] else [ e ]
-    | e :: n -> elem_to_string e :: pattern_to_string n
+        | _ -> super#visit_PImpl () ty
+
+      method! visit_EPrimAdt _ adt g =
+        if all_vars g then
+          match adt with
+          | TTuple ->
+              let l = List.length g in
+              if l = 2 then EComp [ PIdent ("Pair", []) ]
+              else super#visit_EPrimAdt () adt g
+          | TArray -> EComp [ PIdent ("Array", []) ]
+          | TSlice -> EComp [ PIdent ("Slice", []) ]
+        else if adt = TTuple && List.length g = 2 then
+          super#visit_EComp () [ PIdent ("Pair", g) ]
+        else super#visit_EPrimAdt () adt g
+    end
   in
-  pattern_to_string name
+  let name = visitor#visit_pattern () name in
+  List.map (pattern_elem_to_string c) name
 
-let pattern_to_type_extract_name = pattern_to_extract_name false
-let pattern_to_fun_extract_name = pattern_to_extract_name false
-let pattern_to_trait_impl_extract_name = pattern_to_extract_name true
+let pattern_to_type_extract_name = pattern_to_extract_name
+let pattern_to_fun_extract_name = pattern_to_extract_name
+let pattern_to_trait_impl_extract_name = pattern_to_extract_name
 
 (* TODO: this is provisional. We just want to make sure that the extraction
    names we derive from the patterns (for the builtin definitions) are
    consistent with the extraction names we derive from the Rust names *)
-let name_to_simple_name (ctx : ctx) (is_trait_impl : bool) (n : Types.name) :
-    string list =
+let name_to_simple_name (ctx : ctx) (n : Types.name) : string list =
   let c : to_pat_config =
     { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs }
   in
-  pattern_to_extract_name is_trait_impl (name_to_pattern ctx c n)
+  pattern_to_extract_name (name_to_pattern ctx c n)
 
 (** If the [prefix] is Some, we attempt to remove the common prefix
     between [prefix] and [name] from [name] *)
-let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool)
+let name_with_generics_to_simple_name (ctx : ctx)
     ?(prefix : Types.name option = None) (name : Types.name)
     (p : Types.generic_params) (g : Types.generic_args) : string list =
   let c : to_pat_config =
@@ -111,4 +124,4 @@ let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool)
         let _, _, name = pattern_common_prefix { equiv = true } prefix name in
         name
   in
-  pattern_to_extract_name is_trait_impl name
+  pattern_to_extract_name name
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 05b71b9f..9d4131d2 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1116,8 +1116,8 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
   F.pp_print_string fmt rd;
   F.pp_close_box fmt ()
 
-let extract_comment_with_span (fmt : F.formatter) (sl : string list)
-    (span : Meta.span) : unit =
+let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
+    (sl : string list) (name : Types.name option) (span : Meta.span) : unit =
   let file = match span.file with Virtual s | Local s -> s in
   let loc_to_string (l : Meta.loc) : string =
     string_of_int l.line ^ ":" ^ string_of_int l.col
@@ -1126,7 +1126,13 @@ let extract_comment_with_span (fmt : F.formatter) (sl : string list)
     "Source: '" ^ file ^ "', lines " ^ loc_to_string span.beg_loc ^ "-"
     ^ loc_to_string span.end_loc
   in
-  extract_comment fmt (sl @ [ span ])
+  let name =
+    match name with
+    | None -> []
+    | Some name ->
+        [ "Name pattern: " ^ name_to_pattern_string ctx.trans_ctx name ]
+  in
+  extract_comment fmt (sl @ [ span ] @ name)
 
 let extract_trait_clause_type (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit =
@@ -1359,9 +1365,14 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   if !backend <> HOL4 || not (decl_is_first_from_group kind) then
     F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment_with_span fmt
-    [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]
-    def.meta.span;
+  (let name =
+     if !Config.extract_external_name_patterns && not def.is_local then
+       Some def.llbc_name
+     else None
+   in
+   extract_comment_with_span ctx fmt
+     [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]
+     name def.meta.span);
   F.pp_print_break fmt 0 0;
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line. Note however that in the case of Lean line breaks are important
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index fd3e334b..ccae4588 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -68,12 +68,12 @@ let normalize_inst_fun_sig (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig =
     normalize because a trait clause was instantiated with a specific trait ref).
  *)
 let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
-    (regions_hierarchy : region_var_groups) (kind : fun_kind) :
+    (regions_hierarchy : region_var_groups) (kind : item_kind) :
     eval_ctx * inst_fun_sig =
   let tr_self =
     match kind with
-    | RegularKind | TraitMethodImpl _ -> UnknownTrait __FUNCTION__
-    | TraitMethodDecl _ | TraitMethodProvided _ -> Self
+    | RegularKind | TraitItemImpl _ -> UnknownTrait __FUNCTION__
+    | TraitItemDecl _ | TraitItemProvided _ -> Self
   in
   let generics =
     let { regions; types; const_generics; trait_clauses } = sg.generics in
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index d3fac032..1053c9ab 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -44,7 +44,7 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
     d.body = None
     (* Something to pay attention to: we must ignore trait method *declarations*
        (which don't have a body but must not be considered as opaque) *)
-    && (match d.kind with TraitMethodDecl _ -> false | _ -> true)
+    && (match d.kind with TraitItemDecl _ -> false | _ -> true)
     && ((not filter_assumed)
        || (not (NameMatcherMap.mem ctx d.name builtin_globals_map))
           && not (NameMatcherMap.mem ctx d.name (builtin_funs_map ())))
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 3f5e62ad..e703f1a0 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -118,6 +118,9 @@ let () =
         Arg.Set use_nested_tuple_projectors,
         " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \
          (0, 1).1)." );
+      ( "-ext-name-pats",
+        Arg.Set extract_external_name_patterns,
+        " Generate name patterns for the external definitions we find." );
     ]
   in
 
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index dd7a4acf..33c23cc3 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1063,13 +1063,13 @@ type fun_body = {
 }
 [@@deriving show]
 
-type fun_kind = A.fun_kind [@@deriving show]
+type item_kind = A.item_kind [@@deriving show]
 
 type fun_decl = {
   def_id : FunDeclId.id;
   is_local : bool;
   meta : meta;
-  kind : fun_kind;
+  kind : item_kind;
   num_loops : int;
       (** The number of loops in the parent forward function (basically the number
           of loops appearing in the original Rust functions, unless some loops are
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index c12de045..48a3685b 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -730,7 +730,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            the trait declarations themselves, there is no point in having
            separate type definitions) *)
         match pure_fun.f.Pure.kind with
-        | TraitMethodDecl _ -> ()
+        | TraitItemDecl _ -> ()
         | _ ->
             (* Translate *)
             export_functions_group [ pure_fun ])
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index 05877b5a..3e4c7375 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -60,8 +60,7 @@ let name_to_simple_name (ctx : trans_ctx) (n : Types.name) : string list =
       trait_impls = ctx.trait_impls_ctx.trait_impls;
     }
   in
-  let is_trait_impl = false in
-  name_to_simple_name mctx is_trait_impl n
+  name_to_simple_name mctx n
 
 let trait_name_with_generics_to_simple_name (ctx : trans_ctx)
     ?(prefix : Types.name option = None) (n : Types.name)
@@ -75,5 +74,20 @@ let trait_name_with_generics_to_simple_name (ctx : trans_ctx)
       trait_impls = ctx.trait_impls_ctx.trait_impls;
     }
   in
-  let is_trait_impl = true in
-  name_with_generics_to_simple_name mctx is_trait_impl ~prefix n p g
+  name_with_generics_to_simple_name mctx ~prefix n p g
+
+let name_to_pattern_string (ctx : trans_ctx) (n : Types.name) : string =
+  let mctx : Charon.NameMatcher.ctx =
+    {
+      type_decls = ctx.type_ctx.type_decls;
+      global_decls = ctx.global_ctx.global_decls;
+      fun_decls = ctx.fun_ctx.fun_decls;
+      trait_decls = ctx.trait_decls_ctx.trait_decls;
+      trait_impls = ctx.trait_impls_ctx.trait_impls;
+    }
+  in
+  let c : Charon.NameMatcher.to_pat_config =
+    { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs }
+  in
+  let pat = Charon.NameMatcher.name_to_pattern mctx c n in
+  Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat
diff --git a/flake.lock b/flake.lock
index b9382775..db195035 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,11 +8,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1709941742,
-        "narHash": "sha256-iSi3HQBac+JSACClXRJBooQbPOtyqA/P//WzwLQH+tQ=",
+        "lastModified": 1710149523,
+        "narHash": "sha256-y6ZZvC7y+uIdorsdBEKJG0u02CLsWFf1CTkE8DNWn2o=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "c1b3f94afb32ae0917a2abd09f0c6f8e31bed9d6",
+        "rev": "879469900b4baadb85835c5e7da47e6506f6642c",
         "type": "github"
       },
       "original": {
@@ -82,11 +82,11 @@
         "systems": "systems_3"
       },
       "locked": {
-        "lastModified": 1709126324,
-        "narHash": "sha256-q6EQdSeUZOG26WelxqkmR7kArjgWCdw5sfJVHPH/7j8=",
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "d465f4819400de7c8d874d50b982301f28a84605",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
         "type": "github"
       },
       "original": {
@@ -265,11 +265,11 @@
         "nixpkgs": "nixpkgs_4"
       },
       "locked": {
-        "lastModified": 1709930258,
-        "narHash": "sha256-0oJSuzf3zSRMbfmtZ789sJqhg+pgbBZWo9mATpe/dsE=",
+        "lastModified": 1710111430,
+        "narHash": "sha256-TsVeepxSag4OMVWH2UxntI0HHF2Db7hYUpAwhM8XjUQ=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "b39042b32c00b6455153f9df26153680b2dc6d6f",
+        "rev": "32dcc6eb895b58df3d3241a2521963e64995b621",
         "type": "github"
       },
       "original": {
@@ -318,11 +318,11 @@
         "nixpkgs": "nixpkgs_7"
       },
       "locked": {
-        "lastModified": 1709930258,
-        "narHash": "sha256-0oJSuzf3zSRMbfmtZ789sJqhg+pgbBZWo9mATpe/dsE=",
+        "lastModified": 1710111430,
+        "narHash": "sha256-TsVeepxSag4OMVWH2UxntI0HHF2Db7hYUpAwhM8XjUQ=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "b39042b32c00b6455153f9df26153680b2dc6d6f",
+        "rev": "32dcc6eb895b58df3d3241a2521963e64995b621",
         "type": "github"
       },
       "original": {
diff --git a/tests/Makefile b/tests/Makefile
index ccdbf652..8d40e8da 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,4 +1,4 @@
-all: test-fstar test-fstar-split test-coq test-lean test-hol4
+all: test-fstar test-coq test-lean test-hol4
 
 test-%:
 	cd $* && $(MAKE) all
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 79be3678..34d163b7 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -492,7 +492,7 @@ Definition f3 (n : nat) : result u32 :=
 (** [arrays::SZ]
     Source: 'src/arrays.rs', lines 286:0-286:19 *)
 Definition sz_body : result usize := Return 32%usize.
-Definition sz_c : usize := sz_body%global.
+Definition sz : usize := sz_body%global.
 
 (** [arrays::f5]:
     Source: 'src/arrays.rs', lines 289:0-289:31 *)
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index cefab0f4..3863a90f 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -159,7 +159,7 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
 
 (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
     Source: 'src/betree.rs', lines 327:4-327:44 *)
-Definition betree_ListTupleU64T_head_has_key
+Definition betree_ListPairU64T_head_has_key
   (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
   match self with
   | Betree_List_Cons hd _ => let (i, _) := hd in Return (i s= key)
@@ -169,7 +169,7 @@ Definition betree_ListTupleU64T_head_has_key
 
 (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
     Source: 'src/betree.rs', lines 339:4-339:73 *)
-Fixpoint betree_ListTupleU64T_partition_at_pivot
+Fixpoint betree_ListPairU64T_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)))
   :=
@@ -182,7 +182,7 @@ Fixpoint betree_ListTupleU64T_partition_at_pivot
       if i s>= pivot
       then Return (Betree_List_Nil, Betree_List_Cons (i, t) tl)
       else (
-        p <- betree_ListTupleU64T_partition_at_pivot T n1 tl pivot;
+        p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot;
         let (ls0, ls1) := p in
         Return (Betree_List_Cons (i, t) ls0, ls1))
     | Betree_List_Nil => Return (Betree_List_Nil, Betree_List_Nil)
@@ -286,7 +286,7 @@ Fixpoint betree_Node_apply_upserts
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key;
+    b <- betree_ListPairU64T_head_has_key betree_Message_t msgs key;
     if b
     then (
       p <- betree_List_pop_front (u64 * betree_Message_t) msgs;
@@ -462,7 +462,7 @@ Definition betree_Node_apply_to_internal
   :=
   p <- betree_Node_lookup_first_message_for_key n key msgs;
   let (msgs1, lookup_first_message_for_key_back) := p in
-  b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs1 key;
+  b <- betree_ListPairU64T_head_has_key betree_Message_t msgs1 key;
   if b
   then
     match new_msg with
@@ -570,7 +570,7 @@ Definition betree_Node_apply_to_leaf
   :=
   p <- betree_Node_lookup_mut_in_bindings n key bindings;
   let (bindings1, lookup_mut_in_bindings_back) := p in
-  b <- betree_ListTupleU64T_head_has_key u64 bindings1 key;
+  b <- betree_ListPairU64T_head_has_key u64 bindings1 key;
   if b
   then (
     p1 <- betree_List_pop_front (u64 * u64) bindings1;
@@ -632,7 +632,7 @@ Fixpoint betree_Internal_flush
   | O => Fail_ OutOfFuel
   | S n1 =>
     p <-
-      betree_ListTupleU64T_partition_at_pivot betree_Message_t n1 content
+      betree_ListPairU64T_partition_at_pivot betree_Message_t n1 content
         self.(betree_Internal_pivot);
     let (msgs_left, msgs_right) := p in
     len_left <- betree_List_len (u64 * betree_Message_t) n1 msgs_left;
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 1abe7c5c..ec7ca29d 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -145,23 +145,23 @@ Record Counter_t (Self : Type) := mkCounter_t {
 Arguments mkCounter_t { _ }.
 Arguments Counter_t_incr { _ }.
 
-(** [demo::{usize}::incr]:
+(** [demo::{(demo::Counter for usize)}::incr]:
     Source: 'src/demo.rs', lines 88:4-88:31 *)
-Definition usize_incr (self : usize) : result (usize * usize) :=
+Definition counterUsize_incr (self : usize) : result (usize * usize) :=
   self1 <- usize_add self 1%usize; Return (self, self1)
 .
 
-(** Trait implementation: [demo::{usize}]
+(** Trait implementation: [demo::{(demo::Counter for usize)}]
     Source: 'src/demo.rs', lines 87:0-87:22 *)
-Definition demo_CounterUsizeInst : Counter_t usize := {|
-  Counter_t_incr := usize_incr;
+Definition CounterUsize : Counter_t usize := {|
+  Counter_t_incr := counterUsize_incr;
 |}.
 
 (** [demo::use_counter]:
     Source: 'src/demo.rs', lines 95:0-95:59 *)
 Definition use_counter
-  (T : Type) (counterTInst : Counter_t T) (cnt : T) : result (usize * T) :=
-  counterTInst.(Counter_t_incr) cnt
+  (T : Type) (counterInst : Counter_t T) (cnt : T) : result (usize * T) :=
+  counterInst.(Counter_t_incr) cnt
 .
 
 End Demo.
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 0f33cbd6..5fa952b4 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -11,17 +11,17 @@ Module Constants.
 (** [constants::X0]
     Source: 'src/constants.rs', lines 5:0-5:17 *)
 Definition x0_body : result u32 := Return 0%u32.
-Definition x0_c : u32 := x0_body%global.
+Definition x0 : u32 := x0_body%global.
 
 (** [constants::X1]
     Source: 'src/constants.rs', lines 7:0-7:17 *)
 Definition x1_body : result u32 := Return core_u32_max.
-Definition x1_c : u32 := x1_body%global.
+Definition x1 : u32 := x1_body%global.
 
 (** [constants::X2]
     Source: 'src/constants.rs', lines 10:0-10:17 *)
 Definition x2_body : result u32 := Return 3%u32.
-Definition x2_c : u32 := x2_body%global.
+Definition x2 : u32 := x2_body%global.
 
 (** [constants::incr]:
     Source: 'src/constants.rs', lines 17:0-17:32 *)
@@ -31,12 +31,13 @@ Definition incr (n : u32) : result u32 :=
 (** [constants::X3]
     Source: 'src/constants.rs', lines 15:0-15:17 *)
 Definition x3_body : result u32 := incr 32%u32.
-Definition x3_c : u32 := x3_body%global.
+Definition x3 : u32 := x3_body%global.
 
 (** [constants::mk_pair0]:
     Source: 'src/constants.rs', lines 23:0-23:51 *)
-Definition mk_pair0 (x : u32) (y : u32) : result (u32 * u32) :=
-  Return (x, y).
+Definition mk_pair0 (x : u32) (y1 : u32) : result (u32 * u32) :=
+  Return (x, y1)
+.
 
 (** [constants::Pair]
     Source: 'src/constants.rs', lines 36:0-36:23 *)
@@ -48,31 +49,31 @@ Arguments pair_y { _ _ }.
 
 (** [constants::mk_pair1]:
     Source: 'src/constants.rs', lines 27:0-27:55 *)
-Definition mk_pair1 (x : u32) (y : u32) : result (Pair_t u32 u32) :=
-  Return {| pair_x := x; pair_y := y |}
+Definition mk_pair1 (x : u32) (y1 : u32) : result (Pair_t u32 u32) :=
+  Return {| pair_x := x; pair_y := y1 |}
 .
 
 (** [constants::P0]
     Source: 'src/constants.rs', lines 31:0-31:24 *)
 Definition p0_body : result (u32 * u32) := mk_pair0 0%u32 1%u32.
-Definition p0_c : (u32 * u32) := p0_body%global.
+Definition p0 : (u32 * u32) := p0_body%global.
 
 (** [constants::P1]
     Source: 'src/constants.rs', lines 32:0-32:28 *)
 Definition p1_body : result (Pair_t u32 u32) := mk_pair1 0%u32 1%u32.
-Definition p1_c : Pair_t u32 u32 := p1_body%global.
+Definition p1 : Pair_t u32 u32 := p1_body%global.
 
 (** [constants::P2]
     Source: 'src/constants.rs', lines 33:0-33:24 *)
 Definition p2_body : result (u32 * u32) := Return (0%u32, 1%u32).
-Definition p2_c : (u32 * u32) := p2_body%global.
+Definition p2 : (u32 * u32) := p2_body%global.
 
 (** [constants::P3]
     Source: 'src/constants.rs', lines 34:0-34:28 *)
 Definition p3_body : result (Pair_t u32 u32) :=
   Return {| pair_x := 0%u32; pair_y := 1%u32 |}
 .
-Definition p3_c : Pair_t u32 u32 := p3_body%global.
+Definition p3 : Pair_t u32 u32 := p3_body%global.
 
 (** [constants::Wrap]
     Source: 'src/constants.rs', lines 49:0-49:18 *)
@@ -90,27 +91,27 @@ Definition wrap_new (T : Type) (value : T) : result (Wrap_t T) :=
 (** [constants::Y]
     Source: 'src/constants.rs', lines 41:0-41:22 *)
 Definition y_body : result (Wrap_t i32) := wrap_new i32 2%i32.
-Definition y_c : Wrap_t i32 := y_body%global.
+Definition y : Wrap_t i32 := y_body%global.
 
 (** [constants::unwrap_y]:
     Source: 'src/constants.rs', lines 43:0-43:30 *)
 Definition unwrap_y : result i32 :=
-  Return y_c.(wrap_value).
+  Return y.(wrap_value).
 
 (** [constants::YVAL]
     Source: 'src/constants.rs', lines 47:0-47:19 *)
 Definition yval_body : result i32 := unwrap_y.
-Definition yval_c : i32 := yval_body%global.
+Definition yval : i32 := yval_body%global.
 
 (** [constants::get_z1::Z1]
     Source: 'src/constants.rs', lines 62:4-62:17 *)
 Definition get_z1_z1_body : result i32 := Return 3%i32.
-Definition get_z1_z1_c : i32 := get_z1_z1_body%global.
+Definition get_z1_z1 : i32 := get_z1_z1_body%global.
 
 (** [constants::get_z1]:
     Source: 'src/constants.rs', lines 61:0-61:28 *)
 Definition get_z1 : result i32 :=
-  Return get_z1_z1_c.
+  Return get_z1_z1.
 
 (** [constants::add]:
     Source: 'src/constants.rs', lines 66:0-66:39 *)
@@ -120,41 +121,41 @@ Definition add (a : i32) (b : i32) : result i32 :=
 (** [constants::Q1]
     Source: 'src/constants.rs', lines 74:0-74:17 *)
 Definition q1_body : result i32 := Return 5%i32.
-Definition q1_c : i32 := q1_body%global.
+Definition q1 : i32 := q1_body%global.
 
 (** [constants::Q2]
     Source: 'src/constants.rs', lines 75:0-75:17 *)
-Definition q2_body : result i32 := Return q1_c.
-Definition q2_c : i32 := q2_body%global.
+Definition q2_body : result i32 := Return q1.
+Definition q2 : i32 := q2_body%global.
 
 (** [constants::Q3]
     Source: 'src/constants.rs', lines 76:0-76:17 *)
-Definition q3_body : result i32 := add q2_c 3%i32.
-Definition q3_c : i32 := q3_body%global.
+Definition q3_body : result i32 := add q2 3%i32.
+Definition q3 : i32 := q3_body%global.
 
 (** [constants::get_z2]:
     Source: 'src/constants.rs', lines 70:0-70:28 *)
 Definition get_z2 : result i32 :=
-  i <- get_z1; i1 <- add i q3_c; add q1_c i1.
+  i <- get_z1; i1 <- add i q3; add q1 i1.
 
 (** [constants::S1]
     Source: 'src/constants.rs', lines 80:0-80:18 *)
 Definition s1_body : result u32 := Return 6%u32.
-Definition s1_c : u32 := s1_body%global.
+Definition s1 : u32 := s1_body%global.
 
 (** [constants::S2]
     Source: 'src/constants.rs', lines 81:0-81:18 *)
-Definition s2_body : result u32 := incr s1_c.
-Definition s2_c : u32 := s2_body%global.
+Definition s2_body : result u32 := incr s1.
+Definition s2 : u32 := s2_body%global.
 
 (** [constants::S3]
     Source: 'src/constants.rs', lines 82:0-82:29 *)
-Definition s3_body : result (Pair_t u32 u32) := Return p3_c.
-Definition s3_c : Pair_t u32 u32 := s3_body%global.
+Definition s3_body : result (Pair_t u32 u32) := Return p3.
+Definition s3 : Pair_t u32 u32 := s3_body%global.
 
 (** [constants::S4]
     Source: 'src/constants.rs', lines 83:0-83:29 *)
 Definition s4_body : result (Pair_t u32 u32) := mk_pair1 7%u32 8%u32.
-Definition s4_c : Pair_t u32 u32 := s4_body%global.
+Definition s4 : Pair_t u32 u32 := s4_body%global.
 
 End Constants.
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 8857d4b6..73c4ee58 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -150,12 +150,12 @@ Definition mix_arith_i32 (x : i32) (y : i32) (z : i32) : result i32 :=
 (** [no_nested_borrows::CONST0]
     Source: 'src/no_nested_borrows.rs', lines 125:0-125:23 *)
 Definition const0_body : result usize := usize_add 1%usize 1%usize.
-Definition const0_c : usize := const0_body%global.
+Definition const0 : usize := const0_body%global.
 
 (** [no_nested_borrows::CONST1]
     Source: 'src/no_nested_borrows.rs', lines 126:0-126:23 *)
 Definition const1_body : result usize := usize_mul 2%usize 2%usize.
-Definition const1_c : usize := const1_body%global.
+Definition const1 : usize := const1_body%global.
 
 (** [no_nested_borrows::cast_u32_to_i32]:
     Source: 'src/no_nested_borrows.rs', lines 128:0-128:37 *)
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 4d0beae2..a9cd7e91 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -17,15 +17,15 @@ Record BoolTrait_t (Self : Type) := mkBoolTrait_t {
 Arguments mkBoolTrait_t { _ }.
 Arguments BoolTrait_t_get_bool { _ }.
 
-(** [traits::{bool}::get_bool]:
+(** [traits::{(traits::BoolTrait for bool)}::get_bool]:
     Source: 'src/traits.rs', lines 12:4-12:30 *)
-Definition bool_get_bool (self : bool) : result bool :=
+Definition boolTraitBool_get_bool (self : bool) : result bool :=
   Return self.
 
-(** Trait implementation: [traits::{bool}]
+(** Trait implementation: [traits::{(traits::BoolTrait for bool)}]
     Source: 'src/traits.rs', lines 11:0-11:23 *)
-Definition traits_BoolTraitBoolInst : BoolTrait_t bool := {|
-  BoolTrait_t_get_bool := bool_get_bool;
+Definition BoolTraitBool : BoolTrait_t bool := {|
+  BoolTrait_t_get_bool := boolTraitBool_get_bool;
 |}.
 
 (** [traits::BoolTrait::ret_true]:
@@ -38,37 +38,35 @@ Definition boolTrait_ret_true
 (** [traits::test_bool_trait_bool]:
     Source: 'src/traits.rs', lines 17:0-17:44 *)
 Definition test_bool_trait_bool (x : bool) : result bool :=
-  b <- bool_get_bool x;
-  if b then boolTrait_ret_true traits_BoolTraitBoolInst x else Return false
+  b <- boolTraitBool_get_bool x;
+  if b then boolTrait_ret_true BoolTraitBool x else Return false
 .
 
-(** [traits::{core::option::Option<T>#1}::get_bool]:
+(** [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]:
     Source: 'src/traits.rs', lines 23:4-23:30 *)
-Definition option_get_bool (T : Type) (self : option T) : result bool :=
+Definition boolTraitOption_get_bool
+  (T : Type) (self : option T) : result bool :=
   match self with | None => Return false | Some _ => Return true end
 .
 
-(** Trait implementation: [traits::{core::option::Option<T>#1}]
+(** Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}]
     Source: 'src/traits.rs', lines 22:0-22:31 *)
-Definition traits_BoolTraitcoreoptionOptionTInst (T : Type) : BoolTrait_t
-  (option T) := {|
-  BoolTrait_t_get_bool := option_get_bool T;
+Definition BoolTraitOption (T : Type) : BoolTrait_t (option T) := {|
+  BoolTrait_t_get_bool := boolTraitOption_get_bool T;
 |}.
 
 (** [traits::test_bool_trait_option]:
     Source: 'src/traits.rs', lines 31:0-31:54 *)
 Definition test_bool_trait_option (T : Type) (x : option T) : result bool :=
-  b <- option_get_bool T x;
-  if b
-  then boolTrait_ret_true (traits_BoolTraitcoreoptionOptionTInst T) x
-  else Return false
+  b <- boolTraitOption_get_bool T x;
+  if b then boolTrait_ret_true (BoolTraitOption T) x else Return false
 .
 
 (** [traits::test_bool_trait]:
     Source: 'src/traits.rs', lines 35:0-35:50 *)
 Definition test_bool_trait
-  (T : Type) (boolTraitTInst : BoolTrait_t T) (x : T) : result bool :=
-  boolTraitTInst.(BoolTrait_t_get_bool) x
+  (T : Type) (boolTraitInst : BoolTrait_t T) (x : T) : result bool :=
+  boolTraitInst.(BoolTrait_t_get_bool) x
 .
 
 (** Trait declaration: [traits::ToU64]
@@ -80,51 +78,48 @@ Record ToU64_t (Self : Type) := mkToU64_t {
 Arguments mkToU64_t { _ }.
 Arguments ToU64_t_to_u64 { _ }.
 
-(** [traits::{u64#2}::to_u64]:
+(** [traits::{(traits::ToU64 for u64)#2}::to_u64]:
     Source: 'src/traits.rs', lines 44:4-44:26 *)
-Definition u64_to_u64 (self : u64) : result u64 :=
+Definition toU64U64_to_u64 (self : u64) : result u64 :=
   Return self.
 
-(** Trait implementation: [traits::{u64#2}]
+(** Trait implementation: [traits::{(traits::ToU64 for u64)#2}]
     Source: 'src/traits.rs', lines 43:0-43:18 *)
-Definition traits_ToU64U64Inst : ToU64_t u64 := {|
-  ToU64_t_to_u64 := u64_to_u64;
-|}.
+Definition ToU64U64 : ToU64_t u64 := {| ToU64_t_to_u64 := toU64U64_to_u64; |}.
 
-(** [traits::{(A, A)#3}::to_u64]:
+(** [traits::{(traits::ToU64 for (A, A))#3}::to_u64]:
     Source: 'src/traits.rs', lines 50:4-50:26 *)
-Definition pair_to_u64
-  (A : Type) (toU64AInst : ToU64_t A) (self : (A * A)) : result u64 :=
+Definition toU64Pair_to_u64
+  (A : Type) (toU64Inst : ToU64_t A) (self : (A * A)) : result u64 :=
   let (t, t1) := self in
-  i <- toU64AInst.(ToU64_t_to_u64) t;
-  i1 <- toU64AInst.(ToU64_t_to_u64) t1;
+  i <- toU64Inst.(ToU64_t_to_u64) t;
+  i1 <- toU64Inst.(ToU64_t_to_u64) t1;
   u64_add i i1
 .
 
-(** Trait implementation: [traits::{(A, A)#3}]
+(** Trait implementation: [traits::{(traits::ToU64 for (A, A))#3}]
     Source: 'src/traits.rs', lines 49:0-49:31 *)
-Definition traits_ToU64TupleAAInst (A : Type) (toU64AInst : ToU64_t A) :
-  ToU64_t (A * A) := {|
-  ToU64_t_to_u64 := pair_to_u64 A toU64AInst;
+Definition ToU64Pair (A : Type) (toU64Inst : ToU64_t A) : ToU64_t (A * A) := {|
+  ToU64_t_to_u64 := toU64Pair_to_u64 A toU64Inst;
 |}.
 
 (** [traits::f]:
     Source: 'src/traits.rs', lines 55:0-55:36 *)
-Definition f (T : Type) (toU64TInst : ToU64_t T) (x : (T * T)) : result u64 :=
-  pair_to_u64 T toU64TInst x
+Definition f (T : Type) (toU64Inst : ToU64_t T) (x : (T * T)) : result u64 :=
+  toU64Pair_to_u64 T toU64Inst x
 .
 
 (** [traits::g]:
     Source: 'src/traits.rs', lines 59:0-61:18 *)
 Definition g
-  (T : Type) (toU64TupleTTInst : ToU64_t (T * T)) (x : (T * T)) : result u64 :=
-  toU64TupleTTInst.(ToU64_t_to_u64) x
+  (T : Type) (toU64PairInst : ToU64_t (T * T)) (x : (T * T)) : result u64 :=
+  toU64PairInst.(ToU64_t_to_u64) x
 .
 
 (** [traits::h0]:
     Source: 'src/traits.rs', lines 66:0-66:24 *)
 Definition h0 (x : u64) : result u64 :=
-  u64_to_u64 x.
+  toU64U64_to_u64 x.
 
 (** [traits::Wrapper]
     Source: 'src/traits.rs', lines 70:0-70:21 *)
@@ -133,31 +128,31 @@ Record Wrapper_t (T : Type) := mkWrapper_t { wrapper_x : T; }.
 Arguments mkWrapper_t { _ }.
 Arguments wrapper_x { _ }.
 
-(** [traits::{traits::Wrapper<T>#4}::to_u64]:
+(** [traits::{(traits::ToU64 for traits::Wrapper<T>)#4}::to_u64]:
     Source: 'src/traits.rs', lines 75:4-75:26 *)
-Definition wrapper_to_u64
-  (T : Type) (toU64TInst : ToU64_t T) (self : Wrapper_t T) : result u64 :=
-  toU64TInst.(ToU64_t_to_u64) self.(wrapper_x)
+Definition toU64traitsWrapper_to_u64
+  (T : Type) (toU64Inst : ToU64_t T) (self : Wrapper_t T) : result u64 :=
+  toU64Inst.(ToU64_t_to_u64) self.(wrapper_x)
 .
 
-(** Trait implementation: [traits::{traits::Wrapper<T>#4}]
+(** Trait implementation: [traits::{(traits::ToU64 for traits::Wrapper<T>)#4}]
     Source: 'src/traits.rs', lines 74:0-74:35 *)
-Definition traits_ToU64traitsWrapperTInst (T : Type) (toU64TInst : ToU64_t T) :
-  ToU64_t (Wrapper_t T) := {|
-  ToU64_t_to_u64 := wrapper_to_u64 T toU64TInst;
+Definition ToU64traitsWrapper (T : Type) (toU64Inst : ToU64_t T) : ToU64_t
+  (Wrapper_t T) := {|
+  ToU64_t_to_u64 := toU64traitsWrapper_to_u64 T toU64Inst;
 |}.
 
 (** [traits::h1]:
     Source: 'src/traits.rs', lines 80:0-80:33 *)
 Definition h1 (x : Wrapper_t u64) : result u64 :=
-  wrapper_to_u64 u64 traits_ToU64U64Inst x
+  toU64traitsWrapper_to_u64 u64 ToU64U64 x
 .
 
 (** [traits::h2]:
     Source: 'src/traits.rs', lines 84:0-84:41 *)
 Definition h2
-  (T : Type) (toU64TInst : ToU64_t T) (x : Wrapper_t T) : result u64 :=
-  wrapper_to_u64 T toU64TInst x
+  (T : Type) (toU64Inst : ToU64_t T) (x : Wrapper_t T) : result u64 :=
+  toU64traitsWrapper_to_u64 T toU64Inst x
 .
 
 (** Trait declaration: [traits::ToType]
@@ -169,22 +164,23 @@ Record ToType_t (Self T : Type) := mkToType_t {
 Arguments mkToType_t { _ _ }.
 Arguments ToType_t_to_type { _ _ }.
 
-(** [traits::{u64#5}::to_type]:
+(** [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
     Source: 'src/traits.rs', lines 93:4-93:28 *)
-Definition u64_to_type (self : u64) : result bool :=
-  Return (self s> 0%u64).
+Definition toTypeU64Bool_to_type (self : u64) : result bool :=
+  Return (self s> 0%u64)
+.
 
-(** Trait implementation: [traits::{u64#5}]
+(** Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
     Source: 'src/traits.rs', lines 92:0-92:25 *)
-Definition traits_ToTypeU64BoolInst : ToType_t u64 bool := {|
-  ToType_t_to_type := u64_to_type;
+Definition ToTypeU64Bool : ToType_t u64 bool := {|
+  ToType_t_to_type := toTypeU64Bool_to_type;
 |}.
 
 (** Trait declaration: [traits::OfType]
     Source: 'src/traits.rs', lines 98:0-98:16 *)
 Record OfType_t (Self : Type) := mkOfType_t {
-  OfType_t_of_type : forall (T : Type) (toTypeTSelfInst : ToType_t T Self), T
-    -> result Self;
+  OfType_t_of_type : forall (T : Type) (toTypeInst : ToType_t T Self), T ->
+    result Self;
 }.
 
 Arguments mkOfType_t { _ }.
@@ -193,32 +189,32 @@ Arguments OfType_t_of_type { _ }.
 (** [traits::h3]:
     Source: 'src/traits.rs', lines 104:0-104:50 *)
 Definition h3
-  (T1 T2 : Type) (ofTypeT1Inst : OfType_t T1) (toTypeT2T1Inst : ToType_t T2 T1)
+  (T1 T2 : Type) (ofTypeInst : OfType_t T1) (toTypeInst : ToType_t T2 T1)
   (y : T2) :
   result T1
   :=
-  ofTypeT1Inst.(OfType_t_of_type) T2 toTypeT2T1Inst y
+  ofTypeInst.(OfType_t_of_type) T2 toTypeInst y
 .
 
 (** Trait declaration: [traits::OfTypeBis]
     Source: 'src/traits.rs', lines 109:0-109:36 *)
 Record OfTypeBis_t (Self T : Type) := mkOfTypeBis_t {
-  OfTypeBis_tOfTypeBis_t_ToTypeTSelfInst : ToType_t T Self;
+  OfTypeBis_tOfTypeBis_t_ToTypeInst : ToType_t T Self;
   OfTypeBis_t_of_type : T -> result Self;
 }.
 
 Arguments mkOfTypeBis_t { _ _ }.
-Arguments OfTypeBis_tOfTypeBis_t_ToTypeTSelfInst { _ _ }.
+Arguments OfTypeBis_tOfTypeBis_t_ToTypeInst { _ _ }.
 Arguments OfTypeBis_t_of_type { _ _ }.
 
 (** [traits::h4]:
     Source: 'src/traits.rs', lines 118:0-118:57 *)
 Definition h4
-  (T1 T2 : Type) (ofTypeBisT1T2Inst : OfTypeBis_t T1 T2) (toTypeT2T1Inst :
-  ToType_t T2 T1) (y : T2) :
+  (T1 T2 : Type) (ofTypeBisInst : OfTypeBis_t T1 T2) (toTypeInst : ToType_t T2
+  T1) (y : T2) :
   result T1
   :=
-  ofTypeBisT1T2Inst.(OfTypeBis_t_of_type) y
+  ofTypeBisInst.(OfTypeBis_t_of_type) y
 .
 
 (** [traits::TestType]
@@ -238,54 +234,59 @@ Record TestType_test_TestTrait_t (Self : Type) := mkTestType_test_TestTrait_t {
 Arguments mkTestType_test_TestTrait_t { _ }.
 Arguments TestType_test_TestTrait_t_test { _ }.
 
-(** [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}::test]:
+(** [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}::test]:
     Source: 'src/traits.rs', lines 139:12-139:34 *)
-Definition testType_test_TestType1_test
+Definition testType_test_TestTraittraitsTestTypetestTestType1_test
   (self : TestType_test_TestType1_t) : result bool :=
   Return (self s> 1%u64)
 .
 
-(** Trait implementation: [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}]
+(** Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}]
     Source: 'src/traits.rs', lines 138:8-138:36 *)
-Definition traits_TestType_test_TestTraittraitstraitsTestTypeTtestTestType1Inst
-  : TestType_test_TestTrait_t TestType_test_TestType1_t := {|
-  TestType_test_TestTrait_t_test := testType_test_TestType1_test;
+Definition TestType_test_TestTraittraitsTestTypetestTestType1 :
+  TestType_test_TestTrait_t TestType_test_TestType1_t := {|
+  TestType_test_TestTrait_t_test :=
+    testType_test_TestTraittraitsTestTypetestTestType1_test;
 |}.
 
 (** [traits::{traits::TestType<T>#6}::test]:
     Source: 'src/traits.rs', lines 126:4-126:36 *)
 Definition testType_test
-  (T : Type) (toU64TInst : ToU64_t T) (self : TestType_t T) (x : T) :
+  (T : Type) (toU64Inst : ToU64_t T) (self : TestType_t T) (x : T) :
   result bool
   :=
-  x1 <- toU64TInst.(ToU64_t_to_u64) x;
-  if x1 s> 0%u64 then testType_test_TestType1_test 0%u64 else Return false
+  x1 <- toU64Inst.(ToU64_t_to_u64) x;
+  if x1 s> 0%u64
+  then testType_test_TestTraittraitsTestTypetestTestType1_test 0%u64
+  else Return false
 .
 
 (** [traits::BoolWrapper]
     Source: 'src/traits.rs', lines 150:0-150:22 *)
 Definition BoolWrapper_t : Type := bool.
 
-(** [traits::{traits::BoolWrapper#7}::to_type]:
+(** [traits::{(traits::ToType<T> for traits::BoolWrapper)#7}::to_type]:
     Source: 'src/traits.rs', lines 156:4-156:25 *)
-Definition boolWrapper_to_type
+Definition toTypetraitsBoolWrapperT_to_type
   (T : Type) (toTypeBoolTInst : ToType_t bool T) (self : BoolWrapper_t) :
   result T
   :=
   toTypeBoolTInst.(ToType_t_to_type) self
 .
 
-(** Trait implementation: [traits::{traits::BoolWrapper#7}]
+(** Trait implementation: [traits::{(traits::ToType<T> for traits::BoolWrapper)#7}]
     Source: 'src/traits.rs', lines 152:0-152:33 *)
-Definition traits_ToTypetraitsBoolWrapperTInst (T : Type) (toTypeBoolTInst :
-  ToType_t bool T) : ToType_t BoolWrapper_t T := {|
-  ToType_t_to_type := boolWrapper_to_type T toTypeBoolTInst;
+Definition ToTypetraitsBoolWrapperT (T : Type) (toTypeBoolTInst : ToType_t bool
+  T) : ToType_t BoolWrapper_t T := {|
+  ToType_t_to_type := toTypetraitsBoolWrapperT_to_type T toTypeBoolTInst;
 |}.
 
 (** [traits::WithConstTy::LEN2]
     Source: 'src/traits.rs', lines 164:4-164:21 *)
-Definition with_const_ty_len2_body : result usize := Return 32%usize.
-Definition with_const_ty_len2_c : usize := with_const_ty_len2_body%global.
+Definition with_const_ty_len2_default_body : result usize := Return 32%usize.
+Definition with_const_ty_len2_default : usize :=
+  with_const_ty_len2_default_body%global
+.
 
 (** Trait declaration: [traits::WithConstTy]
     Source: 'src/traits.rs', lines 161:0-161:39 *)
@@ -307,41 +308,45 @@ Arguments WithConstTy_tWithConstTy_t_W { _ _ }.
 Arguments WithConstTy_tWithConstTy_t_W_clause_0 { _ _ }.
 Arguments WithConstTy_t_f { _ _ }.
 
-(** [traits::{bool#8}::LEN1]
+(** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
     Source: 'src/traits.rs', lines 175:4-175:21 *)
-Definition bool_len1_body : result usize := Return 12%usize.
-Definition bool_len1_c : usize := bool_len1_body%global.
+Definition with_const_ty_bool32_len1_body : result usize := Return 12%usize.
+Definition with_const_ty_bool32_len1 : usize :=
+  with_const_ty_bool32_len1_body%global
+.
 
-(** [traits::{bool#8}::f]:
+(** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::f]:
     Source: 'src/traits.rs', lines 180:4-180:39 *)
-Definition bool_f (i : u64) (a : array u8 32%usize) : result u64 :=
-  Return i.
+Definition withConstTyBool32_f
+  (i : u64) (a : array u8 32%usize) : result u64 :=
+  Return i
+.
 
-(** Trait implementation: [traits::{bool#8}]
+(** Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}]
     Source: 'src/traits.rs', lines 174:0-174:29 *)
-Definition traits_WithConstTyBool32Inst : WithConstTy_t bool 32%usize := {|
-  WithConstTy_tWithConstTy_t_LEN1 := bool_len1_c;
-  WithConstTy_tWithConstTy_t_LEN2 := with_const_ty_len2_c;
+Definition WithConstTyBool32 : WithConstTy_t bool 32%usize := {|
+  WithConstTy_tWithConstTy_t_LEN1 := with_const_ty_bool32_len1;
+  WithConstTy_tWithConstTy_t_LEN2 := with_const_ty_len2_default;
   WithConstTy_tWithConstTy_t_V := u8;
   WithConstTy_tWithConstTy_t_W := u64;
-  WithConstTy_tWithConstTy_t_W_clause_0 := traits_ToU64U64Inst;
-  WithConstTy_t_f := bool_f;
+  WithConstTy_tWithConstTy_t_W_clause_0 := ToU64U64;
+  WithConstTy_t_f := withConstTyBool32_f;
 |}.
 
 (** [traits::use_with_const_ty1]:
     Source: 'src/traits.rs', lines 183:0-183:75 *)
 Definition use_with_const_ty1
-  (H : Type) (LEN : usize) (withConstTyHLENInst : WithConstTy_t H LEN) :
+  (H : Type) (LEN : usize) (withConstTyInst : WithConstTy_t H LEN) :
   result usize
   :=
-  Return withConstTyHLENInst.(WithConstTy_tWithConstTy_t_LEN1)
+  Return withConstTyInst.(WithConstTy_tWithConstTy_t_LEN1)
 .
 
 (** [traits::use_with_const_ty2]:
     Source: 'src/traits.rs', lines 187:0-187:73 *)
 Definition use_with_const_ty2
-  (H : Type) (LEN : usize) (withConstTyHLENInst : WithConstTy_t H LEN)
-  (w : withConstTyHLENInst.(WithConstTy_tWithConstTy_t_W)) :
+  (H : Type) (LEN : usize) (withConstTyInst : WithConstTy_t H LEN)
+  (w : withConstTyInst.(WithConstTy_tWithConstTy_t_W)) :
   result unit
   :=
   Return tt
@@ -350,12 +355,11 @@ Definition use_with_const_ty2
 (** [traits::use_with_const_ty3]:
     Source: 'src/traits.rs', lines 189:0-189:80 *)
 Definition use_with_const_ty3
-  (H : Type) (LEN : usize) (withConstTyHLENInst : WithConstTy_t H LEN)
-  (x : withConstTyHLENInst.(WithConstTy_tWithConstTy_t_W)) :
+  (H : Type) (LEN : usize) (withConstTyInst : WithConstTy_t H LEN)
+  (x : withConstTyInst.(WithConstTy_tWithConstTy_t_W)) :
   result u64
   :=
-  withConstTyHLENInst.(WithConstTy_tWithConstTy_t_W_clause_0).(ToU64_t_to_u64)
-    x
+  withConstTyInst.(WithConstTy_tWithConstTy_t_W_clause_0).(ToU64_t_to_u64) x
 .
 
 (** [traits::test_where1]:
@@ -394,37 +398,37 @@ Arguments mkParentTrait1_t { _ }.
 (** Trait declaration: [traits::ChildTrait]
     Source: 'src/traits.rs', lines 206:0-206:49 *)
 Record ChildTrait_t (Self : Type) := mkChildTrait_t {
-  ChildTrait_tChildTrait_t_ParentTrait0SelfInst : ParentTrait0_t Self;
-  ChildTrait_tChildTrait_t_ParentTrait1SelfInst : ParentTrait1_t Self;
+  ChildTrait_tChildTrait_t_ParentTrait0Inst : ParentTrait0_t Self;
+  ChildTrait_tChildTrait_t_ParentTrait1Inst : ParentTrait1_t Self;
 }.
 
 Arguments mkChildTrait_t { _ }.
-Arguments ChildTrait_tChildTrait_t_ParentTrait0SelfInst { _ }.
-Arguments ChildTrait_tChildTrait_t_ParentTrait1SelfInst { _ }.
+Arguments ChildTrait_tChildTrait_t_ParentTrait0Inst { _ }.
+Arguments ChildTrait_tChildTrait_t_ParentTrait1Inst { _ }.
 
 (** [traits::test_child_trait1]:
     Source: 'src/traits.rs', lines 209:0-209:56 *)
 Definition test_child_trait1
-  (T : Type) (childTraitTInst : ChildTrait_t T) (x : T) : result string :=
-  childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_name)
+  (T : Type) (childTraitInst : ChildTrait_t T) (x : T) : result string :=
+  childTraitInst.(ChildTrait_tChildTrait_t_ParentTrait0Inst).(ParentTrait0_t_get_name)
     x
 .
 
 (** [traits::test_child_trait2]:
     Source: 'src/traits.rs', lines 213:0-213:54 *)
 Definition test_child_trait2
-  (T : Type) (childTraitTInst : ChildTrait_t T) (x : T) :
+  (T : Type) (childTraitInst : ChildTrait_t T) (x : T) :
   result
-    childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_tParentTrait0_t_W)
+    childTraitInst.(ChildTrait_tChildTrait_t_ParentTrait0Inst).(ParentTrait0_tParentTrait0_t_W)
   :=
-  childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_w)
+  childTraitInst.(ChildTrait_tChildTrait_t_ParentTrait0Inst).(ParentTrait0_t_get_w)
     x
 .
 
 (** [traits::order1]:
     Source: 'src/traits.rs', lines 219:0-219:59 *)
 Definition order1
-  (T U : Type) (parentTrait0TInst : ParentTrait0_t T) (parentTrait0UInst :
+  (T U : Type) (parentTrait0Inst : ParentTrait0_t T) (parentTrait0Inst1 :
   ParentTrait0_t U) :
   result unit
   :=
@@ -434,22 +438,20 @@ Definition order1
 (** Trait declaration: [traits::ChildTrait1]
     Source: 'src/traits.rs', lines 222:0-222:35 *)
 Record ChildTrait1_t (Self : Type) := mkChildTrait1_t {
-  ChildTrait1_tChildTrait1_t_ParentTrait1SelfInst : ParentTrait1_t Self;
+  ChildTrait1_tChildTrait1_t_ParentTrait1Inst : ParentTrait1_t Self;
 }.
 
 Arguments mkChildTrait1_t { _ }.
-Arguments ChildTrait1_tChildTrait1_t_ParentTrait1SelfInst { _ }.
+Arguments ChildTrait1_tChildTrait1_t_ParentTrait1Inst { _ }.
 
-(** Trait implementation: [traits::{usize#9}]
+(** Trait implementation: [traits::{(traits::ParentTrait1 for usize)#9}]
     Source: 'src/traits.rs', lines 224:0-224:27 *)
-Definition traits_ParentTrait1UsizeInst : ParentTrait1_t usize
-  := mkParentTrait1_t.
+Definition ParentTrait1Usize : ParentTrait1_t usize := mkParentTrait1_t.
 
-(** Trait implementation: [traits::{usize#10}]
+(** Trait implementation: [traits::{(traits::ChildTrait1 for usize)#10}]
     Source: 'src/traits.rs', lines 225:0-225:26 *)
-Definition traits_ChildTrait1UsizeInst : ChildTrait1_t usize := {|
-  ChildTrait1_tChildTrait1_t_ParentTrait1SelfInst :=
-    traits_ParentTrait1UsizeInst;
+Definition ChildTrait1Usize : ChildTrait1_t usize := {|
+  ChildTrait1_tChildTrait1_t_ParentTrait1Inst := ParentTrait1Usize;
 |}.
 
 (** Trait declaration: [traits::Iterator]
@@ -488,13 +490,13 @@ Arguments mkFromResidual_t { _ _ }.
     Source: 'src/traits.rs', lines 246:0-246:48 *)
 Record Try_t (Self : Type) := mkTry_t {
   Try_tTry_t_Residual : Type;
-  Try_tTry_t_FromResidualSelftraitsTrySelfResidualInst : FromResidual_t Self
+  Try_tTry_t_FromResidualSelftraitsTryResidualInst : FromResidual_t Self
     Try_tTry_t_Residual;
 }.
 
 Arguments mkTry_t { _ }.
 Arguments Try_tTry_t_Residual { _ }.
-Arguments Try_tTry_t_FromResidualSelftraitsTrySelfResidualInst { _ }.
+Arguments Try_tTry_t_FromResidualSelftraitsTryResidualInst { _ }.
 
 (** Trait declaration: [traits::WithTarget]
     Source: 'src/traits.rs', lines 252:0-252:20 *)
@@ -520,41 +522,40 @@ Arguments ParentTrait2_tParentTrait2_t_U_clause_0 { _ }.
 (** Trait declaration: [traits::ChildTrait2]
     Source: 'src/traits.rs', lines 260:0-260:35 *)
 Record ChildTrait2_t (Self : Type) := mkChildTrait2_t {
-  ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst : ParentTrait2_t Self;
+  ChildTrait2_tChildTrait2_t_ParentTrait2Inst : ParentTrait2_t Self;
   ChildTrait2_t_convert :
-    (ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst).(ParentTrait2_tParentTrait2_t_U)
+    (ChildTrait2_tChildTrait2_t_ParentTrait2Inst).(ParentTrait2_tParentTrait2_t_U)
     -> result
-    (ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst).(ParentTrait2_tParentTrait2_t_U_clause_0).(WithTarget_tWithTarget_t_Target);
+    (ChildTrait2_tChildTrait2_t_ParentTrait2Inst).(ParentTrait2_tParentTrait2_t_U_clause_0).(WithTarget_tWithTarget_t_Target);
 }.
 
 Arguments mkChildTrait2_t { _ }.
-Arguments ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst { _ }.
+Arguments ChildTrait2_tChildTrait2_t_ParentTrait2Inst { _ }.
 Arguments ChildTrait2_t_convert { _ }.
 
-(** Trait implementation: [traits::{u32#11}]
+(** Trait implementation: [traits::{(traits::WithTarget for u32)#11}]
     Source: 'src/traits.rs', lines 264:0-264:23 *)
-Definition traits_WithTargetU32Inst : WithTarget_t u32 := {|
+Definition WithTargetU32 : WithTarget_t u32 := {|
   WithTarget_tWithTarget_t_Target := u32;
 |}.
 
-(** Trait implementation: [traits::{u32#12}]
+(** Trait implementation: [traits::{(traits::ParentTrait2 for u32)#12}]
     Source: 'src/traits.rs', lines 268:0-268:25 *)
-Definition traits_ParentTrait2U32Inst : ParentTrait2_t u32 := {|
+Definition ParentTrait2U32 : ParentTrait2_t u32 := {|
   ParentTrait2_tParentTrait2_t_U := u32;
-  ParentTrait2_tParentTrait2_t_U_clause_0 := traits_WithTargetU32Inst;
+  ParentTrait2_tParentTrait2_t_U_clause_0 := WithTargetU32;
 |}.
 
-(** [traits::{u32#13}::convert]:
+(** [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
     Source: 'src/traits.rs', lines 273:4-273:29 *)
-Definition u32_convert (x : u32) : result u32 :=
+Definition childTrait2U32_convert (x : u32) : result u32 :=
   Return x.
 
-(** Trait implementation: [traits::{u32#13}]
+(** Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}]
     Source: 'src/traits.rs', lines 272:0-272:24 *)
-Definition traits_ChildTrait2U32Inst : ChildTrait2_t u32 := {|
-  ChildTrait2_tChildTrait2_t_ParentTrait2SelfInst :=
-    traits_ParentTrait2U32Inst;
-  ChildTrait2_t_convert := u32_convert;
+Definition ChildTrait2U32 : ChildTrait2_t u32 := {|
+  ChildTrait2_tChildTrait2_t_ParentTrait2Inst := ParentTrait2U32;
+  ChildTrait2_t_convert := childTrait2U32_convert;
 |}.
 
 (** Trait declaration: [traits::CFnOnce]
@@ -571,26 +572,25 @@ Arguments CFnOnce_t_call_once { _ _ }.
 (** Trait declaration: [traits::CFnMut]
     Source: 'src/traits.rs', lines 292:0-292:37 *)
 Record CFnMut_t (Self Args : Type) := mkCFnMut_t {
-  CFnMut_tCFnMut_t_CFnOnceSelfArgsInst : CFnOnce_t Self Args;
+  CFnMut_tCFnMut_t_CFnOnceInst : CFnOnce_t Self Args;
   CFnMut_t_call_mut : Self -> Args -> result
-    ((CFnMut_tCFnMut_t_CFnOnceSelfArgsInst).(CFnOnce_tCFnOnce_t_Output) *
-    Self);
+    ((CFnMut_tCFnMut_t_CFnOnceInst).(CFnOnce_tCFnOnce_t_Output) * Self);
 }.
 
 Arguments mkCFnMut_t { _ _ }.
-Arguments CFnMut_tCFnMut_t_CFnOnceSelfArgsInst { _ _ }.
+Arguments CFnMut_tCFnMut_t_CFnOnceInst { _ _ }.
 Arguments CFnMut_t_call_mut { _ _ }.
 
 (** Trait declaration: [traits::CFn]
     Source: 'src/traits.rs', lines 296:0-296:33 *)
 Record CFn_t (Self Args : Type) := mkCFn_t {
-  CFn_tCFn_t_CFnMutSelfArgsInst : CFnMut_t Self Args;
+  CFn_tCFn_t_CFnMutInst : CFnMut_t Self Args;
   CFn_t_call : Self -> Args -> result
-    (CFn_tCFn_t_CFnMutSelfArgsInst).(CFnMut_tCFnMut_t_CFnOnceSelfArgsInst).(CFnOnce_tCFnOnce_t_Output);
+    (CFn_tCFn_t_CFnMutInst).(CFnMut_tCFnMut_t_CFnOnceInst).(CFnOnce_tCFnOnce_t_Output);
 }.
 
 Arguments mkCFn_t { _ _ }.
-Arguments CFn_tCFn_t_CFnMutSelfArgsInst { _ _ }.
+Arguments CFn_tCFn_t_CFnMutInst { _ _ }.
 Arguments CFn_t_call { _ _ }.
 
 (** Trait declaration: [traits::GetTrait]
@@ -607,10 +607,10 @@ Arguments GetTrait_t_get_w { _ }.
 (** [traits::test_get_trait]:
     Source: 'src/traits.rs', lines 305:0-305:49 *)
 Definition test_get_trait
-  (T : Type) (getTraitTInst : GetTrait_t T) (x : T) :
-  result getTraitTInst.(GetTrait_tGetTrait_t_W)
+  (T : Type) (getTraitInst : GetTrait_t T) (x : T) :
+  result getTraitInst.(GetTrait_tGetTrait_t_W)
   :=
-  getTraitTInst.(GetTrait_t_get_w) x
+  getTraitInst.(GetTrait_t_get_w) x
 .
 
 End Traits.
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index ac57b8fc..cf0f4f8b 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -398,7 +398,7 @@ let f3 : result u32 =
 (** [arrays::SZ]
     Source: 'src/arrays.rs', lines 286:0-286:19 *)
 let sz_body : result usize = Return 32
-let sz_c : usize = eval_global sz_body
+let sz : usize = eval_global sz_body
 
 (** [arrays::f5]:
     Source: 'src/arrays.rs', lines 289:0-289:31 *)
diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
index 537705c5..de56ba46 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
@@ -22,7 +22,7 @@ let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
 (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
     Source: 'src/betree.rs', lines 339:4-339:73 *)
 unfold
-let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
+let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0)
   (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
   admit ()
 
diff --git a/tests/fstar/betree/BetreeMain.Clauses.fst b/tests/fstar/betree/BetreeMain.Clauses.fst
index 21f953d1..ed5c5069 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_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
+let betree_ListPairU64T_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 196f120c..ec042fb3 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -134,7 +134,7 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
 
 (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
     Source: 'src/betree.rs', lines 327:4-327:44 *)
-let betree_ListTupleU64T_head_has_key
+let betree_ListPairU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
   begin match self with
   | Betree_List_Cons hd _ -> let (i, _) = hd in Return (i = key)
@@ -143,10 +143,10 @@ let betree_ListTupleU64T_head_has_key
 
 (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
     Source: 'src/betree.rs', lines 339:4-339:73 *)
-let rec betree_ListTupleU64T_partition_at_pivot
+let rec betree_ListPairU64T_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_ListTupleU64T_partition_at_pivot_decreases t self pivot))
+  (decreases (betree_ListPairU64T_partition_at_pivot_decreases t self pivot))
   =
   begin match self with
   | Betree_List_Cons hd tl ->
@@ -154,7 +154,7 @@ let rec betree_ListTupleU64T_partition_at_pivot
     if i >= pivot
     then Return (Betree_List_Nil, Betree_List_Cons (i, x) tl)
     else
-      let* p = betree_ListTupleU64T_partition_at_pivot t tl pivot in
+      let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in
       let (ls0, ls1) = p in
       Return (Betree_List_Cons (i, x) ls0, ls1)
   | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil)
@@ -228,7 +228,7 @@ let rec betree_Node_apply_upserts
   Tot (result (state & (u64 & (betree_List_t (u64 & betree_Message_t)))))
   (decreases (betree_Node_apply_upserts_decreases msgs prev key st))
   =
-  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in
+  let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in
   if b
   then
     let* (msg, l) = betree_List_pop_front (u64 & betree_Message_t) msgs in
@@ -369,7 +369,7 @@ let betree_Node_apply_to_internal
   =
   let* (msgs1, lookup_first_message_for_key_back) =
     betree_Node_lookup_first_message_for_key key msgs in
-  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs1 key in
+  let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs1 key in
   if b
   then
     begin match new_msg with
@@ -467,7 +467,7 @@ let betree_Node_apply_to_leaf
   =
   let* (bindings1, lookup_mut_in_bindings_back) =
     betree_Node_lookup_mut_in_bindings key bindings in
-  let* b = betree_ListTupleU64T_head_has_key u64 bindings1 key in
+  let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in
   if b
   then
     let* (hd, l) = betree_List_pop_front (u64 & u64) bindings1 in
@@ -522,7 +522,7 @@ let rec betree_Internal_flush
     betree_Internal_flush_decreases self params node_id_cnt content st))
   =
   let* p =
-    betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot
+    betree_ListPairU64T_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
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
index 537705c5..de56ba46 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
@@ -22,7 +22,7 @@ let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
 (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
     Source: 'src/betree.rs', lines 339:4-339:73 *)
 unfold
-let betree_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
+let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0)
   (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
   admit ()
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.fst
index 21f953d1..ed5c5069 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_ListTupleU64T_partition_at_pivot_decreases (t : Type0)
+let betree_ListPairU64T_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 196f120c..ec042fb3 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -134,7 +134,7 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
 
 (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
     Source: 'src/betree.rs', lines 327:4-327:44 *)
-let betree_ListTupleU64T_head_has_key
+let betree_ListPairU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
   begin match self with
   | Betree_List_Cons hd _ -> let (i, _) = hd in Return (i = key)
@@ -143,10 +143,10 @@ let betree_ListTupleU64T_head_has_key
 
 (** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
     Source: 'src/betree.rs', lines 339:4-339:73 *)
-let rec betree_ListTupleU64T_partition_at_pivot
+let rec betree_ListPairU64T_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_ListTupleU64T_partition_at_pivot_decreases t self pivot))
+  (decreases (betree_ListPairU64T_partition_at_pivot_decreases t self pivot))
   =
   begin match self with
   | Betree_List_Cons hd tl ->
@@ -154,7 +154,7 @@ let rec betree_ListTupleU64T_partition_at_pivot
     if i >= pivot
     then Return (Betree_List_Nil, Betree_List_Cons (i, x) tl)
     else
-      let* p = betree_ListTupleU64T_partition_at_pivot t tl pivot in
+      let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in
       let (ls0, ls1) = p in
       Return (Betree_List_Cons (i, x) ls0, ls1)
   | Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil)
@@ -228,7 +228,7 @@ let rec betree_Node_apply_upserts
   Tot (result (state & (u64 & (betree_List_t (u64 & betree_Message_t)))))
   (decreases (betree_Node_apply_upserts_decreases msgs prev key st))
   =
-  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs key in
+  let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in
   if b
   then
     let* (msg, l) = betree_List_pop_front (u64 & betree_Message_t) msgs in
@@ -369,7 +369,7 @@ let betree_Node_apply_to_internal
   =
   let* (msgs1, lookup_first_message_for_key_back) =
     betree_Node_lookup_first_message_for_key key msgs in
-  let* b = betree_ListTupleU64T_head_has_key betree_Message_t msgs1 key in
+  let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs1 key in
   if b
   then
     begin match new_msg with
@@ -467,7 +467,7 @@ let betree_Node_apply_to_leaf
   =
   let* (bindings1, lookup_mut_in_bindings_back) =
     betree_Node_lookup_mut_in_bindings key bindings in
-  let* b = betree_ListTupleU64T_head_has_key u64 bindings1 key in
+  let* b = betree_ListPairU64T_head_has_key u64 bindings1 key in
   if b
   then
     let* (hd, l) = betree_List_pop_front (u64 & u64) bindings1 in
@@ -522,7 +522,7 @@ let rec betree_Internal_flush
     betree_Internal_flush_decreases self params node_id_cnt content st))
   =
   let* p =
-    betree_ListTupleU64T_partition_at_pivot betree_Message_t content self.pivot
+    betree_ListPairU64T_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
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index f9082979..d13d2ba3 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -121,18 +121,18 @@ let rec i32_id (n : nat) (i : i32) : result i32 =
     Source: 'src/demo.rs', lines 83:0-83:17 *)
 noeq type counter_t (self : Type0) = { incr : self -> result (usize & self); }
 
-(** [demo::{usize}::incr]:
+(** [demo::{(demo::Counter for usize)}::incr]:
     Source: 'src/demo.rs', lines 88:4-88:31 *)
-let usize_incr (self : usize) : result (usize & usize) =
+let counterUsize_incr (self : usize) : result (usize & usize) =
   let* self1 = usize_add self 1 in Return (self, self1)
 
-(** Trait implementation: [demo::{usize}]
+(** Trait implementation: [demo::{(demo::Counter for usize)}]
     Source: 'src/demo.rs', lines 87:0-87:22 *)
-let demo_CounterUsizeInst : counter_t usize = { incr = usize_incr; }
+let counterUsize : counter_t usize = { incr = counterUsize_incr; }
 
 (** [demo::use_counter]:
     Source: 'src/demo.rs', lines 95:0-95:59 *)
 let use_counter
-  (t : Type0) (counterTInst : counter_t t) (cnt : t) : result (usize & t) =
-  counterTInst.incr cnt
+  (t : Type0) (counterInst : counter_t t) (cnt : t) : result (usize & t) =
+  counterInst.incr cnt
 
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index 7bf42b46..66429c80 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -8,17 +8,17 @@ open Primitives
 (** [constants::X0]
     Source: 'src/constants.rs', lines 5:0-5:17 *)
 let x0_body : result u32 = Return 0
-let x0_c : u32 = eval_global x0_body
+let x0 : u32 = eval_global x0_body
 
 (** [constants::X1]
     Source: 'src/constants.rs', lines 7:0-7:17 *)
 let x1_body : result u32 = Return core_u32_max
-let x1_c : u32 = eval_global x1_body
+let x1 : u32 = eval_global x1_body
 
 (** [constants::X2]
     Source: 'src/constants.rs', lines 10:0-10:17 *)
 let x2_body : result u32 = Return 3
-let x2_c : u32 = eval_global x2_body
+let x2 : u32 = eval_global x2_body
 
 (** [constants::incr]:
     Source: 'src/constants.rs', lines 17:0-17:32 *)
@@ -28,12 +28,12 @@ let incr (n : u32) : result u32 =
 (** [constants::X3]
     Source: 'src/constants.rs', lines 15:0-15:17 *)
 let x3_body : result u32 = incr 32
-let x3_c : u32 = eval_global x3_body
+let x3 : u32 = eval_global x3_body
 
 (** [constants::mk_pair0]:
     Source: 'src/constants.rs', lines 23:0-23:51 *)
-let mk_pair0 (x : u32) (y : u32) : result (u32 & u32) =
-  Return (x, y)
+let mk_pair0 (x : u32) (y1 : u32) : result (u32 & u32) =
+  Return (x, y1)
 
 (** [constants::Pair]
     Source: 'src/constants.rs', lines 36:0-36:23 *)
@@ -41,28 +41,28 @@ type pair_t (t1 t2 : Type0) = { x : t1; y : t2; }
 
 (** [constants::mk_pair1]:
     Source: 'src/constants.rs', lines 27:0-27:55 *)
-let mk_pair1 (x : u32) (y : u32) : result (pair_t u32 u32) =
-  Return { x = x; y = y }
+let mk_pair1 (x : u32) (y1 : u32) : result (pair_t u32 u32) =
+  Return { x = x; y = y1 }
 
 (** [constants::P0]
     Source: 'src/constants.rs', lines 31:0-31:24 *)
 let p0_body : result (u32 & u32) = mk_pair0 0 1
-let p0_c : (u32 & u32) = eval_global p0_body
+let p0 : (u32 & u32) = eval_global p0_body
 
 (** [constants::P1]
     Source: 'src/constants.rs', lines 32:0-32:28 *)
 let p1_body : result (pair_t u32 u32) = mk_pair1 0 1
-let p1_c : pair_t u32 u32 = eval_global p1_body
+let p1 : pair_t u32 u32 = eval_global p1_body
 
 (** [constants::P2]
     Source: 'src/constants.rs', lines 33:0-33:24 *)
 let p2_body : result (u32 & u32) = Return (0, 1)
-let p2_c : (u32 & u32) = eval_global p2_body
+let p2 : (u32 & u32) = eval_global p2_body
 
 (** [constants::P3]
     Source: 'src/constants.rs', lines 34:0-34:28 *)
 let p3_body : result (pair_t u32 u32) = Return { x = 0; y = 1 }
-let p3_c : pair_t u32 u32 = eval_global p3_body
+let p3 : pair_t u32 u32 = eval_global p3_body
 
 (** [constants::Wrap]
     Source: 'src/constants.rs', lines 49:0-49:18 *)
@@ -76,27 +76,27 @@ let wrap_new (t : Type0) (value : t) : result (wrap_t t) =
 (** [constants::Y]
     Source: 'src/constants.rs', lines 41:0-41:22 *)
 let y_body : result (wrap_t i32) = wrap_new i32 2
-let y_c : wrap_t i32 = eval_global y_body
+let y : wrap_t i32 = eval_global y_body
 
 (** [constants::unwrap_y]:
     Source: 'src/constants.rs', lines 43:0-43:30 *)
 let unwrap_y : result i32 =
-  Return y_c.value
+  Return y.value
 
 (** [constants::YVAL]
     Source: 'src/constants.rs', lines 47:0-47:19 *)
 let yval_body : result i32 = unwrap_y
-let yval_c : i32 = eval_global yval_body
+let yval : i32 = eval_global yval_body
 
 (** [constants::get_z1::Z1]
     Source: 'src/constants.rs', lines 62:4-62:17 *)
 let get_z1_z1_body : result i32 = Return 3
-let get_z1_z1_c : i32 = eval_global get_z1_z1_body
+let get_z1_z1 : i32 = eval_global get_z1_z1_body
 
 (** [constants::get_z1]:
     Source: 'src/constants.rs', lines 61:0-61:28 *)
 let get_z1 : result i32 =
-  Return get_z1_z1_c
+  Return get_z1_z1
 
 (** [constants::add]:
     Source: 'src/constants.rs', lines 66:0-66:39 *)
@@ -106,40 +106,40 @@ let add (a : i32) (b : i32) : result i32 =
 (** [constants::Q1]
     Source: 'src/constants.rs', lines 74:0-74:17 *)
 let q1_body : result i32 = Return 5
-let q1_c : i32 = eval_global q1_body
+let q1 : i32 = eval_global q1_body
 
 (** [constants::Q2]
     Source: 'src/constants.rs', lines 75:0-75:17 *)
-let q2_body : result i32 = Return q1_c
-let q2_c : i32 = eval_global q2_body
+let q2_body : result i32 = Return q1
+let q2 : i32 = eval_global q2_body
 
 (** [constants::Q3]
     Source: 'src/constants.rs', lines 76:0-76:17 *)
-let q3_body : result i32 = add q2_c 3
-let q3_c : i32 = eval_global q3_body
+let q3_body : result i32 = add q2 3
+let q3 : i32 = eval_global q3_body
 
 (** [constants::get_z2]:
     Source: 'src/constants.rs', lines 70:0-70:28 *)
 let get_z2 : result i32 =
-  let* i = get_z1 in let* i1 = add i q3_c in add q1_c i1
+  let* i = get_z1 in let* i1 = add i q3 in add q1 i1
 
 (** [constants::S1]
     Source: 'src/constants.rs', lines 80:0-80:18 *)
 let s1_body : result u32 = Return 6
-let s1_c : u32 = eval_global s1_body
+let s1 : u32 = eval_global s1_body
 
 (** [constants::S2]
     Source: 'src/constants.rs', lines 81:0-81:18 *)
-let s2_body : result u32 = incr s1_c
-let s2_c : u32 = eval_global s2_body
+let s2_body : result u32 = incr s1
+let s2 : u32 = eval_global s2_body
 
 (** [constants::S3]
     Source: 'src/constants.rs', lines 82:0-82:29 *)
-let s3_body : result (pair_t u32 u32) = Return p3_c
-let s3_c : pair_t u32 u32 = eval_global s3_body
+let s3_body : result (pair_t u32 u32) = Return p3
+let s3 : pair_t u32 u32 = eval_global s3_body
 
 (** [constants::S4]
     Source: 'src/constants.rs', lines 83:0-83:29 *)
 let s4_body : result (pair_t u32 u32) = mk_pair1 7 8
-let s4_c : pair_t u32 u32 = eval_global s4_body
+let s4 : pair_t u32 u32 = eval_global s4_body
 
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index ffcc32f3..c71f8dbb 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -131,12 +131,12 @@ let mix_arith_i32 (x : i32) (y : i32) (z : i32) : result i32 =
 (** [no_nested_borrows::CONST0]
     Source: 'src/no_nested_borrows.rs', lines 125:0-125:23 *)
 let const0_body : result usize = usize_add 1 1
-let const0_c : usize = eval_global const0_body
+let const0 : usize = eval_global const0_body
 
 (** [no_nested_borrows::CONST1]
     Source: 'src/no_nested_borrows.rs', lines 126:0-126:23 *)
 let const1_body : result usize = usize_mul 2 2
-let const1_c : usize = eval_global const1_body
+let const1 : usize = eval_global const1_body
 
 (** [no_nested_borrows::cast_u32_to_i32]:
     Source: 'src/no_nested_borrows.rs', lines 128:0-128:37 *)
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 0760de2e..466fb482 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -9,14 +9,14 @@ open Primitives
     Source: 'src/traits.rs', lines 1:0-1:19 *)
 noeq type boolTrait_t (self : Type0) = { get_bool : self -> result bool; }
 
-(** [traits::{bool}::get_bool]:
+(** [traits::{(traits::BoolTrait for bool)}::get_bool]:
     Source: 'src/traits.rs', lines 12:4-12:30 *)
-let bool_get_bool (self : bool) : result bool =
+let boolTraitBool_get_bool (self : bool) : result bool =
   Return self
 
-(** Trait implementation: [traits::{bool}]
+(** Trait implementation: [traits::{(traits::BoolTrait for bool)}]
     Source: 'src/traits.rs', lines 11:0-11:23 *)
-let traits_BoolTraitBoolInst : boolTrait_t bool = { get_bool = bool_get_bool; }
+let boolTraitBool : boolTrait_t bool = { get_bool = boolTraitBool_get_bool; }
 
 (** [traits::BoolTrait::ret_true]:
     Source: 'src/traits.rs', lines 6:4-6:30 *)
@@ -29,151 +29,146 @@ let boolTrait_ret_true
 (** [traits::test_bool_trait_bool]:
     Source: 'src/traits.rs', lines 17:0-17:44 *)
 let test_bool_trait_bool (x : bool) : result bool =
-  let* b = bool_get_bool x in
-  if b then boolTrait_ret_true traits_BoolTraitBoolInst x else Return false
+  let* b = boolTraitBool_get_bool x in
+  if b then boolTrait_ret_true boolTraitBool x else Return false
 
-(** [traits::{core::option::Option<T>#1}::get_bool]:
+(** [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]:
     Source: 'src/traits.rs', lines 23:4-23:30 *)
-let option_get_bool (t : Type0) (self : option t) : result bool =
+let boolTraitOption_get_bool (t : Type0) (self : option t) : result bool =
   begin match self with | None -> Return false | Some _ -> Return true end
 
-(** Trait implementation: [traits::{core::option::Option<T>#1}]
+(** Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}]
     Source: 'src/traits.rs', lines 22:0-22:31 *)
-let traits_BoolTraitcoreoptionOptionTInst (t : Type0) : boolTrait_t (option t)
-  = {
-  get_bool = option_get_bool t;
+let boolTraitOption (t : Type0) : boolTrait_t (option t) = {
+  get_bool = boolTraitOption_get_bool t;
 }
 
 (** [traits::test_bool_trait_option]:
     Source: 'src/traits.rs', lines 31:0-31:54 *)
 let test_bool_trait_option (t : Type0) (x : option t) : result bool =
-  let* b = option_get_bool t x in
-  if b
-  then boolTrait_ret_true (traits_BoolTraitcoreoptionOptionTInst t) x
-  else Return false
+  let* b = boolTraitOption_get_bool t x in
+  if b then boolTrait_ret_true (boolTraitOption t) x else Return false
 
 (** [traits::test_bool_trait]:
     Source: 'src/traits.rs', lines 35:0-35:50 *)
 let test_bool_trait
-  (t : Type0) (boolTraitTInst : boolTrait_t t) (x : t) : result bool =
-  boolTraitTInst.get_bool x
+  (t : Type0) (boolTraitInst : boolTrait_t t) (x : t) : result bool =
+  boolTraitInst.get_bool x
 
 (** Trait declaration: [traits::ToU64]
     Source: 'src/traits.rs', lines 39:0-39:15 *)
 noeq type toU64_t (self : Type0) = { to_u64 : self -> result u64; }
 
-(** [traits::{u64#2}::to_u64]:
+(** [traits::{(traits::ToU64 for u64)#2}::to_u64]:
     Source: 'src/traits.rs', lines 44:4-44:26 *)
-let u64_to_u64 (self : u64) : result u64 =
+let toU64U64_to_u64 (self : u64) : result u64 =
   Return self
 
-(** Trait implementation: [traits::{u64#2}]
+(** Trait implementation: [traits::{(traits::ToU64 for u64)#2}]
     Source: 'src/traits.rs', lines 43:0-43:18 *)
-let traits_ToU64U64Inst : toU64_t u64 = { to_u64 = u64_to_u64; }
+let toU64U64 : toU64_t u64 = { to_u64 = toU64U64_to_u64; }
 
-(** [traits::{(A, A)#3}::to_u64]:
+(** [traits::{(traits::ToU64 for (A, A))#3}::to_u64]:
     Source: 'src/traits.rs', lines 50:4-50:26 *)
-let pair_to_u64
-  (a : Type0) (toU64AInst : toU64_t a) (self : (a & a)) : result u64 =
+let toU64Pair_to_u64
+  (a : Type0) (toU64Inst : toU64_t a) (self : (a & a)) : result u64 =
   let (x, x1) = self in
-  let* i = toU64AInst.to_u64 x in
-  let* i1 = toU64AInst.to_u64 x1 in
+  let* i = toU64Inst.to_u64 x in
+  let* i1 = toU64Inst.to_u64 x1 in
   u64_add i i1
 
-(** Trait implementation: [traits::{(A, A)#3}]
+(** Trait implementation: [traits::{(traits::ToU64 for (A, A))#3}]
     Source: 'src/traits.rs', lines 49:0-49:31 *)
-let traits_ToU64TupleAAInst (a : Type0) (toU64AInst : toU64_t a) : toU64_t (a &
-  a) = {
-  to_u64 = pair_to_u64 a toU64AInst;
+let toU64Pair (a : Type0) (toU64Inst : toU64_t a) : toU64_t (a & a) = {
+  to_u64 = toU64Pair_to_u64 a toU64Inst;
 }
 
 (** [traits::f]:
     Source: 'src/traits.rs', lines 55:0-55:36 *)
-let f (t : Type0) (toU64TInst : toU64_t t) (x : (t & t)) : result u64 =
-  pair_to_u64 t toU64TInst x
+let f (t : Type0) (toU64Inst : toU64_t t) (x : (t & t)) : result u64 =
+  toU64Pair_to_u64 t toU64Inst x
 
 (** [traits::g]:
     Source: 'src/traits.rs', lines 59:0-61:18 *)
 let g
-  (t : Type0) (toU64TupleTTInst : toU64_t (t & t)) (x : (t & t)) : result u64 =
-  toU64TupleTTInst.to_u64 x
+  (t : Type0) (toU64PairInst : toU64_t (t & t)) (x : (t & t)) : result u64 =
+  toU64PairInst.to_u64 x
 
 (** [traits::h0]:
     Source: 'src/traits.rs', lines 66:0-66:24 *)
 let h0 (x : u64) : result u64 =
-  u64_to_u64 x
+  toU64U64_to_u64 x
 
 (** [traits::Wrapper]
     Source: 'src/traits.rs', lines 70:0-70:21 *)
 type wrapper_t (t : Type0) = { x : t; }
 
-(** [traits::{traits::Wrapper<T>#4}::to_u64]:
+(** [traits::{(traits::ToU64 for traits::Wrapper<T>)#4}::to_u64]:
     Source: 'src/traits.rs', lines 75:4-75:26 *)
-let wrapper_to_u64
-  (t : Type0) (toU64TInst : toU64_t t) (self : wrapper_t t) : result u64 =
-  toU64TInst.to_u64 self.x
+let toU64traitsWrapper_to_u64
+  (t : Type0) (toU64Inst : toU64_t t) (self : wrapper_t t) : result u64 =
+  toU64Inst.to_u64 self.x
 
-(** Trait implementation: [traits::{traits::Wrapper<T>#4}]
+(** Trait implementation: [traits::{(traits::ToU64 for traits::Wrapper<T>)#4}]
     Source: 'src/traits.rs', lines 74:0-74:35 *)
-let traits_ToU64traitsWrapperTInst (t : Type0) (toU64TInst : toU64_t t) :
-  toU64_t (wrapper_t t) = {
-  to_u64 = wrapper_to_u64 t toU64TInst;
+let toU64traitsWrapper (t : Type0) (toU64Inst : toU64_t t) : toU64_t (wrapper_t
+  t) = {
+  to_u64 = toU64traitsWrapper_to_u64 t toU64Inst;
 }
 
 (** [traits::h1]:
     Source: 'src/traits.rs', lines 80:0-80:33 *)
 let h1 (x : wrapper_t u64) : result u64 =
-  wrapper_to_u64 u64 traits_ToU64U64Inst x
+  toU64traitsWrapper_to_u64 u64 toU64U64 x
 
 (** [traits::h2]:
     Source: 'src/traits.rs', lines 84:0-84:41 *)
-let h2 (t : Type0) (toU64TInst : toU64_t t) (x : wrapper_t t) : result u64 =
-  wrapper_to_u64 t toU64TInst x
+let h2 (t : Type0) (toU64Inst : toU64_t t) (x : wrapper_t t) : result u64 =
+  toU64traitsWrapper_to_u64 t toU64Inst x
 
 (** Trait declaration: [traits::ToType]
     Source: 'src/traits.rs', lines 88:0-88:19 *)
 noeq type toType_t (self t : Type0) = { to_type : self -> result t; }
 
-(** [traits::{u64#5}::to_type]:
+(** [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
     Source: 'src/traits.rs', lines 93:4-93:28 *)
-let u64_to_type (self : u64) : result bool =
+let toTypeU64Bool_to_type (self : u64) : result bool =
   Return (self > 0)
 
-(** Trait implementation: [traits::{u64#5}]
+(** Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
     Source: 'src/traits.rs', lines 92:0-92:25 *)
-let traits_ToTypeU64BoolInst : toType_t u64 bool = { to_type = u64_to_type; }
+let toTypeU64Bool : toType_t u64 bool = { to_type = toTypeU64Bool_to_type; }
 
 (** Trait declaration: [traits::OfType]
     Source: 'src/traits.rs', lines 98:0-98:16 *)
 noeq type ofType_t (self : Type0) = {
-  of_type : (t : Type0) -> (toTypeTSelfInst : toType_t t self) -> t -> result
-    self;
+  of_type : (t : Type0) -> (toTypeInst : toType_t t self) -> t -> result self;
 }
 
 (** [traits::h3]:
     Source: 'src/traits.rs', lines 104:0-104:50 *)
 let h3
-  (t1 t2 : Type0) (ofTypeT1Inst : ofType_t t1) (toTypeT2T1Inst : toType_t t2
-  t1) (y : t2) :
+  (t1 t2 : Type0) (ofTypeInst : ofType_t t1) (toTypeInst : toType_t t2 t1)
+  (y : t2) :
   result t1
   =
-  ofTypeT1Inst.of_type t2 toTypeT2T1Inst y
+  ofTypeInst.of_type t2 toTypeInst y
 
 (** Trait declaration: [traits::OfTypeBis]
     Source: 'src/traits.rs', lines 109:0-109:36 *)
 noeq type ofTypeBis_t (self t : Type0) = {
-  toTypeTSelfInst : toType_t t self;
+  toTypeInst : toType_t t self;
   of_type : t -> result self;
 }
 
 (** [traits::h4]:
     Source: 'src/traits.rs', lines 118:0-118:57 *)
 let h4
-  (t1 t2 : Type0) (ofTypeBisT1T2Inst : ofTypeBis_t t1 t2) (toTypeT2T1Inst :
-  toType_t t2 t1) (y : t2) :
+  (t1 t2 : Type0) (ofTypeBisInst : ofTypeBis_t t1 t2) (toTypeInst : toType_t t2
+  t1) (y : t2) :
   result t1
   =
-  ofTypeBisT1T2Inst.of_type y
+  ofTypeBisInst.of_type y
 
 (** [traits::TestType]
     Source: 'src/traits.rs', lines 122:0-122:22 *)
@@ -189,51 +184,54 @@ noeq type testType_test_TestTrait_t (self : Type0) = {
   test : self -> result bool;
 }
 
-(** [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}::test]:
+(** [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}::test]:
     Source: 'src/traits.rs', lines 139:12-139:34 *)
-let testType_test_TestType1_test
+let testType_test_TestTraittraitsTestTypetestTestType1_test
   (self : testType_test_TestType1_t) : result bool =
   Return (self > 1)
 
-(** Trait implementation: [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}]
+(** Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}]
     Source: 'src/traits.rs', lines 138:8-138:36 *)
-let traits_TestType_test_TestTraittraitstraitsTestTypeTtestTestType1Inst :
+let testType_test_TestTraittraitsTestTypetestTestType1 :
   testType_test_TestTrait_t testType_test_TestType1_t = {
-  test = testType_test_TestType1_test;
+  test = testType_test_TestTraittraitsTestTypetestTestType1_test;
 }
 
 (** [traits::{traits::TestType<T>#6}::test]:
     Source: 'src/traits.rs', lines 126:4-126:36 *)
 let testType_test
-  (t : Type0) (toU64TInst : toU64_t t) (self : testType_t t) (x : t) :
+  (t : Type0) (toU64Inst : toU64_t t) (self : testType_t t) (x : t) :
   result bool
   =
-  let* x1 = toU64TInst.to_u64 x in
-  if x1 > 0 then testType_test_TestType1_test 0 else Return false
+  let* x1 = toU64Inst.to_u64 x in
+  if x1 > 0
+  then testType_test_TestTraittraitsTestTypetestTestType1_test 0
+  else Return false
 
 (** [traits::BoolWrapper]
     Source: 'src/traits.rs', lines 150:0-150:22 *)
 type boolWrapper_t = bool
 
-(** [traits::{traits::BoolWrapper#7}::to_type]:
+(** [traits::{(traits::ToType<T> for traits::BoolWrapper)#7}::to_type]:
     Source: 'src/traits.rs', lines 156:4-156:25 *)
-let boolWrapper_to_type
+let toTypetraitsBoolWrapperT_to_type
   (t : Type0) (toTypeBoolTInst : toType_t bool t) (self : boolWrapper_t) :
   result t
   =
   toTypeBoolTInst.to_type self
 
-(** Trait implementation: [traits::{traits::BoolWrapper#7}]
+(** Trait implementation: [traits::{(traits::ToType<T> for traits::BoolWrapper)#7}]
     Source: 'src/traits.rs', lines 152:0-152:33 *)
-let traits_ToTypetraitsBoolWrapperTInst (t : Type0) (toTypeBoolTInst : toType_t
-  bool t) : toType_t boolWrapper_t t = {
-  to_type = boolWrapper_to_type t toTypeBoolTInst;
+let toTypetraitsBoolWrapperT (t : Type0) (toTypeBoolTInst : toType_t bool t) :
+  toType_t boolWrapper_t t = {
+  to_type = toTypetraitsBoolWrapperT_to_type t toTypeBoolTInst;
 }
 
 (** [traits::WithConstTy::LEN2]
     Source: 'src/traits.rs', lines 164:4-164:21 *)
-let with_const_ty_len2_body : result usize = Return 32
-let with_const_ty_len2_c : usize = eval_global with_const_ty_len2_body
+let with_const_ty_len2_default_body : result usize = Return 32
+let with_const_ty_len2_default : usize =
+  eval_global with_const_ty_len2_default_body
 
 (** Trait declaration: [traits::WithConstTy]
     Source: 'src/traits.rs', lines 161:0-161:39 *)
@@ -246,40 +244,41 @@ noeq type withConstTy_t (self : Type0) (len : usize) = {
   f : tW -> array u8 len -> result tW;
 }
 
-(** [traits::{bool#8}::LEN1]
+(** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
     Source: 'src/traits.rs', lines 175:4-175:21 *)
-let bool_len1_body : result usize = Return 12
-let bool_len1_c : usize = eval_global bool_len1_body
+let with_const_ty_bool32_len1_body : result usize = Return 12
+let with_const_ty_bool32_len1 : usize =
+  eval_global with_const_ty_bool32_len1_body
 
-(** [traits::{bool#8}::f]:
+(** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::f]:
     Source: 'src/traits.rs', lines 180:4-180:39 *)
-let bool_f (i : u64) (a : array u8 32) : result u64 =
+let withConstTyBool32_f (i : u64) (a : array u8 32) : result u64 =
   Return i
 
-(** Trait implementation: [traits::{bool#8}]
+(** Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}]
     Source: 'src/traits.rs', lines 174:0-174:29 *)
-let traits_WithConstTyBool32Inst : withConstTy_t bool 32 = {
-  cLEN1 = bool_len1_c;
-  cLEN2 = with_const_ty_len2_c;
+let withConstTyBool32 : withConstTy_t bool 32 = {
+  cLEN1 = with_const_ty_bool32_len1;
+  cLEN2 = with_const_ty_len2_default;
   tV = u8;
   tW = u64;
-  tW_clause_0 = traits_ToU64U64Inst;
-  f = bool_f;
+  tW_clause_0 = toU64U64;
+  f = withConstTyBool32_f;
 }
 
 (** [traits::use_with_const_ty1]:
     Source: 'src/traits.rs', lines 183:0-183:75 *)
 let use_with_const_ty1
-  (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len) :
+  (h : Type0) (len : usize) (withConstTyInst : withConstTy_t h len) :
   result usize
   =
-  Return withConstTyHLENInst.cLEN1
+  Return withConstTyInst.cLEN1
 
 (** [traits::use_with_const_ty2]:
     Source: 'src/traits.rs', lines 187:0-187:73 *)
 let use_with_const_ty2
-  (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len)
-  (w : withConstTyHLENInst.tW) :
+  (h : Type0) (len : usize) (withConstTyInst : withConstTy_t h len)
+  (w : withConstTyInst.tW) :
   result unit
   =
   Return ()
@@ -287,11 +286,11 @@ let use_with_const_ty2
 (** [traits::use_with_const_ty3]:
     Source: 'src/traits.rs', lines 189:0-189:80 *)
 let use_with_const_ty3
-  (h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len)
-  (x : withConstTyHLENInst.tW) :
+  (h : Type0) (len : usize) (withConstTyInst : withConstTy_t h len)
+  (x : withConstTyInst.tW) :
   result u64
   =
-  withConstTyHLENInst.tW_clause_0.to_u64 x
+  withConstTyInst.tW_clause_0.to_u64 x
 
 (** [traits::test_where1]:
     Source: 'src/traits.rs', lines 193:0-193:40 *)
@@ -321,28 +320,28 @@ type parentTrait1_t (self : Type0) = unit
 (** Trait declaration: [traits::ChildTrait]
     Source: 'src/traits.rs', lines 206:0-206:49 *)
 noeq type childTrait_t (self : Type0) = {
-  parentTrait0SelfInst : parentTrait0_t self;
-  parentTrait1SelfInst : parentTrait1_t self;
+  parentTrait0Inst : parentTrait0_t self;
+  parentTrait1Inst : parentTrait1_t self;
 }
 
 (** [traits::test_child_trait1]:
     Source: 'src/traits.rs', lines 209:0-209:56 *)
 let test_child_trait1
-  (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : result string =
-  childTraitTInst.parentTrait0SelfInst.get_name x
+  (t : Type0) (childTraitInst : childTrait_t t) (x : t) : result string =
+  childTraitInst.parentTrait0Inst.get_name x
 
 (** [traits::test_child_trait2]:
     Source: 'src/traits.rs', lines 213:0-213:54 *)
 let test_child_trait2
-  (t : Type0) (childTraitTInst : childTrait_t t) (x : t) :
-  result childTraitTInst.parentTrait0SelfInst.tW
+  (t : Type0) (childTraitInst : childTrait_t t) (x : t) :
+  result childTraitInst.parentTrait0Inst.tW
   =
-  childTraitTInst.parentTrait0SelfInst.get_w x
+  childTraitInst.parentTrait0Inst.get_w x
 
 (** [traits::order1]:
     Source: 'src/traits.rs', lines 219:0-219:59 *)
 let order1
-  (t u : Type0) (parentTrait0TInst : parentTrait0_t t) (parentTrait0UInst :
+  (t u : Type0) (parentTrait0Inst : parentTrait0_t t) (parentTrait0Inst1 :
   parentTrait0_t u) :
   result unit
   =
@@ -351,17 +350,17 @@ let order1
 (** Trait declaration: [traits::ChildTrait1]
     Source: 'src/traits.rs', lines 222:0-222:35 *)
 noeq type childTrait1_t (self : Type0) = {
-  parentTrait1SelfInst : parentTrait1_t self;
+  parentTrait1Inst : parentTrait1_t self;
 }
 
-(** Trait implementation: [traits::{usize#9}]
+(** Trait implementation: [traits::{(traits::ParentTrait1 for usize)#9}]
     Source: 'src/traits.rs', lines 224:0-224:27 *)
-let traits_ParentTrait1UsizeInst : parentTrait1_t usize = ()
+let parentTrait1Usize : parentTrait1_t usize = ()
 
-(** Trait implementation: [traits::{usize#10}]
+(** Trait implementation: [traits::{(traits::ChildTrait1 for usize)#10}]
     Source: 'src/traits.rs', lines 225:0-225:26 *)
-let traits_ChildTrait1UsizeInst : childTrait1_t usize = {
-  parentTrait1SelfInst = traits_ParentTrait1UsizeInst;
+let childTrait1Usize : childTrait1_t usize = {
+  parentTrait1Inst = parentTrait1Usize;
 }
 
 (** Trait declaration: [traits::Iterator]
@@ -385,7 +384,7 @@ type fromResidual_t (self t : Type0) = unit
     Source: 'src/traits.rs', lines 246:0-246:48 *)
 noeq type try_t (self : Type0) = {
   tResidual : Type0;
-  fromResidualSelftraitsTrySelfResidualInst : fromResidual_t self tResidual;
+  fromResidualSelftraitsTryResidualInst : fromResidual_t self tResidual;
 }
 
 (** Trait declaration: [traits::WithTarget]
@@ -402,32 +401,31 @@ noeq type parentTrait2_t (self : Type0) = {
 (** Trait declaration: [traits::ChildTrait2]
     Source: 'src/traits.rs', lines 260:0-260:35 *)
 noeq type childTrait2_t (self : Type0) = {
-  parentTrait2SelfInst : parentTrait2_t self;
-  convert : parentTrait2SelfInst.tU -> result
-    parentTrait2SelfInst.tU_clause_0.tTarget;
+  parentTrait2Inst : parentTrait2_t self;
+  convert : parentTrait2Inst.tU -> result parentTrait2Inst.tU_clause_0.tTarget;
 }
 
-(** Trait implementation: [traits::{u32#11}]
+(** Trait implementation: [traits::{(traits::WithTarget for u32)#11}]
     Source: 'src/traits.rs', lines 264:0-264:23 *)
-let traits_WithTargetU32Inst : withTarget_t u32 = { tTarget = u32; }
+let withTargetU32 : withTarget_t u32 = { tTarget = u32; }
 
-(** Trait implementation: [traits::{u32#12}]
+(** Trait implementation: [traits::{(traits::ParentTrait2 for u32)#12}]
     Source: 'src/traits.rs', lines 268:0-268:25 *)
-let traits_ParentTrait2U32Inst : parentTrait2_t u32 = {
+let parentTrait2U32 : parentTrait2_t u32 = {
   tU = u32;
-  tU_clause_0 = traits_WithTargetU32Inst;
+  tU_clause_0 = withTargetU32;
 }
 
-(** [traits::{u32#13}::convert]:
+(** [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
     Source: 'src/traits.rs', lines 273:4-273:29 *)
-let u32_convert (x : u32) : result u32 =
+let childTrait2U32_convert (x : u32) : result u32 =
   Return x
 
-(** Trait implementation: [traits::{u32#13}]
+(** Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}]
     Source: 'src/traits.rs', lines 272:0-272:24 *)
-let traits_ChildTrait2U32Inst : childTrait2_t u32 = {
-  parentTrait2SelfInst = traits_ParentTrait2U32Inst;
-  convert = u32_convert;
+let childTrait2U32 : childTrait2_t u32 = {
+  parentTrait2Inst = parentTrait2U32;
+  convert = childTrait2U32_convert;
 }
 
 (** Trait declaration: [traits::CFnOnce]
@@ -440,15 +438,15 @@ noeq type cFnOnce_t (self args : Type0) = {
 (** Trait declaration: [traits::CFnMut]
     Source: 'src/traits.rs', lines 292:0-292:37 *)
 noeq type cFnMut_t (self args : Type0) = {
-  cFnOnceSelfArgsInst : cFnOnce_t self args;
-  call_mut : self -> args -> result (cFnOnceSelfArgsInst.tOutput & self);
+  cFnOnceInst : cFnOnce_t self args;
+  call_mut : self -> args -> result (cFnOnceInst.tOutput & self);
 }
 
 (** Trait declaration: [traits::CFn]
     Source: 'src/traits.rs', lines 296:0-296:33 *)
 noeq type cFn_t (self args : Type0) = {
-  cFnMutSelfArgsInst : cFnMut_t self args;
-  call : self -> args -> result cFnMutSelfArgsInst.cFnOnceSelfArgsInst.tOutput;
+  cFnMutInst : cFnMut_t self args;
+  call : self -> args -> result cFnMutInst.cFnOnceInst.tOutput;
 }
 
 (** Trait declaration: [traits::GetTrait]
@@ -459,8 +457,6 @@ noeq type getTrait_t (self : Type0) = { tW : Type0; get_w : self -> result tW;
 (** [traits::test_get_trait]:
     Source: 'src/traits.rs', lines 305:0-305:49 *)
 let test_get_trait
-  (t : Type0) (getTraitTInst : getTrait_t t) (x : t) :
-  result getTraitTInst.tW
-  =
-  getTraitTInst.get_w x
+  (t : Type0) (getTraitInst : getTrait_t t) (x : t) : result getTraitInst.tW =
+  getTraitInst.get_w x
 
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 59458393..d637ee13 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -451,8 +451,8 @@ def f3 : Result U32 :=
 
 /- [arrays::SZ]
    Source: 'src/arrays.rs', lines 286:0-286:19 -/
-def sz_body : Result Usize := Result.ret 32#usize
-def sz_c : Usize := eval_global sz_body
+def SZ_body : Result Usize := Result.ret 32#usize
+def SZ : Usize := eval_global SZ_body
 
 /- [arrays::f5]:
    Source: 'src/arrays.rs', lines 289:0-289:31 -/
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 96daa197..d6449b37 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -135,7 +135,7 @@ def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
 
 /- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
    Source: 'src/betree.rs', lines 327:4-327:44 -/
-def betree.ListTupleU64T.head_has_key
+def betree.ListPairU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
   match self with
   | betree.List.Cons hd _ => let (i, _) := hd
@@ -144,7 +144,7 @@ def betree.ListTupleU64T.head_has_key
 
 /- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
    Source: 'src/betree.rs', lines 339:4-339:73 -/
-divergent def betree.ListTupleU64T.partition_at_pivot
+divergent def betree.ListPairU64T.partition_at_pivot
   (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
   Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
   :=
@@ -155,7 +155,7 @@ divergent def betree.ListTupleU64T.partition_at_pivot
     then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl)
     else
       do
-      let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot
+      let p ← betree.ListPairU64T.partition_at_pivot T tl pivot
       let (ls0, ls1) := p
       Result.ret (betree.List.Cons (i, t) ls0, ls1)
   | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil)
@@ -227,7 +227,7 @@ divergent def betree.Node.apply_upserts
   Result (State × (U64 × (betree.List (U64 × betree.Message))))
   :=
   do
-  let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
+  let b ← betree.ListPairU64T.head_has_key betree.Message msgs key
   if b
   then
     do
@@ -387,7 +387,7 @@ def betree.Node.apply_to_internal
   do
   let (msgs1, lookup_first_message_for_key_back) ←
     betree.Node.lookup_first_message_for_key key msgs
-  let b ← betree.ListTupleU64T.head_has_key betree.Message msgs1 key
+  let b ← betree.ListPairU64T.head_has_key betree.Message msgs1 key
   if b
   then
     match new_msg with
@@ -490,7 +490,7 @@ def betree.Node.apply_to_leaf
   do
   let (bindings1, lookup_mut_in_bindings_back) ←
     betree.Node.lookup_mut_in_bindings key bindings
-  let b ← betree.ListTupleU64T.head_has_key U64 bindings1 key
+  let b ← betree.ListPairU64T.head_has_key U64 bindings1 key
   if b
   then
     do
@@ -546,7 +546,7 @@ mutual divergent def betree.Internal.flush
   :=
   do
   let ⟨ i, i1, n, n1 ⟩ := self
-  let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i1
+  let p ← betree.ListPairU64T.partition_at_pivot betree.Message content i1
   let (msgs_left, msgs_right) := p
   let len_left ← betree.List.len (U64 × betree.Message) msgs_left
   if len_left >= params.min_flush_size
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 32e0317b..7949a25c 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -7,18 +7,18 @@ namespace constants
 
 /- [constants::X0]
    Source: 'src/constants.rs', lines 5:0-5:17 -/
-def x0_body : Result U32 := Result.ret 0#u32
-def x0_c : U32 := eval_global x0_body
+def X0_body : Result U32 := Result.ret 0#u32
+def X0 : U32 := eval_global X0_body
 
 /- [constants::X1]
    Source: 'src/constants.rs', lines 7:0-7:17 -/
-def x1_body : Result U32 := Result.ret core_u32_max
-def x1_c : U32 := eval_global x1_body
+def X1_body : Result U32 := Result.ret core_u32_max
+def X1 : U32 := eval_global X1_body
 
 /- [constants::X2]
    Source: 'src/constants.rs', lines 10:0-10:17 -/
-def x2_body : Result U32 := Result.ret 3#u32
-def x2_c : U32 := eval_global x2_body
+def X2_body : Result U32 := Result.ret 3#u32
+def X2 : U32 := eval_global X2_body
 
 /- [constants::incr]:
    Source: 'src/constants.rs', lines 17:0-17:32 -/
@@ -27,8 +27,8 @@ def incr (n : U32) : Result U32 :=
 
 /- [constants::X3]
    Source: 'src/constants.rs', lines 15:0-15:17 -/
-def x3_body : Result U32 := incr 32#u32
-def x3_c : U32 := eval_global x3_body
+def X3_body : Result U32 := incr 32#u32
+def X3 : U32 := eval_global X3_body
 
 /- [constants::mk_pair0]:
    Source: 'src/constants.rs', lines 23:0-23:51 -/
@@ -48,23 +48,23 @@ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) :=
 
 /- [constants::P0]
    Source: 'src/constants.rs', lines 31:0-31:24 -/
-def p0_body : Result (U32 × U32) := mk_pair0 0#u32 1#u32
-def p0_c : (U32 × U32) := eval_global p0_body
+def P0_body : Result (U32 × U32) := mk_pair0 0#u32 1#u32
+def P0 : (U32 × U32) := eval_global P0_body
 
 /- [constants::P1]
    Source: 'src/constants.rs', lines 32:0-32:28 -/
-def p1_body : Result (Pair U32 U32) := mk_pair1 0#u32 1#u32
-def p1_c : Pair U32 U32 := eval_global p1_body
+def P1_body : Result (Pair U32 U32) := mk_pair1 0#u32 1#u32
+def P1 : Pair U32 U32 := eval_global P1_body
 
 /- [constants::P2]
    Source: 'src/constants.rs', lines 33:0-33:24 -/
-def p2_body : Result (U32 × U32) := Result.ret (0#u32, 1#u32)
-def p2_c : (U32 × U32) := eval_global p2_body
+def P2_body : Result (U32 × U32) := Result.ret (0#u32, 1#u32)
+def P2 : (U32 × U32) := eval_global P2_body
 
 /- [constants::P3]
    Source: 'src/constants.rs', lines 34:0-34:28 -/
-def p3_body : Result (Pair U32 U32) := Result.ret { x := 0#u32, y := 1#u32 }
-def p3_c : Pair U32 U32 := eval_global p3_body
+def P3_body : Result (Pair U32 U32) := Result.ret { x := 0#u32, y := 1#u32 }
+def P3 : Pair U32 U32 := eval_global P3_body
 
 /- [constants::Wrap]
    Source: 'src/constants.rs', lines 49:0-49:18 -/
@@ -78,28 +78,28 @@ def Wrap.new (T : Type) (value : T) : Result (Wrap T) :=
 
 /- [constants::Y]
    Source: 'src/constants.rs', lines 41:0-41:22 -/
-def y_body : Result (Wrap I32) := Wrap.new I32 2#i32
-def y_c : Wrap I32 := eval_global y_body
+def Y_body : Result (Wrap I32) := Wrap.new I32 2#i32
+def Y : Wrap I32 := eval_global Y_body
 
 /- [constants::unwrap_y]:
    Source: 'src/constants.rs', lines 43:0-43:30 -/
 def unwrap_y : Result I32 :=
-  Result.ret y_c.value
+  Result.ret Y.value
 
 /- [constants::YVAL]
    Source: 'src/constants.rs', lines 47:0-47:19 -/
-def yval_body : Result I32 := unwrap_y
-def yval_c : I32 := eval_global yval_body
+def YVAL_body : Result I32 := unwrap_y
+def YVAL : I32 := eval_global YVAL_body
 
 /- [constants::get_z1::Z1]
    Source: 'src/constants.rs', lines 62:4-62:17 -/
-def get_z1_z1_body : Result I32 := Result.ret 3#i32
-def get_z1_z1_c : I32 := eval_global get_z1_z1_body
+def get_z1.Z1_body : Result I32 := Result.ret 3#i32
+def get_z1.Z1 : I32 := eval_global get_z1.Z1_body
 
 /- [constants::get_z1]:
    Source: 'src/constants.rs', lines 61:0-61:28 -/
 def get_z1 : Result I32 :=
-  Result.ret get_z1_z1_c
+  Result.ret get_z1.Z1
 
 /- [constants::add]:
    Source: 'src/constants.rs', lines 66:0-66:39 -/
@@ -108,45 +108,45 @@ def add (a : I32) (b : I32) : Result I32 :=
 
 /- [constants::Q1]
    Source: 'src/constants.rs', lines 74:0-74:17 -/
-def q1_body : Result I32 := Result.ret 5#i32
-def q1_c : I32 := eval_global q1_body
+def Q1_body : Result I32 := Result.ret 5#i32
+def Q1 : I32 := eval_global Q1_body
 
 /- [constants::Q2]
    Source: 'src/constants.rs', lines 75:0-75:17 -/
-def q2_body : Result I32 := Result.ret q1_c
-def q2_c : I32 := eval_global q2_body
+def Q2_body : Result I32 := Result.ret Q1
+def Q2 : I32 := eval_global Q2_body
 
 /- [constants::Q3]
    Source: 'src/constants.rs', lines 76:0-76:17 -/
-def q3_body : Result I32 := add q2_c 3#i32
-def q3_c : I32 := eval_global q3_body
+def Q3_body : Result I32 := add Q2 3#i32
+def Q3 : I32 := eval_global Q3_body
 
 /- [constants::get_z2]:
    Source: 'src/constants.rs', lines 70:0-70:28 -/
 def get_z2 : Result I32 :=
   do
   let i ← get_z1
-  let i1 ← add i q3_c
-  add q1_c i1
+  let i1 ← add i Q3
+  add Q1 i1
 
 /- [constants::S1]
    Source: 'src/constants.rs', lines 80:0-80:18 -/
-def s1_body : Result U32 := Result.ret 6#u32
-def s1_c : U32 := eval_global s1_body
+def S1_body : Result U32 := Result.ret 6#u32
+def S1 : U32 := eval_global S1_body
 
 /- [constants::S2]
    Source: 'src/constants.rs', lines 81:0-81:18 -/
-def s2_body : Result U32 := incr s1_c
-def s2_c : U32 := eval_global s2_body
+def S2_body : Result U32 := incr S1
+def S2 : U32 := eval_global S2_body
 
 /- [constants::S3]
    Source: 'src/constants.rs', lines 82:0-82:29 -/
-def s3_body : Result (Pair U32 U32) := Result.ret p3_c
-def s3_c : Pair U32 U32 := eval_global s3_body
+def S3_body : Result (Pair U32 U32) := Result.ret P3
+def S3 : Pair U32 U32 := eval_global S3_body
 
 /- [constants::S4]
    Source: 'src/constants.rs', lines 83:0-83:29 -/
-def s4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32
-def s4_c : Pair U32 U32 := eval_global s4_body
+def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32
+def S4 : Pair U32 U32 := eval_global S4_body
 
 end constants
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 01818585..854b4853 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -126,23 +126,23 @@ divergent def i32_id (i : I32) : Result I32 :=
 structure Counter (Self : Type) where
   incr : Self → Result (Usize × Self)
 
-/- [demo::{usize}::incr]:
+/- [demo::{(demo::Counter for usize)}::incr]:
    Source: 'src/demo.rs', lines 88:4-88:31 -/
-def Usize.incr (self : Usize) : Result (Usize × Usize) :=
+def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
   do
   let self1 ← self + 1#usize
   Result.ret (self, self1)
 
-/- Trait implementation: [demo::{usize}]
+/- Trait implementation: [demo::{(demo::Counter for usize)}]
    Source: 'src/demo.rs', lines 87:0-87:22 -/
-def demo.CounterUsizeInst : Counter Usize := {
-  incr := Usize.incr
+def CounterUsize : Counter Usize := {
+  incr := CounterUsize.incr
 }
 
 /- [demo::use_counter]:
    Source: 'src/demo.rs', lines 95:0-95:59 -/
 def use_counter
-  (T : Type) (CounterTInst : Counter T) (cnt : T) : Result (Usize × T) :=
-  CounterTInst.incr cnt
+  (T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
+  CounterInst.incr cnt
 
 end demo
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index a85209ea..2112e282 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -138,13 +138,13 @@ def mix_arith_i32 (x : I32) (y : I32) (z : I32) : Result I32 :=
 
 /- [no_nested_borrows::CONST0]
    Source: 'src/no_nested_borrows.rs', lines 125:0-125:23 -/
-def const0_body : Result Usize := 1#usize + 1#usize
-def const0_c : Usize := eval_global const0_body
+def CONST0_body : Result Usize := 1#usize + 1#usize
+def CONST0 : Usize := eval_global CONST0_body
 
 /- [no_nested_borrows::CONST1]
    Source: 'src/no_nested_borrows.rs', lines 126:0-126:23 -/
-def const1_body : Result Usize := 2#usize * 2#usize
-def const1_c : Usize := eval_global const1_body
+def CONST1_body : Result Usize := 2#usize * 2#usize
+def CONST1 : Usize := eval_global CONST1_body
 
 /- [no_nested_borrows::cast_u32_to_i32]:
    Source: 'src/no_nested_borrows.rs', lines 128:0-128:37 -/
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index f83fbc2f..26dac252 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -10,15 +10,15 @@ namespace traits
 structure BoolTrait (Self : Type) where
   get_bool : Self → Result Bool
 
-/- [traits::{bool}::get_bool]:
+/- [traits::{(traits::BoolTrait for bool)}::get_bool]:
    Source: 'src/traits.rs', lines 12:4-12:30 -/
-def Bool.get_bool (self : Bool) : Result Bool :=
+def BoolTraitBool.get_bool (self : Bool) : Result Bool :=
   Result.ret self
 
-/- Trait implementation: [traits::{bool}]
+/- Trait implementation: [traits::{(traits::BoolTrait for bool)}]
    Source: 'src/traits.rs', lines 11:0-11:23 -/
-def traits.BoolTraitBoolInst : BoolTrait Bool := {
-  get_bool := Bool.get_bool
+def BoolTraitBool : BoolTrait Bool := {
+  get_bool := BoolTraitBool.get_bool
 }
 
 /- [traits::BoolTrait::ret_true]:
@@ -31,162 +31,159 @@ def BoolTrait.ret_true
    Source: 'src/traits.rs', lines 17:0-17:44 -/
 def test_bool_trait_bool (x : Bool) : Result Bool :=
   do
-  let b ← Bool.get_bool x
+  let b ← BoolTraitBool.get_bool x
   if b
-  then BoolTrait.ret_true traits.BoolTraitBoolInst x
+  then BoolTrait.ret_true BoolTraitBool x
   else Result.ret false
 
-/- [traits::{core::option::Option<T>#1}::get_bool]:
+/- [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]:
    Source: 'src/traits.rs', lines 23:4-23:30 -/
-def Option.get_bool (T : Type) (self : Option T) : Result Bool :=
+def BoolTraitOption.get_bool (T : Type) (self : Option T) : Result Bool :=
   match self with
   | none => Result.ret false
   | some _ => Result.ret true
 
-/- Trait implementation: [traits::{core::option::Option<T>#1}]
+/- Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}]
    Source: 'src/traits.rs', lines 22:0-22:31 -/
-def traits.BoolTraitcoreoptionOptionTInst (T : Type) : BoolTrait (Option T)
-  := {
-  get_bool := Option.get_bool T
+def BoolTraitOption (T : Type) : BoolTrait (Option T) := {
+  get_bool := BoolTraitOption.get_bool T
 }
 
 /- [traits::test_bool_trait_option]:
    Source: 'src/traits.rs', lines 31:0-31:54 -/
 def test_bool_trait_option (T : Type) (x : Option T) : Result Bool :=
   do
-  let b ← Option.get_bool T x
+  let b ← BoolTraitOption.get_bool T x
   if b
-  then BoolTrait.ret_true (traits.BoolTraitcoreoptionOptionTInst T) x
+  then BoolTrait.ret_true (BoolTraitOption T) x
   else Result.ret false
 
 /- [traits::test_bool_trait]:
    Source: 'src/traits.rs', lines 35:0-35:50 -/
 def test_bool_trait
-  (T : Type) (BoolTraitTInst : BoolTrait T) (x : T) : Result Bool :=
-  BoolTraitTInst.get_bool x
+  (T : Type) (BoolTraitInst : BoolTrait T) (x : T) : Result Bool :=
+  BoolTraitInst.get_bool x
 
 /- Trait declaration: [traits::ToU64]
    Source: 'src/traits.rs', lines 39:0-39:15 -/
 structure ToU64 (Self : Type) where
   to_u64 : Self → Result U64
 
-/- [traits::{u64#2}::to_u64]:
+/- [traits::{(traits::ToU64 for u64)#2}::to_u64]:
    Source: 'src/traits.rs', lines 44:4-44:26 -/
-def U64.to_u64 (self : U64) : Result U64 :=
+def ToU64U64.to_u64 (self : U64) : Result U64 :=
   Result.ret self
 
-/- Trait implementation: [traits::{u64#2}]
+/- Trait implementation: [traits::{(traits::ToU64 for u64)#2}]
    Source: 'src/traits.rs', lines 43:0-43:18 -/
-def traits.ToU64U64Inst : ToU64 U64 := {
-  to_u64 := U64.to_u64
+def ToU64U64 : ToU64 U64 := {
+  to_u64 := ToU64U64.to_u64
 }
 
-/- [traits::{(A, A)#3}::to_u64]:
+/- [traits::{(traits::ToU64 for (A, A))#3}::to_u64]:
    Source: 'src/traits.rs', lines 50:4-50:26 -/
-def Pair.to_u64
-  (A : Type) (ToU64AInst : ToU64 A) (self : (A × A)) : Result U64 :=
+def ToU64Pair.to_u64
+  (A : Type) (ToU64Inst : ToU64 A) (self : (A × A)) : Result U64 :=
   do
   let (t, t1) := self
-  let i ← ToU64AInst.to_u64 t
-  let i1 ← ToU64AInst.to_u64 t1
+  let i ← ToU64Inst.to_u64 t
+  let i1 ← ToU64Inst.to_u64 t1
   i + i1
 
-/- Trait implementation: [traits::{(A, A)#3}]
+/- Trait implementation: [traits::{(traits::ToU64 for (A, A))#3}]
    Source: 'src/traits.rs', lines 49:0-49:31 -/
-def traits.ToU64TupleAAInst (A : Type) (ToU64AInst : ToU64 A) : ToU64 (A × A)
-  := {
-  to_u64 := Pair.to_u64 A ToU64AInst
+def ToU64Pair (A : Type) (ToU64Inst : ToU64 A) : ToU64 (A × A) := {
+  to_u64 := ToU64Pair.to_u64 A ToU64Inst
 }
 
 /- [traits::f]:
    Source: 'src/traits.rs', lines 55:0-55:36 -/
-def f (T : Type) (ToU64TInst : ToU64 T) (x : (T × T)) : Result U64 :=
-  Pair.to_u64 T ToU64TInst x
+def f (T : Type) (ToU64Inst : ToU64 T) (x : (T × T)) : Result U64 :=
+  ToU64Pair.to_u64 T ToU64Inst x
 
 /- [traits::g]:
    Source: 'src/traits.rs', lines 59:0-61:18 -/
 def g
-  (T : Type) (ToU64TupleTTInst : ToU64 (T × T)) (x : (T × T)) : Result U64 :=
-  ToU64TupleTTInst.to_u64 x
+  (T : Type) (ToU64PairInst : ToU64 (T × T)) (x : (T × T)) : Result U64 :=
+  ToU64PairInst.to_u64 x
 
 /- [traits::h0]:
    Source: 'src/traits.rs', lines 66:0-66:24 -/
 def h0 (x : U64) : Result U64 :=
-  U64.to_u64 x
+  ToU64U64.to_u64 x
 
 /- [traits::Wrapper]
    Source: 'src/traits.rs', lines 70:0-70:21 -/
 structure Wrapper (T : Type) where
   x : T
 
-/- [traits::{traits::Wrapper<T>#4}::to_u64]:
+/- [traits::{(traits::ToU64 for traits::Wrapper<T>)#4}::to_u64]:
    Source: 'src/traits.rs', lines 75:4-75:26 -/
-def Wrapper.to_u64
-  (T : Type) (ToU64TInst : ToU64 T) (self : Wrapper T) : Result U64 :=
-  ToU64TInst.to_u64 self.x
+def ToU64traitsWrapper.to_u64
+  (T : Type) (ToU64Inst : ToU64 T) (self : Wrapper T) : Result U64 :=
+  ToU64Inst.to_u64 self.x
 
-/- Trait implementation: [traits::{traits::Wrapper<T>#4}]
+/- Trait implementation: [traits::{(traits::ToU64 for traits::Wrapper<T>)#4}]
    Source: 'src/traits.rs', lines 74:0-74:35 -/
-def traits.ToU64traitsWrapperTInst (T : Type) (ToU64TInst : ToU64 T) : ToU64
-  (Wrapper T) := {
-  to_u64 := Wrapper.to_u64 T ToU64TInst
+def ToU64traitsWrapper (T : Type) (ToU64Inst : ToU64 T) : ToU64 (Wrapper T)
+  := {
+  to_u64 := ToU64traitsWrapper.to_u64 T ToU64Inst
 }
 
 /- [traits::h1]:
    Source: 'src/traits.rs', lines 80:0-80:33 -/
 def h1 (x : Wrapper U64) : Result U64 :=
-  Wrapper.to_u64 U64 traits.ToU64U64Inst x
+  ToU64traitsWrapper.to_u64 U64 ToU64U64 x
 
 /- [traits::h2]:
    Source: 'src/traits.rs', lines 84:0-84:41 -/
-def h2 (T : Type) (ToU64TInst : ToU64 T) (x : Wrapper T) : Result U64 :=
-  Wrapper.to_u64 T ToU64TInst x
+def h2 (T : Type) (ToU64Inst : ToU64 T) (x : Wrapper T) : Result U64 :=
+  ToU64traitsWrapper.to_u64 T ToU64Inst x
 
 /- Trait declaration: [traits::ToType]
    Source: 'src/traits.rs', lines 88:0-88:19 -/
 structure ToType (Self T : Type) where
   to_type : Self → Result T
 
-/- [traits::{u64#5}::to_type]:
+/- [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
    Source: 'src/traits.rs', lines 93:4-93:28 -/
-def U64.to_type (self : U64) : Result Bool :=
+def ToTypeU64Bool.to_type (self : U64) : Result Bool :=
   Result.ret (self > 0#u64)
 
-/- Trait implementation: [traits::{u64#5}]
+/- Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
    Source: 'src/traits.rs', lines 92:0-92:25 -/
-def traits.ToTypeU64BoolInst : ToType U64 Bool := {
-  to_type := U64.to_type
+def ToTypeU64Bool : ToType U64 Bool := {
+  to_type := ToTypeU64Bool.to_type
 }
 
 /- Trait declaration: [traits::OfType]
    Source: 'src/traits.rs', lines 98:0-98:16 -/
 structure OfType (Self : Type) where
-  of_type : forall (T : Type) (ToTypeTSelfInst : ToType T Self), T → Result
-    Self
+  of_type : forall (T : Type) (ToTypeInst : ToType T Self), T → Result Self
 
 /- [traits::h3]:
    Source: 'src/traits.rs', lines 104:0-104:50 -/
 def h3
-  (T1 T2 : Type) (OfTypeT1Inst : OfType T1) (ToTypeT2T1Inst : ToType T2 T1)
+  (T1 T2 : Type) (OfTypeInst : OfType T1) (ToTypeInst : ToType T2 T1) 
   (y : T2) :
   Result T1
   :=
-  OfTypeT1Inst.of_type T2 ToTypeT2T1Inst y
+  OfTypeInst.of_type T2 ToTypeInst y
 
 /- Trait declaration: [traits::OfTypeBis]
    Source: 'src/traits.rs', lines 109:0-109:36 -/
 structure OfTypeBis (Self T : Type) where
-  ToTypeTSelfInst : ToType T Self
+  ToTypeInst : ToType T Self
   of_type : T → Result Self
 
 /- [traits::h4]:
    Source: 'src/traits.rs', lines 118:0-118:57 -/
 def h4
-  (T1 T2 : Type) (OfTypeBisT1T2Inst : OfTypeBis T1 T2) (ToTypeT2T1Inst : ToType
-  T2 T1) (y : T2) :
+  (T1 T2 : Type) (OfTypeBisInst : OfTypeBis T1 T2) (ToTypeInst : ToType T2 T1)
+  (y : T2) :
   Result T1
   :=
-  OfTypeBisT1T2Inst.of_type y
+  OfTypeBisInst.of_type y
 
 /- [traits::TestType]
    Source: 'src/traits.rs', lines 122:0-122:22 -/
@@ -201,54 +198,53 @@ def h4
 structure TestType.test.TestTrait (Self : Type) where
   test : Self → Result Bool
 
-/- [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}::test]:
+/- [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}::test]:
    Source: 'src/traits.rs', lines 139:12-139:34 -/
-def TestType.test.TestType1.test
+def TestType.test.TestTraittraitsTestTypetestTestType1.test
   (self : TestType.test.TestType1) : Result Bool :=
   Result.ret (self > 1#u64)
 
-/- Trait implementation: [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}]
+/- Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}]
    Source: 'src/traits.rs', lines 138:8-138:36 -/
-def traits.TestType.test.TestTraittraitstraitsTestTypeTtestTestType1Inst :
+def TestType.test.TestTraittraitsTestTypetestTestType1 :
   TestType.test.TestTrait TestType.test.TestType1 := {
-  test := TestType.test.TestType1.test
+  test := TestType.test.TestTraittraitsTestTypetestTestType1.test
 }
 
 /- [traits::{traits::TestType<T>#6}::test]:
    Source: 'src/traits.rs', lines 126:4-126:36 -/
 def TestType.test
-  (T : Type) (ToU64TInst : ToU64 T) (self : TestType T) (x : T) :
-  Result Bool
-  :=
+  (T : Type) (ToU64Inst : ToU64 T) (self : TestType T) (x : T) : Result Bool :=
   do
-  let x1 ← ToU64TInst.to_u64 x
+  let x1 ← ToU64Inst.to_u64 x
   if x1 > 0#u64
-  then TestType.test.TestType1.test 0#u64
+  then TestType.test.TestTraittraitsTestTypetestTestType1.test 0#u64
   else Result.ret false
 
 /- [traits::BoolWrapper]
    Source: 'src/traits.rs', lines 150:0-150:22 -/
 @[reducible] def BoolWrapper := Bool
 
-/- [traits::{traits::BoolWrapper#7}::to_type]:
+/- [traits::{(traits::ToType<T> for traits::BoolWrapper)#7}::to_type]:
    Source: 'src/traits.rs', lines 156:4-156:25 -/
-def BoolWrapper.to_type
+def ToTypetraitsBoolWrapperT.to_type
   (T : Type) (ToTypeBoolTInst : ToType Bool T) (self : BoolWrapper) :
   Result T
   :=
   ToTypeBoolTInst.to_type self
 
-/- Trait implementation: [traits::{traits::BoolWrapper#7}]
+/- Trait implementation: [traits::{(traits::ToType<T> for traits::BoolWrapper)#7}]
    Source: 'src/traits.rs', lines 152:0-152:33 -/
-def traits.ToTypetraitsBoolWrapperTInst (T : Type) (ToTypeBoolTInst : ToType
-  Bool T) : ToType BoolWrapper T := {
-  to_type := BoolWrapper.to_type T ToTypeBoolTInst
+def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) :
+  ToType BoolWrapper T := {
+  to_type := ToTypetraitsBoolWrapperT.to_type T ToTypeBoolTInst
 }
 
 /- [traits::WithConstTy::LEN2]
    Source: 'src/traits.rs', lines 164:4-164:21 -/
-def with_const_ty_len2_body : Result Usize := Result.ret 32#usize
-def with_const_ty_len2_c : Usize := eval_global with_const_ty_len2_body
+def WithConstTy.LEN2_default_body : Result Usize := Result.ret 32#usize
+def WithConstTy.LEN2_default : Usize :=
+  eval_global WithConstTy.LEN2_default_body
 
 /- Trait declaration: [traits::WithConstTy]
    Source: 'src/traits.rs', lines 161:0-161:39 -/
@@ -260,40 +256,40 @@ structure WithConstTy (Self : Type) (LEN : Usize) where
   W_clause_0 : ToU64 W
   f : W → Array U8 LEN → Result W
 
-/- [traits::{bool#8}::LEN1]
+/- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
    Source: 'src/traits.rs', lines 175:4-175:21 -/
-def bool_len1_body : Result Usize := Result.ret 12#usize
-def bool_len1_c : Usize := eval_global bool_len1_body
+def WithConstTyBool32.LEN1_body : Result Usize := Result.ret 12#usize
+def WithConstTyBool32.LEN1 : Usize := eval_global WithConstTyBool32.LEN1_body
 
-/- [traits::{bool#8}::f]:
+/- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::f]:
    Source: 'src/traits.rs', lines 180:4-180:39 -/
-def Bool.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
+def WithConstTyBool32.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
   Result.ret i
 
-/- Trait implementation: [traits::{bool#8}]
+/- Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}]
    Source: 'src/traits.rs', lines 174:0-174:29 -/
-def traits.WithConstTyBool32Inst : WithConstTy Bool 32#usize := {
-  LEN1 := bool_len1_c
-  LEN2 := with_const_ty_len2_c
+def WithConstTyBool32 : WithConstTy Bool 32#usize := {
+  LEN1 := WithConstTyBool32.LEN1
+  LEN2 := WithConstTy.LEN2_default
   V := U8
   W := U64
-  W_clause_0 := traits.ToU64U64Inst
-  f := Bool.f
+  W_clause_0 := ToU64U64
+  f := WithConstTyBool32.f
 }
 
 /- [traits::use_with_const_ty1]:
    Source: 'src/traits.rs', lines 183:0-183:75 -/
 def use_with_const_ty1
-  (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN) :
+  (H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN) :
   Result Usize
   :=
-  Result.ret WithConstTyHLENInst.LEN1
+  Result.ret WithConstTyInst.LEN1
 
 /- [traits::use_with_const_ty2]:
    Source: 'src/traits.rs', lines 187:0-187:73 -/
 def use_with_const_ty2
-  (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN)
-  (w : WithConstTyHLENInst.W) :
+  (H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN)
+  (w : WithConstTyInst.W) :
   Result Unit
   :=
   Result.ret ()
@@ -301,11 +297,11 @@ def use_with_const_ty2
 /- [traits::use_with_const_ty3]:
    Source: 'src/traits.rs', lines 189:0-189:80 -/
 def use_with_const_ty3
-  (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN)
-  (x : WithConstTyHLENInst.W) :
+  (H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN)
+  (x : WithConstTyInst.W) :
   Result U64
   :=
-  WithConstTyHLENInst.W_clause_0.to_u64 x
+  WithConstTyInst.W_clause_0.to_u64 x
 
 /- [traits::test_where1]:
    Source: 'src/traits.rs', lines 193:0-193:40 -/
@@ -334,27 +330,27 @@ structure ParentTrait1 (Self : Type) where
 /- Trait declaration: [traits::ChildTrait]
    Source: 'src/traits.rs', lines 206:0-206:49 -/
 structure ChildTrait (Self : Type) where
-  ParentTrait0SelfInst : ParentTrait0 Self
-  ParentTrait1SelfInst : ParentTrait1 Self
+  ParentTrait0Inst : ParentTrait0 Self
+  ParentTrait1Inst : ParentTrait1 Self
 
 /- [traits::test_child_trait1]:
    Source: 'src/traits.rs', lines 209:0-209:56 -/
 def test_child_trait1
-  (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : Result String :=
-  ChildTraitTInst.ParentTrait0SelfInst.get_name x
+  (T : Type) (ChildTraitInst : ChildTrait T) (x : T) : Result String :=
+  ChildTraitInst.ParentTrait0Inst.get_name x
 
 /- [traits::test_child_trait2]:
    Source: 'src/traits.rs', lines 213:0-213:54 -/
 def test_child_trait2
-  (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) :
-  Result ChildTraitTInst.ParentTrait0SelfInst.W
+  (T : Type) (ChildTraitInst : ChildTrait T) (x : T) :
+  Result ChildTraitInst.ParentTrait0Inst.W
   :=
-  ChildTraitTInst.ParentTrait0SelfInst.get_w x
+  ChildTraitInst.ParentTrait0Inst.get_w x
 
 /- [traits::order1]:
    Source: 'src/traits.rs', lines 219:0-219:59 -/
 def order1
-  (T U : Type) (ParentTrait0TInst : ParentTrait0 T) (ParentTrait0UInst :
+  (T U : Type) (ParentTrait0Inst : ParentTrait0 T) (ParentTrait0Inst1 :
   ParentTrait0 U) :
   Result Unit
   :=
@@ -363,17 +359,17 @@ def order1
 /- Trait declaration: [traits::ChildTrait1]
    Source: 'src/traits.rs', lines 222:0-222:35 -/
 structure ChildTrait1 (Self : Type) where
-  ParentTrait1SelfInst : ParentTrait1 Self
+  ParentTrait1Inst : ParentTrait1 Self
 
-/- Trait implementation: [traits::{usize#9}]
+/- Trait implementation: [traits::{(traits::ParentTrait1 for usize)#9}]
    Source: 'src/traits.rs', lines 224:0-224:27 -/
-def traits.ParentTrait1UsizeInst : ParentTrait1 Usize := {
+def ParentTrait1Usize : ParentTrait1 Usize := {
 }
 
-/- Trait implementation: [traits::{usize#10}]
+/- Trait implementation: [traits::{(traits::ChildTrait1 for usize)#10}]
    Source: 'src/traits.rs', lines 225:0-225:26 -/
-def traits.ChildTrait1UsizeInst : ChildTrait1 Usize := {
-  ParentTrait1SelfInst := traits.ParentTrait1UsizeInst
+def ChildTrait1Usize : ChildTrait1 Usize := {
+  ParentTrait1Inst := ParentTrait1Usize
 }
 
 /- Trait declaration: [traits::Iterator]
@@ -397,7 +393,7 @@ structure FromResidual (Self T : Type) where
    Source: 'src/traits.rs', lines 246:0-246:48 -/
 structure Try (Self : Type) where
   Residual : Type
-  FromResidualSelftraitsTrySelfResidualInst : FromResidual Self Residual
+  FromResidualSelftraitsTryResidualInst : FromResidual Self Residual
 
 /- Trait declaration: [traits::WithTarget]
    Source: 'src/traits.rs', lines 252:0-252:20 -/
@@ -413,33 +409,32 @@ structure ParentTrait2 (Self : Type) where
 /- Trait declaration: [traits::ChildTrait2]
    Source: 'src/traits.rs', lines 260:0-260:35 -/
 structure ChildTrait2 (Self : Type) where
-  ParentTrait2SelfInst : ParentTrait2 Self
-  convert : ParentTrait2SelfInst.U → Result
-    ParentTrait2SelfInst.U_clause_0.Target
+  ParentTrait2Inst : ParentTrait2 Self
+  convert : ParentTrait2Inst.U → Result ParentTrait2Inst.U_clause_0.Target
 
-/- Trait implementation: [traits::{u32#11}]
+/- Trait implementation: [traits::{(traits::WithTarget for u32)#11}]
    Source: 'src/traits.rs', lines 264:0-264:23 -/
-def traits.WithTargetU32Inst : WithTarget U32 := {
+def WithTargetU32 : WithTarget U32 := {
   Target := U32
 }
 
-/- Trait implementation: [traits::{u32#12}]
+/- Trait implementation: [traits::{(traits::ParentTrait2 for u32)#12}]
    Source: 'src/traits.rs', lines 268:0-268:25 -/
-def traits.ParentTrait2U32Inst : ParentTrait2 U32 := {
+def ParentTrait2U32 : ParentTrait2 U32 := {
   U := U32
-  U_clause_0 := traits.WithTargetU32Inst
+  U_clause_0 := WithTargetU32
 }
 
-/- [traits::{u32#13}::convert]:
+/- [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
    Source: 'src/traits.rs', lines 273:4-273:29 -/
-def U32.convert (x : U32) : Result U32 :=
+def ChildTrait2U32.convert (x : U32) : Result U32 :=
   Result.ret x
 
-/- Trait implementation: [traits::{u32#13}]
+/- Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}]
    Source: 'src/traits.rs', lines 272:0-272:24 -/
-def traits.ChildTrait2U32Inst : ChildTrait2 U32 := {
-  ParentTrait2SelfInst := traits.ParentTrait2U32Inst
-  convert := U32.convert
+def ChildTrait2U32 : ChildTrait2 U32 := {
+  ParentTrait2Inst := ParentTrait2U32
+  convert := ChildTrait2U32.convert
 }
 
 /- Trait declaration: [traits::CFnOnce]
@@ -451,14 +446,14 @@ structure CFnOnce (Self Args : Type) where
 /- Trait declaration: [traits::CFnMut]
    Source: 'src/traits.rs', lines 292:0-292:37 -/
 structure CFnMut (Self Args : Type) where
-  CFnOnceSelfArgsInst : CFnOnce Self Args
-  call_mut : Self → Args → Result (CFnOnceSelfArgsInst.Output × Self)
+  CFnOnceInst : CFnOnce Self Args
+  call_mut : Self → Args → Result (CFnOnceInst.Output × Self)
 
 /- Trait declaration: [traits::CFn]
    Source: 'src/traits.rs', lines 296:0-296:33 -/
 structure CFn (Self Args : Type) where
-  CFnMutSelfArgsInst : CFnMut Self Args
-  call : Self → Args → Result CFnMutSelfArgsInst.CFnOnceSelfArgsInst.Output
+  CFnMutInst : CFnMut Self Args
+  call : Self → Args → Result CFnMutInst.CFnOnceInst.Output
 
 /- Trait declaration: [traits::GetTrait]
    Source: 'src/traits.rs', lines 300:0-300:18 -/
@@ -469,7 +464,7 @@ structure GetTrait (Self : Type) where
 /- [traits::test_get_trait]:
    Source: 'src/traits.rs', lines 305:0-305:49 -/
 def test_get_trait
-  (T : Type) (GetTraitTInst : GetTrait T) (x : T) : Result GetTraitTInst.W :=
-  GetTraitTInst.get_w x
+  (T : Type) (GetTraitInst : GetTrait T) (x : T) : Result GetTraitInst.W :=
+  GetTraitInst.get_w x
 
 end traits