diff --git a/charon-pin b/charon-pin
index d27a488d..ee0e7820 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-cccc38353eec92c32c0f7a755fcef4ab5b1ae863
+65a82e39d87f019eb2d83b7e5a9f6ee4026db696
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index dc1aa67d..c041aa03 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -90,12 +90,11 @@ let ctx_add_norm_trait_types_from_preds (span : Meta.span) (ctx : eval_ctx)
   { ctx with norm_trait_types }
 
 (** A trait instance id refers to a local clause if it only uses the variants:
-    [Self], [Clause], [ParentClause], [ItemClause] *)
+    [Self], [Clause], [ParentClause] *)
 let rec trait_instance_id_is_local_clause (id : trait_instance_id) : bool =
   match id with
   | Self | Clause _ -> true
-  | ParentClause (id, _, _) | ItemClause (id, _, _, _) ->
-      trait_instance_id_is_local_clause id
+  | ParentClause (id, _, _) -> trait_instance_id_is_local_clause id
   | TraitImpl _
   | BuiltinOrAuto _
   | UnknownTrait _
@@ -185,7 +184,7 @@ let norm_ctx_lookup_trait_impl_ty (ctx : norm_ctx) (impl_id : TraitImplId.id)
   (* Lookup the implementation *)
   let trait_impl, subst = norm_ctx_lookup_trait_impl ctx impl_id generics in
   (* Lookup the type *)
-  let ty = snd (List.assoc type_name trait_impl.types) in
+  let ty = List.assoc type_name trait_impl.types in
   (* Substitute *)
   Subst.ty_substitute subst ty
 
@@ -201,19 +200,6 @@ let norm_ctx_lookup_trait_impl_parent_clause (ctx : norm_ctx)
   (* Substitute *)
   Subst.trait_ref_substitute subst clause
 
