diff --git a/charon-pin b/charon-pin
index a7235a281..1de0f0abc 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.
-03f6136bea6b2b0f1d6701b0569cc49611d9de4a
+17609ac76fb83a5c3cb944fa3ff6121c085c3071
diff --git a/flake.lock b/flake.lock
index 6b31bd098..6811fc510 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1750428484,
-        "narHash": "sha256-O4A8IQN8mJCfGFVXa3ULyLNPZIdEeCTV4gha334s2mU=",
+        "lastModified": 1751377419,
+        "narHash": "sha256-Sm5XQdcIoIDEIeb6ClAmIsPf01m7j5nAcvl03IbxbD8=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "03f6136bea6b2b0f1d6701b0569cc49611d9de4a",
+        "rev": "17609ac76fb83a5c3cb944fa3ff6121c085c3071",
         "type": "github"
       },
       "original": {
@@ -177,17 +177,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1748399823,
-        "narHash": "sha256-kahD8D5hOXOsGbNdoLLnqCL887cjHkx98Izc37nDjlA=",
+        "lastModified": 1751338093,
+        "narHash": "sha256-/yd9nPcTfUZPFtwjRbdB5yGLdt3LTPqz6Ja63Joiahs=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "d68a69dc71bc19beb3479800392112c2f6218159",
+        "rev": "6cfb7821732dac2d3e2dea857a5613d3b856c20c",
         "type": "github"
       },
       "original": {
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "d68a69dc71bc19beb3479800392112c2f6218159",
+        "rev": "6cfb7821732dac2d3e2dea857a5613d3b856c20c",
         "type": "github"
       }
     },
diff --git a/src/pure/Pure.ml b/src/pure/Pure.ml
index 77d2a3812..4823ce874 100644
--- a/src/pure/Pure.ml
+++ b/src/pure/Pure.ml
@@ -1380,7 +1380,7 @@ type fun_body = {
 }
 [@@deriving show]
 
-type item_kind = A.item_kind [@@deriving show]
+type item_kind = T.item_kind [@@deriving show]
 
 (** Attributes to add to the generated code *)
 type backend_attributes = {
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 1fa990b48..a3e9e6e16 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -9,12 +9,12 @@ Local Open Scope Primitives_scope.
 Module Demo.
 
 (** [core::num::{u32}::wrapping_add]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2025:8-2025:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2037:8-2037:58
     Name pattern: [core::num::{u32}::wrapping_add] *)
 Axiom core_num_U32_wrapping_add : u32 -> u32 -> result u32.
 
 (** [core::num::{u32}::wrapping_sub]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2066:8-2066:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2074:8-2074:58
     Name pattern: [core::num::{u32}::wrapping_sub] *)
 Axiom core_num_U32_wrapping_sub : u32 -> u32 -> result u32.
 
diff --git a/tests/coq/misc/DefaultedMethod.v b/tests/coq/misc/DefaultedMethod.v
index f3f5b6de4..cd06c3c67 100644
--- a/tests/coq/misc/DefaultedMethod.v
+++ b/tests/coq/misc/DefaultedMethod.v
@@ -9,7 +9,7 @@ Local Open Scope Primitives_scope.
 Module DefaultedMethod.
 
 (** Trait declaration: [core::cmp::PartialEq]
-    Source: '/rustc/library/core/src/cmp.rs', lines 249:0-249:39
+    Source: '/rustc/library/core/src/cmp.rs', lines 252:0-252:59
     Name pattern: [core::cmp::PartialEq] *)
 Record core_cmp_PartialEq_t (Self : Type) (Rhs : Type)
   := mkcore_cmp_PartialEq_t {
@@ -20,7 +20,7 @@ Arguments mkcore_cmp_PartialEq_t { _ } { _ }.
 Arguments core_cmp_PartialEq_t_eq { _ } { _ } _.
 
 (** Trait declaration: [core::cmp::Eq]
-    Source: '/rustc/library/core/src/cmp.rs', lines 335:0-335:29
+    Source: '/rustc/library/core/src/cmp.rs', lines 338:0-338:44
     Name pattern: [core::cmp::Eq] *)
 Record core_cmp_Eq_t (Self : Type) := mkcore_cmp_Eq_t {
   core_cmp_Eq_tcore_cmp_Eq_t_PartialEqInst : core_cmp_PartialEq_t Self Self;
@@ -30,7 +30,7 @@ Arguments mkcore_cmp_Eq_t { _ }.
 Arguments core_cmp_Eq_tcore_cmp_Eq_t_PartialEqInst { _ } _.
 
 (** [core::cmp::Ordering]
-    Source: '/rustc/library/core/src/cmp.rs', lines 388:0-388:17
+    Source: '/rustc/library/core/src/cmp.rs', lines 391:0-391:17
     Name pattern: [core::cmp::Ordering] *)
 Inductive core_cmp_Ordering_t :=
 | Core_cmp_Ordering_Less : core_cmp_Ordering_t
@@ -39,7 +39,7 @@ Inductive core_cmp_Ordering_t :=
 .
 
 (** Trait declaration: [core::cmp::PartialOrd]
-    Source: '/rustc/library/core/src/cmp.rs', lines 1340:0-1340:56
+    Source: '/rustc/library/core/src/cmp.rs', lines 1344:0-1344:77
     Name pattern: [core::cmp::PartialOrd] *)
 Record core_cmp_PartialOrd_t (Self : Type) (Rhs : Type)
   := mkcore_cmp_PartialOrd_t {
@@ -55,7 +55,7 @@ Arguments core_cmp_PartialOrd_tcore_cmp_PartialOrd_t_PartialEqInst { _ } { _ }
 Arguments core_cmp_PartialOrd_t_partial_cmp { _ } { _ } _.
 
 (** Trait declaration: [core::cmp::Ord]
-    Source: '/rustc/library/core/src/cmp.rs', lines 957:0-957:36
+    Source: '/rustc/library/core/src/cmp.rs', lines 960:0-960:51
     Name pattern: [core::cmp::Ord] *)
 Record core_cmp_Ord_t (Self : Type) := mkcore_cmp_Ord_t {
   core_cmp_Ord_tcore_cmp_Ord_t_EqInst : core_cmp_Eq_t Self;
@@ -72,7 +72,7 @@ Arguments core_cmp_Ord_t_cmp { _ } _.
 Arguments core_cmp_Ord_t_min { _ } _.
 
 (** [core::cmp::Ord::min]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1048:4-1050:20
+    Source: '/rustc/library/core/src/cmp.rs', lines 1051:4-1053:20
     Name pattern: [core::cmp::Ord::min] *)
 Axiom core_cmp_Ord_min_default :
   forall{Self : Type} (ordInst : core_cmp_Ord_t Self),
@@ -80,24 +80,24 @@ Axiom core_cmp_Ord_min_default :
 .
 
 (** [core::cmp::impls::{core::cmp::PartialEq<i32> for i32}::eq]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1813:16-1813:50
+    Source: '/rustc/library/core/src/cmp.rs', lines 1819:16-1819:50
     Name pattern: [core::cmp::impls::{core::cmp::PartialEq<i32, i32>}::eq] *)
 Axiom core_cmp_impls_PartialEqI32I32_eq : i32 -> i32 -> result bool.
 
 (** [core::cmp::impls::{core::cmp::PartialOrd<i32> for i32}::partial_cmp]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1928:16-1928:71
+    Source: '/rustc/library/core/src/cmp.rs', lines 1934:16-1934:71
     Name pattern: [core::cmp::impls::{core::cmp::PartialOrd<i32, i32>}::partial_cmp] *)
 Axiom core_cmp_impls_PartialOrdI32I32_partial_cmp
   : i32 -> i32 -> result (option core_cmp_Ordering_t)
 .
 
 (** [core::cmp::impls::{core::cmp::Ord for i32}::cmp]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1938:16-1938:55
+    Source: '/rustc/library/core/src/cmp.rs', lines 1944:16-1944:55
     Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::cmp] *)
 Axiom core_cmp_impls_OrdI32_cmp : i32 -> i32 -> result core_cmp_Ordering_t.
 
 (** [core::cmp::impls::{core::cmp::Ord for i32}::min]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1936:12-1936:27
+    Source: '/rustc/library/core/src/cmp.rs', lines 1942:12-1942:27
     Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min] *)
 Axiom core_cmp_impls_OrdI32_min : i32 -> i32 -> result i32.
 
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index f98738ab4..988579559 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -12,7 +12,7 @@ Include External_Types.
 Module External_FunsExternal_Template.
 
 (** [core::cell::{core::cell::Cell<T>}::get]:
-    Source: '/rustc/library/core/src/cell.rs', lines 541:4-541:32
+    Source: '/rustc/library/core/src/cell.rs', lines 542:4-542:32
     Name pattern: [core::cell::{core::cell::Cell<@T>}::get] *)
 Axiom core_cell_Cell_get :
   forall{T : Type} (markerCopyInst : core_marker_Copy T),
@@ -20,7 +20,7 @@ Axiom core_cell_Cell_get :
 .
 
 (** [core::cell::{core::cell::Cell<T>}::get_mut]:
-    Source: '/rustc/library/core/src/cell.rs', lines 612:4-612:45
+    Source: '/rustc/library/core/src/cell.rs', lines 613:4-613:45
     Name pattern: [core::cell::{core::cell::Cell<@T>}::get_mut] *)
 Axiom core_cell_Cell_get_mut :
   forall{T : Type},
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
index de2dc2b04..b9b720595 100644
--- a/tests/coq/misc/External_TypesExternal_Template.v
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -10,7 +10,7 @@ Local Open Scope Primitives_scope.
 Module External_TypesExternal_Template.
 
 (** [core::cell::Cell]
-    Source: '/rustc/library/core/src/cell.rs', lines 311:0-311:26
+    Source: '/rustc/library/core/src/cell.rs', lines 312:0-312:26
     Name pattern: [core::cell::Cell] *)
 Axiom core_cell_Cell_t : forall (T : Type), Type.
 
diff --git a/tests/coq/misc/Traits.v b/tests/coq/misc/Traits.v
index c13b808a3..f7bed8c4f 100644
--- a/tests/coq/misc/Traits.v
+++ b/tests/coq/misc/Traits.v
@@ -421,9 +421,9 @@ Arguments mkParentTrait1_t { _ }.
 
 (** Trait declaration: [traits::ChildTrait]
     Source: 'tests/src/traits.rs', lines 208:0-208:52 *)
-Record ChildTrait_t (Self : Type) (Self_Clause0_W : Type) := mkChildTrait_t {
+Record ChildTrait_t (Self : Type) (Self_Clause1_W : Type) := mkChildTrait_t {
   ChildTrait_tChildTrait_t_ParentTrait0Inst : ParentTrait0_t Self
-    Self_Clause0_W;
+    Self_Clause1_W;
   ChildTrait_tChildTrait_t_ParentTrait1Inst : ParentTrait1_t Self;
 }.
 
@@ -434,8 +434,8 @@ Arguments ChildTrait_tChildTrait_t_ParentTrait1Inst { _ } { _ } _.
 (** [traits::test_child_trait1]:
     Source: 'tests/src/traits.rs', lines 211:0-213:1 *)
 Definition test_child_trait1
-  {T : Type} {Clause1_Clause0_W : Type} (childTraitInst : ChildTrait_t T
-  Clause1_Clause0_W) (x : T) :
+  {T : Type} {Clause1_Clause1_W : Type} (childTraitInst : ChildTrait_t T
+  Clause1_Clause1_W) (x : T) :
   result string
   :=
   childTraitInst.(ChildTrait_tChildTrait_t_ParentTrait0Inst).(ParentTrait0_t_get_name)
@@ -445,9 +445,9 @@ Definition test_child_trait1
 (** [traits::test_child_trait2]:
     Source: 'tests/src/traits.rs', lines 215:0-217:1 *)
 Definition test_child_trait2
-  {T : Type} {Clause1_Clause0_W : Type} (childTraitInst : ChildTrait_t T
-  Clause1_Clause0_W) (x : T) :
-  result Clause1_Clause0_W
+  {T : Type} {Clause1_Clause1_W : Type} (childTraitInst : ChildTrait_t T
+  Clause1_Clause1_W) (x : T) :
+  result Clause1_Clause1_W
   :=
   childTraitInst.(ChildTrait_tChildTrait_t_ParentTrait0Inst).(ParentTrait0_t_get_w)
     x
@@ -524,10 +524,10 @@ Arguments mkWithTarget_t { _ } { _ }.
 
 (** Trait declaration: [traits::ParentTrait2]
     Source: 'tests/src/traits.rs', lines 258:0-260:1 *)
-Record ParentTrait2_t (Self : Type) (Self_U : Type) (Self_Clause1_Target :
+Record ParentTrait2_t (Self : Type) (Self_U : Type) (Self_Clause2_Target :
   Type) := mkParentTrait2_t {
   ParentTrait2_tParentTrait2_t_WithTargetInst : WithTarget_t Self_U
-    Self_Clause1_Target;
+    Self_Clause2_Target;
 }.
 
 Arguments mkParentTrait2_t { _ } { _ } { _ }.
@@ -535,11 +535,11 @@ Arguments ParentTrait2_tParentTrait2_t_WithTargetInst { _ } { _ } { _ } _.
 
 (** Trait declaration: [traits::ChildTrait2]
     Source: 'tests/src/traits.rs', lines 262:0-264:1 *)
-Record ChildTrait2_t (Self : Type) (Self_Clause0_U : Type)
-  (Self_Clause0_Clause1_Target : Type) := mkChildTrait2_t {
+Record ChildTrait2_t (Self : Type) (Self_Clause1_U : Type)
+  (Self_Clause1_Clause2_Target : Type) := mkChildTrait2_t {
   ChildTrait2_tChildTrait2_t_ParentTrait2Inst : ParentTrait2_t Self
-    Self_Clause0_U Self_Clause0_Clause1_Target;
-  ChildTrait2_t_convert : Self_Clause0_U -> result Self_Clause0_Clause1_Target;
+    Self_Clause1_U Self_Clause1_Clause2_Target;
+  ChildTrait2_t_convert : Self_Clause1_U -> result Self_Clause1_Clause2_Target;
 }.
 
 Arguments mkChildTrait2_t { _ } { _ } { _ }.
@@ -580,10 +580,10 @@ Arguments CFnOnce_t_call_once { _ } { _ } { _ } _.
 
 (** Trait declaration: [traits::CFnMut]
     Source: 'tests/src/traits.rs', lines 294:0-296:1 *)
-Record CFnMut_t (Self : Type) (Args : Type) (Self_Clause0_Output : Type)
+Record CFnMut_t (Self : Type) (Args : Type) (Self_Clause1_Output : Type)
   := mkCFnMut_t {
-  CFnMut_tCFnMut_t_CFnOnceInst : CFnOnce_t Self Args Self_Clause0_Output;
-  CFnMut_t_call_mut : Self -> Args -> result (Self_Clause0_Output * Self);
+  CFnMut_tCFnMut_t_CFnOnceInst : CFnOnce_t Self Args Self_Clause1_Output;
+  CFnMut_t_call_mut : Self -> Args -> result (Self_Clause1_Output * Self);
 }.
 
 Arguments mkCFnMut_t { _ } { _ } { _ }.
@@ -592,10 +592,10 @@ Arguments CFnMut_t_call_mut { _ } { _ } { _ } _.
 
 (** Trait declaration: [traits::CFn]
     Source: 'tests/src/traits.rs', lines 298:0-300:1 *)
-Record CFn_t (Self : Type) (Args : Type) (Self_Clause0_Clause0_Output : Type)
+Record CFn_t (Self : Type) (Args : Type) (Self_Clause1_Clause1_Output : Type)
   := mkCFn_t {
-  CFn_tCFn_t_CFnMutInst : CFnMut_t Self Args Self_Clause0_Clause0_Output;
-  CFn_t_call : Self -> Args -> result Self_Clause0_Clause0_Output;
+  CFn_tCFn_t_CFnMutInst : CFnMut_t Self Args Self_Clause1_Clause1_Output;
+  CFn_t_call : Self -> Args -> result Self_Clause1_Clause1_Output;
 }.
 
 Arguments mkCFn_t { _ } { _ } { _ }.
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index 89ba657e8..b8ef02bf2 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -6,12 +6,12 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::num::{u32}::wrapping_add]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2025:8-2025:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2037:8-2037:58
     Name pattern: [core::num::{u32}::wrapping_add] *)
 assume val core_num_U32_wrapping_add : u32 -> u32 -> result u32
 
 (** [core::num::{u32}::wrapping_sub]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2066:8-2066:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2074:8-2074:58
     Name pattern: [core::num::{u32}::wrapping_sub] *)
 assume val core_num_U32_wrapping_sub : u32 -> u32 -> result u32
 
diff --git a/tests/fstar/misc/DefaultedMethod.fst b/tests/fstar/misc/DefaultedMethod.fst
index 909ee4bd5..8e4368a8c 100644
--- a/tests/fstar/misc/DefaultedMethod.fst
+++ b/tests/fstar/misc/DefaultedMethod.fst
@@ -6,21 +6,21 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** Trait declaration: [core::cmp::PartialEq]
-    Source: '/rustc/library/core/src/cmp.rs', lines 249:0-249:39
+    Source: '/rustc/library/core/src/cmp.rs', lines 252:0-252:59
     Name pattern: [core::cmp::PartialEq] *)
 noeq type core_cmp_PartialEq_t (self : Type0) (rhs : Type0) = {
   eq : self -> rhs -> result bool;
 }
 
 (** Trait declaration: [core::cmp::Eq]
-    Source: '/rustc/library/core/src/cmp.rs', lines 335:0-335:29
+    Source: '/rustc/library/core/src/cmp.rs', lines 338:0-338:44
     Name pattern: [core::cmp::Eq] *)
 noeq type core_cmp_Eq_t (self : Type0) = {
   partialEqInst : core_cmp_PartialEq_t self self;
 }
 
 (** [core::cmp::Ordering]
-    Source: '/rustc/library/core/src/cmp.rs', lines 388:0-388:17
+    Source: '/rustc/library/core/src/cmp.rs', lines 391:0-391:17
     Name pattern: [core::cmp::Ordering] *)
 type core_cmp_Ordering_t =
 | Core_cmp_Ordering_Less : core_cmp_Ordering_t
@@ -28,7 +28,7 @@ type core_cmp_Ordering_t =
 | Core_cmp_Ordering_Greater : core_cmp_Ordering_t
 
 (** Trait declaration: [core::cmp::PartialOrd]
-    Source: '/rustc/library/core/src/cmp.rs', lines 1340:0-1340:56
+    Source: '/rustc/library/core/src/cmp.rs', lines 1344:0-1344:77
     Name pattern: [core::cmp::PartialOrd] *)
 noeq type core_cmp_PartialOrd_t (self : Type0) (rhs : Type0) = {
   partialEqInst : core_cmp_PartialEq_t self rhs;
@@ -36,7 +36,7 @@ noeq type core_cmp_PartialOrd_t (self : Type0) (rhs : Type0) = {
 }
 
 (** Trait declaration: [core::cmp::Ord]
-    Source: '/rustc/library/core/src/cmp.rs', lines 957:0-957:36
+    Source: '/rustc/library/core/src/cmp.rs', lines 960:0-960:51
     Name pattern: [core::cmp::Ord] *)
 noeq type core_cmp_Ord_t (self : Type0) = {
   eqInst : core_cmp_Eq_t self;
@@ -46,29 +46,29 @@ noeq type core_cmp_Ord_t (self : Type0) = {
 }
 
 (** [core::cmp::Ord::min]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1048:4-1050:20
+    Source: '/rustc/library/core/src/cmp.rs', lines 1051:4-1053:20
     Name pattern: [core::cmp::Ord::min] *)
 assume val core_cmp_Ord_min_default
   (#self : Type0) (ordInst : core_cmp_Ord_t self) : self -> self -> result self
 
 (** [core::cmp::impls::{core::cmp::PartialEq<i32> for i32}::eq]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1813:16-1813:50
+    Source: '/rustc/library/core/src/cmp.rs', lines 1819:16-1819:50
     Name pattern: [core::cmp::impls::{core::cmp::PartialEq<i32, i32>}::eq] *)
 assume val core_cmp_impls_PartialEqI32I32_eq : i32 -> i32 -> result bool
 
 (** [core::cmp::impls::{core::cmp::PartialOrd<i32> for i32}::partial_cmp]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1928:16-1928:71
+    Source: '/rustc/library/core/src/cmp.rs', lines 1934:16-1934:71
     Name pattern: [core::cmp::impls::{core::cmp::PartialOrd<i32, i32>}::partial_cmp] *)
 assume val core_cmp_impls_PartialOrdI32I32_partial_cmp
   : i32 -> i32 -> result (option core_cmp_Ordering_t)
 
 (** [core::cmp::impls::{core::cmp::Ord for i32}::cmp]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1938:16-1938:55
+    Source: '/rustc/library/core/src/cmp.rs', lines 1944:16-1944:55
     Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::cmp] *)
 assume val core_cmp_impls_OrdI32_cmp : i32 -> i32 -> result core_cmp_Ordering_t
 
 (** [core::cmp::impls::{core::cmp::Ord for i32}::min]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1936:12-1936:27
+    Source: '/rustc/library/core/src/cmp.rs', lines 1942:12-1942:27
     Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min] *)
 assume val core_cmp_impls_OrdI32_min : i32 -> i32 -> result i32
 
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index a3e06b7be..8b21dc886 100644
--- a/tests/fstar/misc/External.FunsExternal.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -7,14 +7,14 @@ include External.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::cell::{core::cell::Cell<T>}::get]:
-    Source: '/rustc/library/core/src/cell.rs', lines 541:4-541:32
+    Source: '/rustc/library/core/src/cell.rs', lines 542:4-542:32
     Name pattern: [core::cell::{core::cell::Cell<@T>}::get] *)
 val core_cell_Cell_get
   (#t : Type0) (markerCopyInst : core_marker_Copy t) :
   core_cell_Cell_t t -> state -> result (state & t)
 
 (** [core::cell::{core::cell::Cell<T>}::get_mut]:
-    Source: '/rustc/library/core/src/cell.rs', lines 612:4-612:45
+    Source: '/rustc/library/core/src/cell.rs', lines 613:4-613:45
     Name pattern: [core::cell::{core::cell::Cell<@T>}::get_mut] *)
 val core_cell_Cell_get_mut
   (#t : Type0) :
diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti
index daa90218e..87c319686 100644
--- a/tests/fstar/misc/External.TypesExternal.fsti
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -6,7 +6,7 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::cell::Cell]
-    Source: '/rustc/library/core/src/cell.rs', lines 311:0-311:26
+    Source: '/rustc/library/core/src/cell.rs', lines 312:0-312:26
     Name pattern: [core::cell::Cell] *)
 val core_cell_Cell_t (t : Type0) : Type0
 
diff --git a/tests/fstar/misc/Traits.fst b/tests/fstar/misc/Traits.fst
index d9d7e6c59..0f2990420 100644
--- a/tests/fstar/misc/Traits.fst
+++ b/tests/fstar/misc/Traits.fst
@@ -340,16 +340,16 @@ type parentTrait1_t (self : Type0) = unit
 
 (** Trait declaration: [traits::ChildTrait]
     Source: 'tests/src/traits.rs', lines 208:0-208:52 *)
-noeq type childTrait_t (self : Type0) (self_clause0_w : Type0) = {
-  parentTrait0Inst : parentTrait0_t self self_clause0_w;
+noeq type childTrait_t (self : Type0) (self_clause1_w : Type0) = {
+  parentTrait0Inst : parentTrait0_t self self_clause1_w;
   parentTrait1Inst : parentTrait1_t self;
 }
 
 (** [traits::test_child_trait1]:
     Source: 'tests/src/traits.rs', lines 211:0-213:1 *)
 let test_child_trait1
-  (#t : Type0) (#clause1_clause0_w : Type0) (childTraitInst : childTrait_t t
-  clause1_clause0_w) (x : t) :
+  (#t : Type0) (#clause1_clause1_w : Type0) (childTraitInst : childTrait_t t
+  clause1_clause1_w) (x : t) :
   result string
   =
   childTraitInst.parentTrait0Inst.get_name x
@@ -357,9 +357,9 @@ let test_child_trait1
 (** [traits::test_child_trait2]:
     Source: 'tests/src/traits.rs', lines 215:0-217:1 *)
 let test_child_trait2
-  (#t : Type0) (#clause1_clause0_w : Type0) (childTraitInst : childTrait_t t
-  clause1_clause0_w) (x : t) :
-  result clause1_clause0_w
+  (#t : Type0) (#clause1_clause1_w : Type0) (childTraitInst : childTrait_t t
+  clause1_clause1_w) (x : t) :
+  result clause1_clause1_w
   =
   childTraitInst.parentTrait0Inst.get_w x
 
@@ -417,18 +417,18 @@ type withTarget_t (self : Type0) (self_target : Type0) = unit
 
 (** Trait declaration: [traits::ParentTrait2]
     Source: 'tests/src/traits.rs', lines 258:0-260:1 *)
-noeq type parentTrait2_t (self : Type0) (self_u : Type0) (self_clause1_target :
+noeq type parentTrait2_t (self : Type0) (self_u : Type0) (self_clause2_target :
   Type0) = {
-  withTargetInst : withTarget_t self_u self_clause1_target;
+  withTargetInst : withTarget_t self_u self_clause2_target;
 }
 
 (** Trait declaration: [traits::ChildTrait2]
     Source: 'tests/src/traits.rs', lines 262:0-264:1 *)
-noeq type childTrait2_t (self : Type0) (self_clause0_u : Type0)
-  (self_clause0_clause1_target : Type0) = {
-  parentTrait2Inst : parentTrait2_t self self_clause0_u
-    self_clause0_clause1_target;
-  convert : self_clause0_u -> result self_clause0_clause1_target;
+noeq type childTrait2_t (self : Type0) (self_clause1_u : Type0)
+  (self_clause1_clause2_target : Type0) = {
+  parentTrait2Inst : parentTrait2_t self self_clause1_u
+    self_clause1_clause2_target;
+  convert : self_clause1_u -> result self_clause1_clause2_target;
 }
 
 (** Trait implementation: [traits::{traits::WithTarget<u32> for u32}]
@@ -461,18 +461,18 @@ noeq type cFnOnce_t (self : Type0) (args : Type0) (self_output : Type0) = {
 
 (** Trait declaration: [traits::CFnMut]
     Source: 'tests/src/traits.rs', lines 294:0-296:1 *)
-noeq type cFnMut_t (self : Type0) (args : Type0) (self_clause0_output : Type0)
+noeq type cFnMut_t (self : Type0) (args : Type0) (self_clause1_output : Type0)
   = {
-  cFnOnceInst : cFnOnce_t self args self_clause0_output;
-  call_mut : self -> args -> result (self_clause0_output & self);
+  cFnOnceInst : cFnOnce_t self args self_clause1_output;
+  call_mut : self -> args -> result (self_clause1_output & self);
 }
 
 (** Trait declaration: [traits::CFn]
     Source: 'tests/src/traits.rs', lines 298:0-300:1 *)
-noeq type cFn_t (self : Type0) (args : Type0) (self_clause0_clause0_output :
+noeq type cFn_t (self : Type0) (args : Type0) (self_clause1_clause1_output :
   Type0) = {
-  cFnMutInst : cFnMut_t self args self_clause0_clause0_output;
-  call : self -> args -> result self_clause0_clause0_output;
+  cFnMutInst : cFnMut_t self args self_clause1_clause1_output;
+  call : self -> args -> result self_clause1_clause1_output;
 }
 
 (** Trait declaration: [traits::GetTrait]
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index e5a3987b2..ffc792cb1 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -10,14 +10,14 @@ set_option linter.unusedVariables false
 open external
 
 /- [core::cell::{core::cell::Cell<T>}::get]:
-   Source: '/rustc/library/core/src/cell.rs', lines 541:4-541:32
+   Source: '/rustc/library/core/src/cell.rs', lines 542:4-542:32
    Name pattern: [core::cell::{core::cell::Cell<@T>}::get] -/
 axiom core.cell.Cell.get
   {T : Type} (markerCopyInst : core.marker.Copy T) :
   core.cell.Cell T → State → Result (State × T)
 
 /- [core::cell::{core::cell::Cell<T>}::get_mut]:
-   Source: '/rustc/library/core/src/cell.rs', lines 612:4-612:45
+   Source: '/rustc/library/core/src/cell.rs', lines 613:4-613:45
    Name pattern: [core::cell::{core::cell::Cell<@T>}::get_mut] -/
 axiom core.cell.Cell.get_mut
   {T : Type} :
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
index 06a9df2cf..6714831ef 100644
--- a/tests/lean/External/TypesExternal_Template.lean
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -8,7 +8,7 @@ set_option linter.hashCommand false
 set_option linter.unusedVariables false
 
 /- [core::cell::Cell]
-   Source: '/rustc/library/core/src/cell.rs', lines 311:0-311:26
+   Source: '/rustc/library/core/src/cell.rs', lines 312:0-312:26
    Name pattern: [core::cell::Cell] -/
 axiom core.cell.Cell (T : Type) : Type
 
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index a7454a4e1..f239e064e 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -357,15 +357,15 @@ structure ParentTrait1 (Self : Type) where
 
 /- Trait declaration: [traits::ChildTrait]
    Source: 'tests/src/traits.rs', lines 208:0-208:52 -/
-structure ChildTrait (Self : Type) (Self_Clause0_W : Type) where
-  ParentTrait0Inst : ParentTrait0 Self Self_Clause0_W
+structure ChildTrait (Self : Type) (Self_Clause1_W : Type) where
+  ParentTrait0Inst : ParentTrait0 Self Self_Clause1_W
   ParentTrait1Inst : ParentTrait1 Self
 
 /- [traits::test_child_trait1]:
    Source: 'tests/src/traits.rs', lines 211:0-213:1 -/
 def test_child_trait1
-  {T : Type} {Clause1_Clause0_W : Type} (ChildTraitInst : ChildTrait T
-  Clause1_Clause0_W) (x : T) :
+  {T : Type} {Clause1_Clause1_W : Type} (ChildTraitInst : ChildTrait T
+  Clause1_Clause1_W) (x : T) :
   Result String
   :=
   ChildTraitInst.ParentTrait0Inst.get_name x
@@ -373,9 +373,9 @@ def test_child_trait1
 /- [traits::test_child_trait2]:
    Source: 'tests/src/traits.rs', lines 215:0-217:1 -/
 def test_child_trait2
-  {T : Type} {Clause1_Clause0_W : Type} (ChildTraitInst : ChildTrait T
-  Clause1_Clause0_W) (x : T) :
-  Result Clause1_Clause0_W
+  {T : Type} {Clause1_Clause1_W : Type} (ChildTraitInst : ChildTrait T
+  Clause1_Clause1_W) (x : T) :
+  Result Clause1_Clause1_W
   :=
   ChildTraitInst.ParentTrait0Inst.get_w x
 
@@ -432,17 +432,17 @@ structure WithTarget (Self : Type) (Self_Target : Type) where
 
 /- Trait declaration: [traits::ParentTrait2]
    Source: 'tests/src/traits.rs', lines 258:0-260:1 -/
-structure ParentTrait2 (Self : Type) (Self_U : Type) (Self_Clause1_Target :
+structure ParentTrait2 (Self : Type) (Self_U : Type) (Self_Clause2_Target :
   Type) where
-  WithTargetInst : WithTarget Self_U Self_Clause1_Target
+  WithTargetInst : WithTarget Self_U Self_Clause2_Target
 
 /- Trait declaration: [traits::ChildTrait2]
    Source: 'tests/src/traits.rs', lines 262:0-264:1 -/
-structure ChildTrait2 (Self : Type) (Self_Clause0_U : Type)
-  (Self_Clause0_Clause1_Target : Type) where
-  ParentTrait2Inst : ParentTrait2 Self Self_Clause0_U
-    Self_Clause0_Clause1_Target
-  convert : Self_Clause0_U → Result Self_Clause0_Clause1_Target
+structure ChildTrait2 (Self : Type) (Self_Clause1_U : Type)
+  (Self_Clause1_Clause2_Target : Type) where
+  ParentTrait2Inst : ParentTrait2 Self Self_Clause1_U
+    Self_Clause1_Clause2_Target
+  convert : Self_Clause1_U → Result Self_Clause1_Clause2_Target
 
 /- Trait implementation: [traits::{traits::WithTarget<u32> for u32}]
    Source: 'tests/src/traits.rs', lines 266:0-268:1 -/
@@ -477,16 +477,16 @@ structure CFnOnce (Self : Type) (Args : Type) (Self_Output : Type) where
 
 /- Trait declaration: [traits::CFnMut]
    Source: 'tests/src/traits.rs', lines 294:0-296:1 -/
-structure CFnMut (Self : Type) (Args : Type) (Self_Clause0_Output : Type) where
-  CFnOnceInst : CFnOnce Self Args Self_Clause0_Output
-  call_mut : Self → Args → Result (Self_Clause0_Output × Self)
+structure CFnMut (Self : Type) (Args : Type) (Self_Clause1_Output : Type) where
+  CFnOnceInst : CFnOnce Self Args Self_Clause1_Output
+  call_mut : Self → Args → Result (Self_Clause1_Output × Self)
 
 /- Trait declaration: [traits::CFn]
    Source: 'tests/src/traits.rs', lines 298:0-300:1 -/
-structure CFn (Self : Type) (Args : Type) (Self_Clause0_Clause0_Output : Type)
+structure CFn (Self : Type) (Args : Type) (Self_Clause1_Clause1_Output : Type)
   where
-  CFnMutInst : CFnMut Self Args Self_Clause0_Clause0_Output
-  call : Self → Args → Result Self_Clause0_Clause0_Output
+  CFnMutInst : CFnMut Self Args Self_Clause1_Clause1_Output
+  call : Self → Args → Result Self_Clause1_Clause1_Output
 
 /- Trait declaration: [traits::GetTrait]
    Source: 'tests/src/traits.rs', lines 302:0-305:1 -/