diff --git a/backends/lean/Aeneas/Std/Core/Cmp.lean b/backends/lean/Aeneas/Std/Core/Cmp.lean
index 90e4c8784..42c5cf7c5 100644
--- a/backends/lean/Aeneas/Std/Core/Cmp.lean
+++ b/backends/lean/Aeneas/Std/Core/Cmp.lean
@@ -13,12 +13,12 @@ structure core.cmp.PartialEq (Self : Type) (Rhs : Type) where
 @[rust_trait "core::cmp::Eq" (parentClauses := ["partialEqInst"])]
 structure core.cmp.Eq (Self : Type) where
   partialEqInst : core.cmp.PartialEq Self Self
-  assert_receiver_is_total_eq (_ : Self) : Result Unit := .ok ()
+  assert_fields_are_eq (_ : Self) : Result Unit := .ok ()
 
-@[simp, rust_fun "core::cmp::Eq::assert_receiver_is_total_eq"]
-def core.cmp.Eq.assert_receiver_is_total_eq.default
+@[simp, rust_fun "core::cmp::Eq::assert_fields_are_eq"]
+def core.cmp.Eq.assert_fields_are_eq.default
   {Self : Type} (EqInst : core.cmp.Eq Self) (x : Self) : Result Unit :=
-  EqInst.assert_receiver_is_total_eq x
+  EqInst.assert_fields_are_eq x
 
 /- Default method -/
 @[rust_fun "core::cmp::PartialEq::ne"]
diff --git a/charon-pin b/charon-pin
index 19901b667..ca309b005 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.
-d986428c0225810607e95f858a5b07afcfd15f92
+42836b36b666a980cbc9d438a8aed340ad3b848b
diff --git a/flake.lock b/flake.lock
index 499f67ded..37ae0ed51 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1780234437,
-        "narHash": "sha256-3VpxFIRcoJ7FuOETdvQL7rlHwqXGAXM5us9puVjX12E=",
+        "lastModified": 1780248582,
+        "narHash": "sha256-zzh6JL6Boun4OFBSndfSM+5aZJUXfVNaYgePxIszBOA=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "d986428c0225810607e95f858a5b07afcfd15f92",
+        "rev": "42836b36b666a980cbc9d438a8aed340ad3b848b",
         "type": "github"
       },
       "original": {
@@ -158,17 +158,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1771902481,
-        "narHash": "sha256-svI5ivzggtu4KhCdoab3xR5+Btop24o7yLFtIPXrsPM=",
+        "lastModified": 1780024773,
+        "narHash": "sha256-aU9nlrS9S+IJ2EiCzsaxzOXUhggogqTrJojBicE6Oeg=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "5177426d9f8f7f1827001c9749b9a9c5570d456b",
+        "rev": "40b0a3a193e0840c76174b4a322874c8f6dd0a63",
         "type": "github"
       },
       "original": {
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "5177426d9f8f7f1827001c9749b9a9c5570d456b",
+        "rev": "40b0a3a193e0840c76174b4a322874c8f6dd0a63",
         "type": "github"
       }
     },
diff --git a/src/extract/ExtractBuiltinLean.ml b/src/extract/ExtractBuiltinLean.ml
index c5da6ac89..433e0fd17 100644
--- a/src/extract/ExtractBuiltinLean.ml
+++ b/src/extract/ExtractBuiltinLean.ml
@@ -383,8 +383,8 @@ let lean_builtin_funs =
     mk_fun "core::clone::impls::{core::clone::Clone<&'0 @T>}::clone"
       "core.clone.impls.CloneShared.clone";
     (* file: "Aeneas/Std/Core/Cmp.lean", line: 18 *)
-    mk_fun "core::cmp::Eq::assert_receiver_is_total_eq"
-      "core.cmp.Eq.assert_receiver_is_total_eq.default";
+    mk_fun "core::cmp::Eq::assert_fields_are_eq"
+      "core.cmp.Eq.assert_fields_are_eq.default";
     (* file: "Aeneas/Std/Core/Cmp.lean", line: 98 *)
     mk_fun "core::cmp::Ord::clamp" "core.cmp.Ord.clamp.default";
     (* file: "Aeneas/Std/Core/Cmp.lean", line: 86 *)
@@ -948,8 +948,7 @@ let lean_builtin_trait_decls =
     (* file: "Aeneas/Std/Core/Cmp.lean", line: 13 *)
     mk_trait_decl "core::cmp::Eq" "core.cmp.Eq"
       ~parent_clauses:[ "partialEqInst" ]
-      ~methods:
-        [ ("assert_receiver_is_total_eq", "assert_receiver_is_total_eq") ];
+      ~methods:[ ("assert_fields_are_eq", "assert_fields_are_eq") ];
     (* file: "Aeneas/Std/Core/Cmp.lean", line: 76 *)
     mk_trait_decl "core::cmp::Ord" "core.cmp.Ord"
       ~parent_clauses:[ "eqInst"; "partialOrdInst" ]
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 4a7d9d5e2..5b19636e0 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -9,13 +9,13 @@ Local Open Scope Primitives_scope.
 Module Demo.
 
 (** [core::num::{u32}::wrapping_add]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2456:8-2456:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2505:8-2505:58
     Name pattern: [core::num::{u32}::wrapping_add]
     Visibility: public *)
 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 2493:8-2493:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2542:8-2542:58
     Name pattern: [core::num::{u32}::wrapping_sub]
     Visibility: public *)
 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 b1745fa85..e8e57dad6 100644
--- a/tests/coq/misc/DefaultedMethod.v
+++ b/tests/coq/misc/DefaultedMethod.v
@@ -9,7 +9,7 @@ Local Open Scope Primitives_scope.
 Module DefaultedMethod.
 
 (** [core::cmp::impls::{impl core::cmp::Ord for i32}::min]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 2000:12-2000:33
+    Source: '/rustc/library/core/src/cmp.rs', lines 2007:12-2007:33
     Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min]
     Visibility: public *)
 Axiom I32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32.
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index 40a70db7c..b9a40dbcf 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -6,13 +6,13 @@ 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 2456:8-2456:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2505:8-2505:58
     Name pattern: [core::num::{u32}::wrapping_add]
     Visibility: public *)
 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 2493:8-2493:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2542:8-2542:58
     Name pattern: [core::num::{u32}::wrapping_sub]
     Visibility: public *)
 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 0d5f8d697..ed722d32e 100644
--- a/tests/fstar/misc/DefaultedMethod.fst
+++ b/tests/fstar/misc/DefaultedMethod.fst
@@ -6,7 +6,7 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::cmp::impls::{impl core::cmp::Ord for i32}::min]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 2000:12-2000:33
+    Source: '/rustc/library/core/src/cmp.rs', lines 2007:12-2007:33
     Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min]
     Visibility: public *)
 assume val i32_Insts_CoreCmpOrd_min : i32 -> i32 -> result i32
diff --git a/tests/lean/BuiltinAuto.lean b/tests/lean/BuiltinAuto.lean
index a3a080073..7b2e5da9a 100644
--- a/tests/lean/BuiltinAuto.lean
+++ b/tests/lean/BuiltinAuto.lean
@@ -18,7 +18,7 @@ noncomputable section
 namespace builtin_auto
 
 /-- [core::ptr::null]:
-    Source: '/rustc/library/core/src/ptr/mod.rs', lines 837:0-837:55
+    Source: '/rustc/library/core/src/ptr/mod.rs', lines 842:0-842:55
     Name pattern: [core::ptr::null]
     Visibility: public -/
 @[rust_fun "core::ptr::null"]
diff --git a/tests/lean/Derive.lean b/tests/lean/Derive.lean
index 56392cb6b..3fb96ffac 100644
--- a/tests/lean/Derive.lean
+++ b/tests/lean/Derive.lean
@@ -18,14 +18,14 @@ noncomputable section
 namespace derive
 
 /-- [core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}::ne]:
-    Source: '/rustc/library/core/src/cmp.rs', lines 1872:16-1872:50
+    Source: '/rustc/library/core/src/cmp.rs', lines 1879:16-1879:50
     Name pattern: [core::cmp::impls::{core::cmp::PartialEq<bool, bool>}::ne]
     Visibility: public -/
 @[rust_fun "core::cmp::impls::{core::cmp::PartialEq<bool, bool>}::ne"]
 axiom Bool.Insts.CoreCmpPartialEqBool.ne : Bool → Bool → Result Bool
 
 /-- [alloc::boxed::{impl core::cmp::PartialEq<alloc::boxed::Box<T>> for alloc::boxed::Box<T>}::ne]:
-    Source: '/rustc/library/alloc/src/boxed.rs', lines 2100:4-2100:38
+    Source: '/rustc/library/alloc/src/boxed.rs', lines 2109:4-2109:38
     Name pattern: [alloc::boxed::{core::cmp::PartialEq<Box<@T>, Box<@T>>}::ne]
     Visibility: public -/
 @[rust_fun "alloc::boxed::{core::cmp::PartialEq<Box<@T>, Box<@T>>}::ne"]
@@ -93,10 +93,10 @@ def CopyEnumOneVariant.Insts.CoreCmpPartialEqCopyEnumOneVariant :
   ne := CopyEnumOneVariant.Insts.CoreCmpPartialEqCopyEnumOneVariant.ne
 }
 
-/-- [derive::{impl core::cmp::Eq for derive::CopyEnumOneVariant}::assert_receiver_is_total_eq]:
+/-- [derive::{impl core::cmp::Eq for derive::CopyEnumOneVariant}::assert_fields_are_eq]:
     Source: 'tests/src/derive.rs', lines 3:33-3:35
     Visibility: public -/
-def CopyEnumOneVariant.Insts.CoreCmpEq.assert_receiver_is_total_eq
+def CopyEnumOneVariant.Insts.CoreCmpEq.assert_fields_are_eq
   (self : CopyEnumOneVariant) : Result Unit := do
   ok ()
 
@@ -105,8 +105,8 @@ def CopyEnumOneVariant.Insts.CoreCmpEq.assert_receiver_is_total_eq
 @[reducible]
 def CopyEnumOneVariant.Insts.CoreCmpEq : core.cmp.Eq CopyEnumOneVariant := {
   partialEqInst := CopyEnumOneVariant.Insts.CoreCmpPartialEqCopyEnumOneVariant
-  assert_receiver_is_total_eq :=
-    CopyEnumOneVariant.Insts.CoreCmpEq.assert_receiver_is_total_eq
+  assert_fields_are_eq :=
+    CopyEnumOneVariant.Insts.CoreCmpEq.assert_fields_are_eq
 }
 
 /-- [derive::{impl core::fmt::Debug for derive::CopyEnumOneVariant}::fmt]:
@@ -189,10 +189,10 @@ def ScalarEnum.Insts.CoreCmpPartialEqScalarEnum : core.cmp.PartialEq ScalarEnum
   ne := ScalarEnum.Insts.CoreCmpPartialEqScalarEnum.ne
 }
 
-/-- [derive::{impl core::cmp::Eq for derive::ScalarEnum}::assert_receiver_is_total_eq]:
+/-- [derive::{impl core::cmp::Eq for derive::ScalarEnum}::assert_fields_are_eq]:
     Source: 'tests/src/derive.rs', lines 8:33-8:35
     Visibility: public -/
-def ScalarEnum.Insts.CoreCmpEq.assert_receiver_is_total_eq
+def ScalarEnum.Insts.CoreCmpEq.assert_fields_are_eq
   (self : ScalarEnum) : Result Unit := do
   ok ()
 
@@ -201,8 +201,7 @@ def ScalarEnum.Insts.CoreCmpEq.assert_receiver_is_total_eq
 @[reducible]
 def ScalarEnum.Insts.CoreCmpEq : core.cmp.Eq ScalarEnum := {
   partialEqInst := ScalarEnum.Insts.CoreCmpPartialEqScalarEnum
-  assert_receiver_is_total_eq :=
-    ScalarEnum.Insts.CoreCmpEq.assert_receiver_is_total_eq
+  assert_fields_are_eq := ScalarEnum.Insts.CoreCmpEq.assert_fields_are_eq
 }
 
 /-- [derive::{impl core::fmt::Debug for derive::ScalarEnum}::fmt]:
@@ -330,10 +329,10 @@ def CopyEnum.Insts.CoreCmpPartialEqCopyEnum {T : Type} (corecmpPartialEqInst :
   ne := CopyEnum.Insts.CoreCmpPartialEqCopyEnum.ne corecmpPartialEqInst
 }
 
-/-- [derive::{impl core::cmp::Eq for derive::CopyEnum<T>}::assert_receiver_is_total_eq]:
+/-- [derive::{impl core::cmp::Eq for derive::CopyEnum<T>}::assert_fields_are_eq]:
     Source: 'tests/src/derive.rs', lines 16:33-16:35
     Visibility: public -/
-def CopyEnum.Insts.CoreCmpEq.assert_receiver_is_total_eq
+def CopyEnum.Insts.CoreCmpEq.assert_fields_are_eq
   {T : Type} (corecmpEqInst : core.cmp.Eq T) (self : CopyEnum T) :
   Result Unit
   := do
@@ -346,8 +345,8 @@ def CopyEnum.Insts.CoreCmpEq {T : Type} (corecmpEqInst : core.cmp.Eq T) :
   core.cmp.Eq (CopyEnum T) := {
   partialEqInst := CopyEnum.Insts.CoreCmpPartialEqCopyEnum
     corecmpEqInst.partialEqInst
-  assert_receiver_is_total_eq :=
-    CopyEnum.Insts.CoreCmpEq.assert_receiver_is_total_eq corecmpEqInst
+  assert_fields_are_eq := CopyEnum.Insts.CoreCmpEq.assert_fields_are_eq
+    corecmpEqInst
 }
 
 /-- [derive::{impl core::fmt::Debug for derive::CopyEnum<T>}::fmt]:
@@ -492,10 +491,10 @@ def Enum.Insts.CoreCmpPartialEqEnum {T : Type} (corecmpPartialEqInst :
   ne := Enum.Insts.CoreCmpPartialEqEnum.ne corecmpPartialEqInst
 }
 
-/-- [derive::{impl core::cmp::Eq for derive::Enum<T>}::assert_receiver_is_total_eq]:
+/-- [derive::{impl core::cmp::Eq for derive::Enum<T>}::assert_fields_are_eq]:
     Source: 'tests/src/derive.rs', lines 24:27-24:29
     Visibility: public -/
-def Enum.Insts.CoreCmpEq.assert_receiver_is_total_eq
+def Enum.Insts.CoreCmpEq.assert_fields_are_eq
   {T : Type} (corecmpEqInst : core.cmp.Eq T) (self : Enum T) :
   Result Unit
   := do
@@ -507,8 +506,8 @@ def Enum.Insts.CoreCmpEq.assert_receiver_is_total_eq
 def Enum.Insts.CoreCmpEq {T : Type} (corecmpEqInst : core.cmp.Eq T) :
   core.cmp.Eq (Enum T) := {
   partialEqInst := Enum.Insts.CoreCmpPartialEqEnum corecmpEqInst.partialEqInst
-  assert_receiver_is_total_eq :=
-    Enum.Insts.CoreCmpEq.assert_receiver_is_total_eq corecmpEqInst
+  assert_fields_are_eq := Enum.Insts.CoreCmpEq.assert_fields_are_eq
+    corecmpEqInst
 }
 
 /-- [derive::{impl core::fmt::Debug for derive::Enum<T>}::fmt]:
@@ -627,10 +626,10 @@ def List.Insts.CoreCmpPartialEqList {T : Type} (corecmpPartialEqInst :
   ne := List.Insts.CoreCmpPartialEqList.ne corecmpPartialEqInst
 }
 
-/-- [derive::{impl core::cmp::Eq for derive::List<T>}::assert_receiver_is_total_eq]:
+/-- [derive::{impl core::cmp::Eq for derive::List<T>}::assert_fields_are_eq]:
     Source: 'tests/src/derive.rs', lines 34:27-34:29
     Visibility: public -/
-def List.Insts.CoreCmpEq.assert_receiver_is_total_eq
+def List.Insts.CoreCmpEq.assert_fields_are_eq
   {T : Type} (corecmpEqInst : core.cmp.Eq T) (self : List T) :
   Result Unit
   := do
@@ -642,8 +641,8 @@ def List.Insts.CoreCmpEq.assert_receiver_is_total_eq
 def List.Insts.CoreCmpEq {T : Type} (corecmpEqInst : core.cmp.Eq T) :
   core.cmp.Eq (List T) := {
   partialEqInst := List.Insts.CoreCmpPartialEqList corecmpEqInst.partialEqInst
-  assert_receiver_is_total_eq :=
-    List.Insts.CoreCmpEq.assert_receiver_is_total_eq corecmpEqInst
+  assert_fields_are_eq := List.Insts.CoreCmpEq.assert_fields_are_eq
+    corecmpEqInst
 }
 
 /-- [derive::CopyStruct]
@@ -726,10 +725,10 @@ def CopyStruct.Insts.CoreCmpPartialEqCopyStruct {T : Type}
   ne := CopyStruct.Insts.CoreCmpPartialEqCopyStruct.ne corecmpPartialEqInst
 }
 
-/-- [derive::{impl core::cmp::Eq for derive::CopyStruct<T>}::assert_receiver_is_total_eq]:
+/-- [derive::{impl core::cmp::Eq for derive::CopyStruct<T>}::assert_fields_are_eq]:
     Source: 'tests/src/derive.rs', lines 41:33-41:35
     Visibility: public -/
-def CopyStruct.Insts.CoreCmpEq.assert_receiver_is_total_eq
+def CopyStruct.Insts.CoreCmpEq.assert_fields_are_eq
   {T : Type} (corecmpEqInst : core.cmp.Eq T) (self : CopyStruct T) :
   Result Unit
   := do
@@ -742,8 +741,8 @@ def CopyStruct.Insts.CoreCmpEq {T : Type} (corecmpEqInst : core.cmp.Eq T) :
   core.cmp.Eq (CopyStruct T) := {
   partialEqInst := CopyStruct.Insts.CoreCmpPartialEqCopyStruct
     corecmpEqInst.partialEqInst
-  assert_receiver_is_total_eq :=
-    CopyStruct.Insts.CoreCmpEq.assert_receiver_is_total_eq corecmpEqInst
+  assert_fields_are_eq := CopyStruct.Insts.CoreCmpEq.assert_fields_are_eq
+    corecmpEqInst
 }
 
 /-- [derive::{impl core::fmt::Debug for derive::CopyStruct<T>}::fmt]:
@@ -825,10 +824,10 @@ def Struct.Insts.CoreCmpPartialEqStruct {T : Type} (corecmpPartialEqInst :
   ne := Struct.Insts.CoreCmpPartialEqStruct.ne corecmpPartialEqInst
 }
 
-/-- [derive::{impl core::cmp::Eq for derive::Struct<T>}::assert_receiver_is_total_eq]:
+/-- [derive::{impl core::cmp::Eq for derive::Struct<T>}::assert_fields_are_eq]:
     Source: 'tests/src/derive.rs', lines 49:27-49:29
     Visibility: public -/
-def Struct.Insts.CoreCmpEq.assert_receiver_is_total_eq
+def Struct.Insts.CoreCmpEq.assert_fields_are_eq
   {T : Type} (corecmpEqInst : core.cmp.Eq T) (self : Struct T) :
   Result Unit
   := do
@@ -841,8 +840,8 @@ def Struct.Insts.CoreCmpEq {T : Type} (corecmpEqInst : core.cmp.Eq T) :
   core.cmp.Eq (Struct T) := {
   partialEqInst := Struct.Insts.CoreCmpPartialEqStruct
     corecmpEqInst.partialEqInst
-  assert_receiver_is_total_eq :=
-    Struct.Insts.CoreCmpEq.assert_receiver_is_total_eq corecmpEqInst
+  assert_fields_are_eq := Struct.Insts.CoreCmpEq.assert_fields_are_eq
+    corecmpEqInst
 }
 
 /-- [derive::{impl core::fmt::Debug for derive::Struct<T>}::fmt]:
@@ -939,10 +938,10 @@ def Struct6Fields.Insts.CoreCmpPartialEqStruct6Fields : core.cmp.PartialEq
   ne := Struct6Fields.Insts.CoreCmpPartialEqStruct6Fields.ne
 }
 
-/-- [derive::{impl core::cmp::Eq for derive::Struct6Fields}::assert_receiver_is_total_eq]:
+/-- [derive::{impl core::cmp::Eq for derive::Struct6Fields}::assert_fields_are_eq]:
     Source: 'tests/src/derive.rs', lines 54:27-54:29
     Visibility: public -/
-def Struct6Fields.Insts.CoreCmpEq.assert_receiver_is_total_eq
+def Struct6Fields.Insts.CoreCmpEq.assert_fields_are_eq
   (self : Struct6Fields) : Result Unit := do
   ok ()
 
@@ -951,8 +950,7 @@ def Struct6Fields.Insts.CoreCmpEq.assert_receiver_is_total_eq
 @[reducible]
 def Struct6Fields.Insts.CoreCmpEq : core.cmp.Eq Struct6Fields := {
   partialEqInst := Struct6Fields.Insts.CoreCmpPartialEqStruct6Fields
-  assert_receiver_is_total_eq :=
-    Struct6Fields.Insts.CoreCmpEq.assert_receiver_is_total_eq
+  assert_fields_are_eq := Struct6Fields.Insts.CoreCmpEq.assert_fields_are_eq
 }
 
 /-- [derive::{impl core::fmt::Debug for derive::Struct6Fields}::fmt]:
diff --git a/tests/lean/Iterators.lean b/tests/lean/Iterators.lean
index 7b9f68b93..3d0f64099 100644
--- a/tests/lean/Iterators.lean
+++ b/tests/lean/Iterators.lean
@@ -39,7 +39,7 @@ axiom core.iter.adapters.zip.Zip.Insts.CoreIterTraitsIteratorIteratorPair.next
     Clause1_Item)) × (core.iter.adapters.zip.Zip A B))
 
 /-- [core::iter::range::{impl core::iter::traits::iterator::Iterator<A> for core::ops::range::Range<A>}::zip]:
-    Source: '/rustc/library/core/src/iter/range.rs', lines 852:0-852:40
+    Source: '/rustc/library/core/src/iter/range.rs', lines 980:0-980:40
     Name pattern: [core::iter::range::{core::iter::traits::iterator::Iterator<core::ops::range::Range<@A>, @A>}::zip]
     Visibility: public -/
 @[rust_fun
@@ -52,7 +52,7 @@ axiom core.ops.range.Range.Insts.CoreIterTraitsIteratorIterator.zip
     (core.ops.range.Range A) Clause1_IntoIter)
 
 /-- [core::iter::traits::iterator::Iterator::zip]:
-    Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 626:4-629:24
+    Source: '/rustc/library/core/src/iter/traits/iterator.rs', lines 631:4-634:24
     Name pattern: [core::iter::traits::iterator::Iterator::zip]
     Visibility: public -/
 @[rust_fun "core::iter::traits::iterator::Iterator::zip"]
diff --git a/tests/lean/LoopsIssues.lean b/tests/lean/LoopsIssues.lean
index f14c41b92..5481ad755 100644
--- a/tests/lean/LoopsIssues.lean
+++ b/tests/lean/LoopsIssues.lean
@@ -18,7 +18,7 @@ noncomputable section
 namespace loops_issues
 
 /-- [core::iter::range::{impl core::iter::range::Step for i32}::backward_checked]:
-    Source: '/rustc/library/core/src/iter/range.rs', lines 340:16-340:74
+    Source: '/rustc/library/core/src/iter/range.rs', lines 342:16-342:74
     Name pattern: [core::iter::range::{core::iter::range::Step<i32>}::backward_checked]
     Visibility: public -/
 @[rust_fun
@@ -27,7 +27,7 @@ axiom I32.Insts.CoreIterRangeStep.backward_checked
   : Std.I32 → Std.Usize → Result (Option Std.I32)
 
 /-- [core::iter::range::{impl core::iter::range::Step for i32}::forward_checked]:
-    Source: '/rustc/library/core/src/iter/range.rs', lines 319:16-319:73
+    Source: '/rustc/library/core/src/iter/range.rs', lines 321:16-321:73
     Name pattern: [core::iter::range::{core::iter::range::Step<i32>}::forward_checked]
     Visibility: public -/
 @[rust_fun
@@ -36,7 +36,7 @@ axiom I32.Insts.CoreIterRangeStep.forward_checked
   : Std.I32 → Std.Usize → Result (Option Std.I32)
 
 /-- [core::iter::range::{impl core::iter::range::Step for i32}::steps_between]:
-    Source: '/rustc/library/core/src/iter/range.rs', lines 304:16-304:84
+    Source: '/rustc/library/core/src/iter/range.rs', lines 306:16-306:84
     Name pattern: [core::iter::range::{core::iter::range::Step<i32>}::steps_between]
     Visibility: public -/
 @[rust_fun "core::iter::range::{core::iter::range::Step<i32>}::steps_between"]
@@ -44,7 +44,7 @@ axiom I32.Insts.CoreIterRangeStep.steps_between
   : Std.I32 → Std.I32 → Result (Std.Usize × (Option Std.Usize))
 
 /-- Trait implementation: [core::iter::range::{impl core::iter::range::Step for i32}]
-    Source: '/rustc/library/core/src/iter/range.rs', lines 299:12-299:37
+    Source: '/rustc/library/core/src/iter/range.rs', lines 301:12-301:43
     Name pattern: [core::iter::range::Step<i32>] -/
 @[reducible, rust_trait_impl "core::iter::range::Step<i32>"]
 def I32.Insts.CoreIterRangeStep : core.iter.range.Step Std.I32 := {
diff --git a/tests/lean/Order.lean b/tests/lean/Order.lean
index 0ec80d943..4040455b6 100644
--- a/tests/lean/Order.lean
+++ b/tests/lean/Order.lean
@@ -63,11 +63,10 @@ def Wrap.Insts.CoreCmpPartialEqWrap : core.cmp.PartialEq Wrap Wrap := {
   eq := Wrap.Insts.CoreCmpPartialEqWrap.eq
 }
 
-/-- [order::{impl core::cmp::Eq for order::Wrap}::assert_receiver_is_total_eq]:
+/-- [order::{impl core::cmp::Eq for order::Wrap}::assert_fields_are_eq]:
     Source: 'tests/src/order.rs', lines 21:20-21:22
     Visibility: public -/
-def Wrap.Insts.CoreCmpEq.assert_receiver_is_total_eq
-  (self : Wrap) : Result Unit := do
+def Wrap.Insts.CoreCmpEq.assert_fields_are_eq (self : Wrap) : Result Unit := do
   ok ()
 
 /-- Trait implementation: [order::{impl core::cmp::Eq for order::Wrap}]
@@ -75,8 +74,7 @@ def Wrap.Insts.CoreCmpEq.assert_receiver_is_total_eq
 @[reducible]
 def Wrap.Insts.CoreCmpEq : core.cmp.Eq Wrap := {
   partialEqInst := Wrap.Insts.CoreCmpPartialEqWrap
-  assert_receiver_is_total_eq :=
-    Wrap.Insts.CoreCmpEq.assert_receiver_is_total_eq
+  assert_fields_are_eq := Wrap.Insts.CoreCmpEq.assert_fields_are_eq
 }
 
 /-- [order::{impl core::cmp::PartialOrd<order::Wrap> for order::Wrap}::partial_cmp]:
diff --git a/tests/lean/RustBorrowCheckIssues.lean b/tests/lean/RustBorrowCheckIssues.lean
index 8de63da8c..2bd16c6f5 100644
--- a/tests/lean/RustBorrowCheckIssues.lean
+++ b/tests/lean/RustBorrowCheckIssues.lean
@@ -18,7 +18,7 @@ noncomputable section
 namespace rust_borrow_check_issues
 
 /-- [core::mem::drop]:
-    Source: '/rustc/library/core/src/mem/mod.rs', lines 971:0-973:24
+    Source: '/rustc/library/core/src/mem/mod.rs', lines 1000:0-1002:24
     Name pattern: [core::mem::drop]
     Visibility: public -/
 @[rust_fun "core::mem::drop"]