-let norm_ctx_lookup_trait_impl_item_clause (ctx : norm_ctx)
-    (impl_id : TraitImplId.id) (generics : generic_args) (item_name : string)
-    (clause_id : TraitClauseId.id) : trait_ref =
-  (* Lookup the implementation *)
-  let trait_impl, subst = norm_ctx_lookup_trait_impl ctx impl_id generics in
-  (* Lookup the item then its clause *)
-  let item = List.assoc item_name trait_impl.types in
-  let clause = TraitClauseId.nth (fst item) clause_id in
-  (* Sanity check: the clause necessarily refers to an impl *)
-  let _ = TypesUtils.trait_instance_id_as_trait_impl clause.trait_id in
-  (* Substitute *)
-  Subst.trait_ref_substitute subst clause
-
 (** Normalize a type by simplifying the references to trait associated types
     and choosing a representative when there are equalities between types
     enforced by local clauses (i.e., `where Trait1::T = Trait2::U`.
@@ -325,7 +311,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
       the normalization is in particular to eliminate it. Inside a [TraitRef]
       there is necessarily:
       - an id referencing a local (sub-)clause, that is an id using the variants
-        [Self], [Clause], [ItemClause] and [ParentClause] exclusively. We can't
+        [Self], [Clause], and [ParentClause] exclusively. We can't
         simplify those cases: all we can do is remove the [TraitRef] wrapper
         by leveraging the fact that the generic arguments must be empty.
       - a [TraitImpl]. Note that the [TraitImpl] is necessarily just a [TraitImpl],
@@ -377,36 +363,6 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
             ctx.span;
           ParentClause (inst_id, decl_id, clause_id)
     end
-  | ItemClause (inst_id, decl_id, item_name, clause_id) -> begin
-      let inst_id = norm_ctx_normalize_trait_instance_id ctx inst_id in
-      (* Check if the inst_id refers to a specific implementation, if yes project *)
-      match inst_id with
-      | TraitImpl (impl_id, generics) ->
-          (* We figure out the item clause by doing the following:
-             {[
-               // The implementation we are looking at
-               impl Impl1 : Trait1<R> {
-                  type S = ...
-                     with Impl2 : Trait2 ... // Instances satisfying the declared bounds
-                          ^^^^^^^^^^^^^^^^^^
-                      Lookup the clause from here
-               }
-             ]}
-          *)
-          (* Lookup the impl *)
-          let clause =
-            norm_ctx_lookup_trait_impl_item_clause ctx impl_id generics
-              item_name clause_id
-          in
-          (* Normalize the clause *)
-          norm_ctx_normalize_trait_instance_id ctx clause.trait_id
-      | _ ->
-          (* This is actually a local clause *)
-          sanity_check_opt_span __FILE__ __LINE__
-            (trait_instance_id_is_local_clause inst_id)
-            ctx.span;
-          ItemClause (inst_id, decl_id, item_name, clause_id)
-    end
   | FnPointer ty ->
       let ty = norm_ctx_normalize_ty ctx ty in
       (* TODO: we might want to return the ref to the function pointer,
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index c771fff0..84ff9e68 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2120,55 +2120,26 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
           if !record_fields_short_names then type_name
           else ctx_compute_trait_decl_name ctx trait_decl ^ type_name
         in
-        let compute_clause_name (item_name : string) (clause : trait_clause) :
-            TraitClauseId.id * string =
-          let name =
-            ctx_compute_trait_type_clause_name ctx trait_decl item_name clause
-          in
-          (* Add a prefix if necessary *)
-          let name =
-            if !record_fields_short_names then name
-            else ctx_compute_trait_decl_name ctx trait_decl ^ name
-          in
-          (clause.clause_id, name)
-        in
         List.map
-          (fun (item_name, (item_clauses, _)) ->
+          (fun (item_name, _) ->
             (* Type name *)
             let type_name = compute_type_name item_name in
-            (* Clause names *)
-            let clauses =
-              List.map (compute_clause_name item_name) item_clauses
-            in
-            (item_name, (type_name, clauses)))
+            (item_name, type_name))
           types
     | Some info ->
         let type_map = StringMap.of_list info.types in
         List.map
-          (fun (item_name, (item_clauses, _)) ->
-            let type_name, clauses_info = StringMap.find item_name type_map in
-            let clauses =
-              List.map
-                (fun (clause, clause_name) -> (clause.clause_id, clause_name))
-                (List.combine item_clauses clauses_info)
-            in
-            (item_name, (type_name, clauses)))
+          (fun (item_name, _) ->
+            let type_name = StringMap.find item_name type_map in
+            (item_name, type_name))
           types
   in
   (* Register the names *)
   List.fold_left
-    (fun ctx (item_name, (type_name, clauses)) ->
-      let ctx =
-        ctx_add trait_decl.item_meta.span
-          (TraitItemId (trait_decl.def_id, item_name))
-          type_name ctx
-      in
-      List.fold_left
-        (fun ctx (clause_id, clause_name) ->
-          ctx_add trait_decl.item_meta.span
-            (TraitItemClauseId (trait_decl.def_id, item_name, clause_id))
-            clause_name ctx)
-        ctx clauses)
+    (fun ctx (item_name, type_name) ->
+      ctx_add trait_decl.item_meta.span
+        (TraitItemId (trait_decl.def_id, item_name))
+        type_name ctx)
     ctx type_names
 
 (** Similar to {!extract_trait_decl_register_names} *)
@@ -2510,7 +2481,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
     (* The types *)
     List.iter
-      (fun (name, (clauses, _)) ->
+      (fun (name, _) ->
         (* Extract the type *)
         let item_name =
           ctx_get_trait_type decl.item_meta.span decl.def_id name ctx
@@ -2519,21 +2490,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
           F.pp_print_space fmt ();
           F.pp_print_string fmt (type_keyword decl.item_meta.span)
         in
-        extract_trait_decl_item ctx fmt item_name ty;
-        (* Extract the clauses *)
-        List.iter
-          (fun clause ->
-            let item_name =
-              ctx_get_trait_item_clause decl.item_meta.span decl.def_id name
-                clause.clause_id ctx
-            in
-            let ty () =
-              F.pp_print_space fmt ();
-              extract_trait_clause_type decl.item_meta.span ctx fmt
-                TypeDeclId.Set.empty clause
-            in
-            extract_trait_decl_item ctx fmt item_name ty)
-          clauses)
+        extract_trait_decl_item ctx fmt item_name ty)
       decl.types;
 
     (* The parent clauses - note that the parent clauses may refer to the types
@@ -2598,21 +2555,12 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
       decl.consts;
     (* The types *)
     List.iter
-      (fun (name, (clauses, _)) ->
+      (fun (name, _) ->
         (* The type *)
         let item_name =
           ctx_get_trait_type decl.item_meta.span decl.def_id name ctx
         in
-        extract_coq_arguments_instruction ctx fmt item_name num_params;
-        (* The type clauses *)
-        List.iter
-          (fun clause ->
-            let item_name =
-              ctx_get_trait_item_clause decl.item_meta.span decl.def_id name
-                clause.clause_id ctx
-            in
-            extract_coq_arguments_instruction ctx fmt item_name num_params)
-          clauses)
+        extract_coq_arguments_instruction ctx fmt item_name num_params)
       decl.types;
     (* The parent clauses *)
     List.iter
@@ -2859,7 +2807,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
 
     (* The types *)
     List.iter
-      (fun (name, (trait_refs, ty)) ->
+      (fun (name, ty) ->
         (* Extract the type *)
         let item_name =
           ctx_get_trait_type impl.item_meta.span trait_decl_id name ctx
@@ -2868,21 +2816,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
           F.pp_print_space fmt ();
           extract_ty impl.item_meta.span ctx fmt TypeDeclId.Set.empty false ty
         in
-        extract_trait_impl_item ctx fmt item_name ty;
-        (* Extract the clauses *)
-        TraitClauseId.iteri
-          (fun clause_id trait_ref ->
-            let item_name =
-              ctx_get_trait_item_clause impl.item_meta.span trait_decl_id name
-                clause_id ctx
-            in
-            let ty () =
-              F.pp_print_space fmt ();
-              extract_trait_ref impl.item_meta.span ctx fmt TypeDeclId.Set.empty
-                false trait_ref
-            in
-            extract_trait_impl_item ctx fmt item_name ty)
-          trait_refs)
+        extract_trait_impl_item ctx fmt item_name ty)
       impl.types;
 
     (* The parent clauses *)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index c3f6fa59..f93a6a4a 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -172,7 +172,6 @@ type id =
   | TraitItemId of TraitDeclId.id * string
       (** A trait associated item which is not a method *)
   | TraitParentClauseId of TraitDeclId.id * TraitClauseId.id
-  | TraitItemClauseId of TraitDeclId.id * string * TraitClauseId.id
   | TraitSelfClauseId
       (** Specifically for the clause: [Self : Trait].
 
@@ -396,11 +395,8 @@ let strict_collisions (id : id) : bool =
 (** We might not check for collisions for some specific ids (ex.: field names) *)
 let allow_collisions (id : id) : bool =
   match id with
-  | FieldId _
-  | TraitItemClauseId _
-  | TraitParentClauseId _
-  | TraitItemId _
-  | TraitMethodId _ -> !Config.record_fields_short_names
+  | FieldId _ | TraitParentClauseId _ | TraitItemId _ | TraitMethodId _ ->
+      !Config.record_fields_short_names
   | FunId (Pure _ | FromLlbc (FunId (FAssumed _), _)) ->
       (* We map several assumed functions to the same id *)
       true
@@ -675,10 +671,6 @@ let id_to_string (span : Meta.span option) (id : id) (ctx : extraction_ctx) :
   | TraitParentClauseId (id, clause_id) ->
       "trait_parent_clause_id: " ^ trait_decl_id_to_string id ^ ", clause_id: "
       ^ TraitClauseId.to_string clause_id
-  | TraitItemClauseId (id, item_name, clause_id) ->
-      "trait_item_clause_id: " ^ trait_decl_id_to_string id ^ ", item name: "
-      ^ item_name ^ ", clause_id: "
-      ^ TraitClauseId.to_string clause_id
   | TraitItemId (id, name) ->
       "trait_item_id: " ^ trait_decl_id_to_string id ^ ", type name: " ^ name
   | TraitMethodId (trait_decl_id, fun_name) ->
@@ -759,10 +751,6 @@ let ctx_get_trait_parent_clause (span : Meta.span) (id : trait_decl_id)
     (clause : trait_clause_id) (ctx : extraction_ctx) : string =
   ctx_get (Some span) (TraitParentClauseId (id, clause)) ctx
 
-let ctx_get_trait_item_clause (span : Meta.span) (id : trait_decl_id)
-    (item : string) (clause : trait_clause_id) (ctx : extraction_ctx) : string =
-  ctx_get (Some span) (TraitItemClauseId (id, item, clause)) ctx
-
 let ctx_get_var (span : Meta.span) (id : VarId.id) (ctx : extraction_ctx) :
     string =
   ctx_get (Some span) (VarId id) ctx
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 71565399..c8d9af2e 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -550,11 +550,10 @@ type builtin_trait_decl_info = {
   constructor : string;
   parent_clauses : string list;
   consts : (string * string) list;
-  types : (string * (string * string list)) list;
+  types : (string * string) list;
       (** Every type has:
           - a Rust name
-          - an extraction name
-          - a list of clauses *)
+          - an extraction name *)
   methods : (string * builtin_fun_info) list;
 }
 [@@deriving show]
@@ -586,8 +585,7 @@ let builtin_trait_decls_info () =
           | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name
           | Lean -> type_name
         in
-        let clauses = [] in
-        (item_name, (type_name, clauses))
+        (item_name, type_name)
       in
       List.map mk_type types
     in
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index aac39924..12b0deba 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -720,13 +720,6 @@ and extract_trait_instance_id (span : Meta.span) (ctx : extraction_ctx)
       let name = ctx_get_trait_parent_clause span decl_id clause_id ctx in
       extract_trait_instance_id_with_dot span ctx fmt no_params_tys true inst_id;
       F.pp_print_string fmt (add_brackets name)
-  | ItemClause (inst_id, decl_id, item_name, clause_id) ->
-      (* Use the trait decl id to lookup the name *)
-      let name =
-        ctx_get_trait_item_clause span decl_id item_name clause_id ctx
-      in
-      extract_trait_instance_id_with_dot span ctx fmt no_params_tys true inst_id;
-      F.pp_print_string fmt (add_brackets name)
   | UnknownTrait _ ->
       (* This is an error case *)
       craise __FILE__ __LINE__ span "Unexpected"
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 3d679622..bf96aa38 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -198,10 +198,6 @@ and trait_instance_id_to_string (env : fmt_env) (id : trait_instance_id) :
       let inst_id = trait_instance_id_to_string env inst_id in
       let clause_id = trait_clause_id_to_string env clause_id in
       "parent(" ^ inst_id ^ ")::" ^ clause_id
-  | ItemClause (inst_id, _decl_id, item_name, clause_id) ->
-      let inst_id = trait_instance_id_to_string env inst_id in
-      let clause_id = trait_clause_id_to_string env clause_id in
-      "(" ^ inst_id ^ ")::" ^ item_name ^ "::[" ^ clause_id ^ "]"
   | UnknownTrait msg -> "UNKNOWN(" ^ msg ^ ")"
 
 let trait_clause_to_string (env : fmt_env) (clause : trait_clause) : string =
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 0575dce1..e54927f6 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -309,8 +309,6 @@ and trait_instance_id =
   | TraitImpl of trait_impl_id * generic_args
   | Clause of trait_clause_id
   | ParentClause of trait_instance_id * trait_decl_id * trait_clause_id
-  | ItemClause of
-      trait_instance_id * trait_decl_id * trait_item_name * trait_clause_id
   | UnknownTrait of string
 [@@deriving
   show,
@@ -1147,7 +1145,7 @@ type trait_decl = {
   parent_clauses : trait_clause list;
   llbc_parent_clauses : Types.trait_clause list;
   consts : (trait_item_name * (ty * global_decl_id option)) list;
-  types : (trait_item_name * (trait_clause list * ty option)) list;
+  types : (trait_item_name * ty option) list;
   required_methods : (trait_item_name * fun_decl_id) list;
   provided_methods : (trait_item_name * fun_decl_id option) list;
 }
@@ -1170,7 +1168,7 @@ type trait_impl = {
   preds : predicates;
   parent_trait_refs : trait_ref list;
   consts : (trait_item_name * (ty * global_decl_id)) list;
-  types : (trait_item_name * (trait_ref list * ty)) list;
+  types : (trait_item_name * ty) list;
   required_methods : (trait_item_name * fun_decl_id) list;
   provided_methods : (trait_item_name * fun_decl_id) list;
 }
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 29af3efc..bb641912 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -451,9 +451,6 @@ and translate_trait_instance_id (span : Meta.span) (translate_ty : T.ty -> ty)
   | ParentClause (inst_id, decl_id, clause_id) ->
       let inst_id = translate_trait_instance_id inst_id in
       ParentClause (inst_id, decl_id, clause_id)
-  | ItemClause (inst_id, decl_id, item_name, clause_id) ->
-      let inst_id = translate_trait_instance_id inst_id in
-      ItemClause (inst_id, decl_id, item_name, clause_id)
   | FnPointer _ | Closure _ ->
       craise __FILE__ __LINE__ span "Closures are not supported yet"
   | Dyn _ ->
@@ -3981,14 +3978,10 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
   in
   let types =
     List.map
-      (fun (name, (trait_clauses, ty)) ->
+      (fun (name, ty) ->
         ( name,
-          ( List.map
-              (translate_trait_clause trait_decl.item_meta.span)
-              trait_clauses,
-            Option.map
-              (translate_fwd_ty trait_decl.item_meta.span type_infos)
-              ty ) ))
+          Option.map (translate_fwd_ty trait_decl.item_meta.span type_infos) ty
+        ))
       types
   in
   {
@@ -4046,12 +4039,8 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
   in
   let types =
     List.map
-      (fun (name, (trait_refs, ty)) ->
-        ( name,
-          ( List.map
-              (translate_fwd_trait_ref trait_impl.item_meta.span type_infos)
-              trait_refs,
-            translate_fwd_ty trait_impl.item_meta.span type_infos ty ) ))
+      (fun (name, ty) ->
+        (name, translate_fwd_ty trait_impl.item_meta.span type_infos ty))
       types
   in
   {
diff --git a/flake.lock b/flake.lock
index 4f5b189a..2bd891f8 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1720447930,
-        "narHash": "sha256-U5Tz1Pz7pmeFTrheZS90K3iRmfnlHvi47UexXflwV2o=",
+        "lastModified": 1721144517,
+        "narHash": "sha256-O1OiaNTzJ8tsqYbKz4JieP7QAJtENXazKzL7SJZVQD0=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "cccc38353eec92c32c0f7a755fcef4ab5b1ae863",
+        "rev": "65a82e39d87f019eb2d83b7e5a9f6ee4026db696",
         "type": "github"
       },
       "original": {
@@ -272,11 +272,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1720405186,
-        "narHash": "sha256-7D57KwmTIbsopE/1g8hFeIbVoeJGgU3wfuGYvTlNQG4=",
+        "lastModified": 1721096425,
+        "narHash": "sha256-9/58mnoDCyBHsJZwTg3MfgX3kgVqP/SzGMy0WnnWII8=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "f0ca58b37ff4179ce4587589c32205764d9b4a4f",
+        "rev": "1c95d396d7395829b5c06bea84fb1dd23169ca42",
         "type": "github"
       },
       "original": {
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 29063c13..bbb5aa14 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -298,7 +298,8 @@ Record WithConstTy_t (Self : Type) (LEN : usize) := mkWithConstTy_t {
   WithConstTy_tWithConstTy_t_LEN2 : usize;
   WithConstTy_tWithConstTy_t_V : Type;
   WithConstTy_tWithConstTy_t_W : Type;
-  WithConstTy_tWithConstTy_t_W_clause_0 : ToU64_t WithConstTy_tWithConstTy_t_W;
+  WithConstTy_tWithConstTy_t_ToU64traitsWithConstTyWInst : ToU64_t
+    WithConstTy_tWithConstTy_t_W;
   WithConstTy_t_f : WithConstTy_tWithConstTy_t_W -> array u8 LEN -> result
     WithConstTy_tWithConstTy_t_W;
 }.
@@ -308,7 +309,7 @@ Arguments WithConstTy_tWithConstTy_t_LEN1 { _ _ }.
 Arguments WithConstTy_tWithConstTy_t_LEN2 { _ _ }.
 Arguments WithConstTy_tWithConstTy_t_V { _ _ }.
 Arguments WithConstTy_tWithConstTy_t_W { _ _ }.
-Arguments WithConstTy_tWithConstTy_t_W_clause_0 { _ _ }.
+Arguments WithConstTy_tWithConstTy_t_ToU64traitsWithConstTyWInst { _ _ }.
 Arguments WithConstTy_t_f { _ _ }.
 
 (** [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
@@ -332,7 +333,7 @@ Definition WithConstTyBool32 : WithConstTy_t bool 32%usize := {|
   WithConstTy_tWithConstTy_t_LEN2 := with_const_ty_len2_default bool 32%usize;
   WithConstTy_tWithConstTy_t_V := u8;
   WithConstTy_tWithConstTy_t_W := u64;
-  WithConstTy_tWithConstTy_t_W_clause_0 := ToU64U64;
+  WithConstTy_tWithConstTy_t_ToU64traitsWithConstTyWInst := ToU64U64;
   WithConstTy_t_f := withConstTyBool32_f;
 |}.
 
@@ -362,7 +363,8 @@ Definition use_with_const_ty3
   (x : withConstTyInst.(WithConstTy_tWithConstTy_t_W)) :
   result u64
   :=
-  withConstTyInst.(WithConstTy_tWithConstTy_t_W_clause_0).(ToU64_t_to_u64) x
+  withConstTyInst.(WithConstTy_tWithConstTy_t_ToU64traitsWithConstTyWInst).(ToU64_t_to_u64)
+    x
 .
 
 (** [traits::test_where1]:
@@ -471,8 +473,8 @@ Arguments Iterator_tIterator_t_Item { _ }.
 Record IntoIterator_t (Self : Type) := mkIntoIterator_t {
   IntoIterator_tIntoIterator_t_Item : Type;
   IntoIterator_tIntoIterator_t_IntoIter : Type;
-  IntoIterator_tIntoIterator_t_IntoIter_clause_0 : Iterator_t
-    IntoIterator_tIntoIterator_t_IntoIter;
+  IntoIterator_tIntoIterator_t_IteratortraitsIntoIteratorIntoIterInst :
+    Iterator_t IntoIterator_tIntoIterator_t_IntoIter;
   IntoIterator_t_into_iter : Self -> result
     IntoIterator_tIntoIterator_t_IntoIter;
 }.
@@ -480,7 +482,8 @@ Record IntoIterator_t (Self : Type) := mkIntoIterator_t {
 Arguments mkIntoIterator_t { _ }.
 Arguments IntoIterator_tIntoIterator_t_Item { _ }.
 Arguments IntoIterator_tIntoIterator_t_IntoIter { _ }.
-Arguments IntoIterator_tIntoIterator_t_IntoIter_clause_0 { _ }.
+Arguments IntoIterator_tIntoIterator_t_IteratortraitsIntoIteratorIntoIterInst {
+  _ }.
 Arguments IntoIterator_t_into_iter { _ }.
 
 (** Trait declaration: [traits::FromResidual]
@@ -514,13 +517,13 @@ Arguments WithTarget_tWithTarget_t_Target { _ }.
     Source: 'tests/src/traits.rs', lines 257:0-257:22 *)
 Record ParentTrait2_t (Self : Type) := mkParentTrait2_t {
   ParentTrait2_tParentTrait2_t_U : Type;
-  ParentTrait2_tParentTrait2_t_U_clause_0 : WithTarget_t
+  ParentTrait2_tParentTrait2_t_WithTargettraitsParentTrait2UInst : WithTarget_t
     ParentTrait2_tParentTrait2_t_U;
 }.
 
 Arguments mkParentTrait2_t { _ }.
 Arguments ParentTrait2_tParentTrait2_t_U { _ }.
-Arguments ParentTrait2_tParentTrait2_t_U_clause_0 { _ }.
+Arguments ParentTrait2_tParentTrait2_t_WithTargettraitsParentTrait2UInst { _ }.
 
 (** Trait declaration: [traits::ChildTrait2]
     Source: 'tests/src/traits.rs', lines 261:0-261:35 *)
@@ -529,7 +532,7 @@ Record ChildTrait2_t (Self : Type) := mkChildTrait2_t {
   ChildTrait2_t_convert :
     (ChildTrait2_tChildTrait2_t_ParentTrait2Inst).(ParentTrait2_tParentTrait2_t_U)
     -> result
-    (ChildTrait2_tChildTrait2_t_ParentTrait2Inst).(ParentTrait2_tParentTrait2_t_U_clause_0).(WithTarget_tWithTarget_t_Target);
+    (ChildTrait2_tChildTrait2_t_ParentTrait2Inst).(ParentTrait2_tParentTrait2_t_WithTargettraitsParentTrait2UInst).(WithTarget_tWithTarget_t_Target);
 }.
 
 Arguments mkChildTrait2_t { _ }.
@@ -546,7 +549,8 @@ Definition WithTargetU32 : WithTarget_t u32 := {|
     Source: 'tests/src/traits.rs', lines 269:0-269:25 *)
 Definition ParentTrait2U32 : ParentTrait2_t u32 := {|
   ParentTrait2_tParentTrait2_t_U := u32;
-  ParentTrait2_tParentTrait2_t_U_clause_0 := WithTargetU32;
+  ParentTrait2_tParentTrait2_t_WithTargettraitsParentTrait2UInst :=
+    WithTargetU32;
 |}.
 
 (** [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 3de74912..6aae7917 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -242,7 +242,7 @@ noeq type withConstTy_t (self : Type0) (len : usize) = {
   cLEN2 : usize;
   tV : Type0;
   tW : Type0;
-  tW_clause_0 : toU64_t tW;
+  toU64traitsWithConstTyWInst : toU64_t tW;
   f : tW -> array u8 len -> result tW;
 }
 
@@ -264,7 +264,7 @@ let withConstTyBool32 : withConstTy_t bool 32 = {
   cLEN2 = with_const_ty_len2_default bool 32;
   tV = u8;
   tW = u64;
-  tW_clause_0 = toU64U64;
+  toU64traitsWithConstTyWInst = toU64U64;
   f = withConstTyBool32_f;
 }
 
@@ -292,7 +292,7 @@ let use_with_const_ty3
   (x : withConstTyInst.tW) :
   result u64
   =
-  withConstTyInst.tW_clause_0.to_u64 x
+  withConstTyInst.toU64traitsWithConstTyWInst.to_u64 x
 
 (** [traits::test_where1]:
     Source: 'tests/src/traits.rs', lines 194:0-194:40 *)
@@ -374,7 +374,7 @@ noeq type iterator_t (self : Type0) = { tItem : Type0; }
 noeq type intoIterator_t (self : Type0) = {
   tItem : Type0;
   tIntoIter : Type0;
-  tIntoIter_clause_0 : iterator_t tIntoIter;
+  iteratortraitsIntoIteratorIntoIterInst : iterator_t tIntoIter;
   into_iter : self -> result tIntoIter;
 }
 
@@ -397,14 +397,15 @@ noeq type withTarget_t (self : Type0) = { tTarget : Type0; }
     Source: 'tests/src/traits.rs', lines 257:0-257:22 *)
 noeq type parentTrait2_t (self : Type0) = {
   tU : Type0;
-  tU_clause_0 : withTarget_t tU;
+  withTargettraitsParentTrait2UInst : withTarget_t tU;
 }
 
 (** Trait declaration: [traits::ChildTrait2]
     Source: 'tests/src/traits.rs', lines 261:0-261:35 *)
 noeq type childTrait2_t (self : Type0) = {
   parentTrait2Inst : parentTrait2_t self;
-  convert : parentTrait2Inst.tU -> result parentTrait2Inst.tU_clause_0.tTarget;
+  convert : parentTrait2Inst.tU -> result
+    parentTrait2Inst.withTargettraitsParentTrait2UInst.tTarget;
 }
 
 (** Trait implementation: [traits::{(traits::WithTarget for u32)#11}]
@@ -415,7 +416,7 @@ let withTargetU32 : withTarget_t u32 = { tTarget = u32; }
     Source: 'tests/src/traits.rs', lines 269:0-269:25 *)
 let parentTrait2U32 : parentTrait2_t u32 = {
   tU = u32;
-  tU_clause_0 = withTargetU32;
+  withTargettraitsParentTrait2UInst = withTargetU32;
 }
 
 (** [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index b220042f..61b7c5c7 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -257,7 +257,7 @@ structure WithConstTy (Self : Type) (LEN : Usize) where
   LEN2 : Usize
   V : Type
   W : Type
-  W_clause_0 : ToU64 W
+  ToU64traitsWithConstTyWInst : ToU64 W
   f : W → Array U8 LEN → Result W
 
 /- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
@@ -277,7 +277,7 @@ def WithConstTyBool32 : WithConstTy Bool 32#usize := {
   LEN2 := WithConstTy.LEN2_default Bool 32#usize
   V := U8
   W := U64
-  W_clause_0 := ToU64U64
+  ToU64traitsWithConstTyWInst := ToU64U64
   f := WithConstTyBool32.f
 }
 
@@ -305,7 +305,7 @@ def use_with_const_ty3
   (x : WithConstTyInst.W) :
   Result U64
   :=
-  WithConstTyInst.W_clause_0.to_u64 x
+  WithConstTyInst.ToU64traitsWithConstTyWInst.to_u64 x
 
 /- [traits::test_where1]:
    Source: 'tests/src/traits.rs', lines 194:0-194:40 -/
@@ -386,7 +386,7 @@ structure Iterator (Self : Type) where
 structure IntoIterator (Self : Type) where
   Item : Type
   IntoIter : Type
-  IntoIter_clause_0 : Iterator IntoIter
+  IteratortraitsIntoIteratorIntoIterInst : Iterator IntoIter
   into_iter : Self → Result IntoIter
 
 /- Trait declaration: [traits::FromResidual]
@@ -408,13 +408,14 @@ structure WithTarget (Self : Type) where
    Source: 'tests/src/traits.rs', lines 257:0-257:22 -/
 structure ParentTrait2 (Self : Type) where
   U : Type
-  U_clause_0 : WithTarget U
+  WithTargettraitsParentTrait2UInst : WithTarget U
 
 /- Trait declaration: [traits::ChildTrait2]
    Source: 'tests/src/traits.rs', lines 261:0-261:35 -/
 structure ChildTrait2 (Self : Type) where
   ParentTrait2Inst : ParentTrait2 Self
-  convert : ParentTrait2Inst.U → Result ParentTrait2Inst.U_clause_0.Target
+  convert : ParentTrait2Inst.U → Result
+    ParentTrait2Inst.WithTargettraitsParentTrait2UInst.Target
 
 /- Trait implementation: [traits::{(traits::WithTarget for u32)#11}]
    Source: 'tests/src/traits.rs', lines 265:0-265:23 -/
@@ -426,7 +427,7 @@ def WithTargetU32 : WithTarget U32 := {
    Source: 'tests/src/traits.rs', lines 269:0-269:25 -/
 def ParentTrait2U32 : ParentTrait2 U32 := {
   U := U32
-  U_clause_0 := WithTargetU32
+  WithTargettraitsParentTrait2UInst := WithTargetU32
 }
 
 /- [traits::{(traits::ChildTrait2 for u32)#13}::convert]: