diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index 48fde64e14..fcc56570e4 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -875,12 +875,8 @@ Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usi
   | Fail_ e => Fail_ e
   end.
 
-(* Trait declaration: [core::slice::index::private_slice_index::Sealed] *)
-Definition core_slice_index_private_slice_index_Sealed (self : Type) := unit.
-
 (* Trait declaration: [core::slice::index::SliceIndex] *)
 Record core_slice_index_SliceIndex (Self T Output : Type) := mk_core_slice_index_SliceIndex {
-  core_slice_index_SliceIndex_sealedInst : core_slice_index_private_slice_index_Sealed Self;
   core_slice_index_SliceIndex_get : Self -> T -> result (option Output);
   core_slice_index_SliceIndex_get_mut :
     Self -> T -> result (option Output * (option Output -> T));
@@ -891,7 +887,6 @@ Record core_slice_index_SliceIndex (Self T Output : Type) := mk_core_slice_index
     Self -> T -> result (Output * (Output -> T));
 }.
 Arguments mk_core_slice_index_SliceIndex {_ _ _}.
-Arguments core_slice_index_SliceIndex_sealedInst {_ _ _}.
 Arguments core_slice_index_SliceIndex_get {_ _ _}.
 Arguments core_slice_index_SliceIndex_get_mut {_ _ _}.
 Arguments core_slice_index_SliceIndex_get_unchecked {_ _ _}.
@@ -958,14 +953,9 @@ Axiom core_array_Array_index_mut :
   (a : array T N) (i : Idx),
   result (Output * (Output -> array T N)).
 
-(* Trait implementation: [core::slice::index::private_slice_index::Range] *)
-Definition core_slice_index_private_slice_index_SealedRangeUsizeInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt.
-
 (* Trait implementation: [core::slice::index::Range] *)
 Definition core_slice_index_SliceIndexRangeUsizeSliceInst (T : Type) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) (slice T) := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst;
   core_slice_index_SliceIndex_get := core_slice_index_SliceIndexRangeUsizeSlice_get;
   core_slice_index_SliceIndex_get_mut := core_slice_index_SliceIndexRangeUsizeSlice_get_mut;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_SliceIndexRangeUsizeSlice_get_unchecked;
@@ -1026,14 +1016,9 @@ Axiom core_slice_index_usize_index : forall {T : Type}, usize -> slice T -> resu
 Axiom core_slice_index_usize_index_mut :
   forall {T : Type}, usize -> slice T -> result (T * (T -> slice T)).
 
-(* Trait implementation: [core::slice::index::private_slice_index::usize] *)
-Definition core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize := tt.
-
 (* Trait implementation: [core::slice::index::usize] *)
 Definition core_slice_index_SliceIndexUsizeSliceInst (T : Type) :
   core_slice_index_SliceIndex usize (slice T) T := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
   core_slice_index_SliceIndex_get := core_slice_index_usize_get;
   core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_usize_get_unchecked;
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index 2a651c2911..0c208dbfe2 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -804,12 +804,8 @@ let alloc_vec_Vec_push (#a  : Type0) (v : alloc_vec_Vec a) (x : a) :
 let alloc_vec_Vec_insert (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
   if i < length v then Ok (list_update v i x) else Fail Failure
 
-// Trait declaration: [core::slice::index::private_slice_index::Sealed]
-type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
-
 // Trait declaration: [core::slice::index::SliceIndex]
 noeq type core_slice_index_SliceIndex (self t output : Type0) = {
-  sealedInst : core_slice_index_private_slice_index_Sealed self;
   get : self → t → result (option output);
   get_mut : self → t → result (option output & (option output -> t));
   get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
@@ -882,14 +878,9 @@ let core_array_Array_index_mut
   result (out & (out -> array t n)) =
   admit () // TODO
 
-// Trait implementation: [core::slice::index::private_slice_index::Range]
-let core_slice_index_private_slice_index_SealedSliceIndexRangeUsizeSliceInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()
-
 // Trait implementation: [core::slice::index::Range]
 let core_slice_index_SliceIndexRangeUsizeSliceInst (t : Type0) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) (slice t) = {
-  sealedInst = core_slice_index_private_slice_index_SealedSliceIndexRangeUsizeSliceInst;
   get = core_slice_index_SliceIndexRangeUsizeSlice_get #t;
   get_mut = core_slice_index_SliceIndexRangeUsizeSlice_get_mut #t;
   get_unchecked = core_slice_index_SliceIndexRangeUsizeSlice_get_unchecked #t;
@@ -957,14 +948,9 @@ let core_slice_index_usize_index_mut (#t : Type0) :
   usize → slice t → result (t & (t -> slice t)) =
   admit () // TODO
 
-// Trait implementation: [core::slice::index::private_slice_index::usize]
-let core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize = ()
-
 // Trait implementation: [core::slice::index::usize]
 let core_slice_index_SliceIndexUsizeSliceInst (t : Type0) :
   core_slice_index_SliceIndex usize (slice t) t = {
-  sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
   get = core_slice_index_usize_get #t;
   get_mut = core_slice_index_usize_get_mut #t;
   get_unchecked = core_slice_index_usize_get_unchecked #t;
diff --git a/backends/lean/Aeneas/Std/Slice.lean b/backends/lean/Aeneas/Std/Slice.lean
index 16da42b2a3..5e0de5508e 100644
--- a/backends/lean/Aeneas/Std/Slice.lean
+++ b/backends/lean/Aeneas/Std/Slice.lean
@@ -334,12 +334,8 @@ theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (
 def core.slice.Slice.reverse {T : Type} (s : Slice T) : Slice T :=
   ⟨ s.val.reverse, by scalar_tac ⟩
 
-@[rust_trait "core::slice::index::private_slice_index::Sealed"]
-structure core.slice.index.private_slice_index.Sealed (Self : Type) where
-
-@[rust_trait "core::slice::index::SliceIndex" (parentClauses := ["sealedInst"])]
+@[rust_trait "core::slice::index::SliceIndex"]
 structure core.slice.index.SliceIndex (Self T Output : Type) where
-  sealedInst : core.slice.index.private_slice_index.Sealed Self
   get : Self → T → Result (Option Output)
   get_mut : Self → T → Result (Option Output × (Option Output → T))
   get_unchecked : Self → ConstRawPtr T → Result (ConstRawPtr Output)
@@ -431,14 +427,9 @@ def core.slice.index.Slice.index_mut
   (s : Slice T) (i : I) : Result (Output × (Output → Slice T)) :=
   inst.index_mut i s
 
-@[rust_trait_impl "core::slice::index::private_slice_index::Sealed<core::ops::range::Range<usize>>"]
-def core.slice.index.private_slice_index.SealedRangeUsize
-  : core.slice.index.private_slice_index.Sealed (Range Usize) := {}
-
 @[reducible, rust_trait_impl "core::slice::index::SliceIndex<core::ops::range::Range<usize>, [@T], [@T]>"]
 def core.slice.index.SliceIndexRangeUsizeSlice (T : Type) :
   core.slice.index.SliceIndex (Range Usize) (Slice T) (Slice T) := {
-  sealedInst := core.slice.index.private_slice_index.SealedRangeUsize
   get := core.slice.index.SliceIndexRangeUsizeSlice.get
   get_mut := core.slice.index.SliceIndexRangeUsizeSlice.get_mut
   get_unchecked := core.slice.index.SliceIndexRangeUsizeSlice.get_unchecked
@@ -447,11 +438,6 @@ def core.slice.index.SliceIndexRangeUsizeSlice (T : Type) :
   index_mut := core.slice.index.SliceIndexRangeUsizeSlice.index_mut
 }
 
-@[reducible, rust_trait_impl "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeTo<usize>>"]
-def core.slice.index.private_slice_index.SealedRangeToUsize :
-  core.slice.index.private_slice_index.Sealed (core.ops.range.RangeTo Usize)
-  := {}
-
 @[rust_fun "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeTo<usize>, [@T], [@T]>}::get"]
 def core.slice.index.SliceIndexRangeToUsizeSlice.get
   {T : Type} (r : core.ops.range.RangeTo Usize) (s : Slice T) : Result (Option (Slice T)) :=
@@ -511,7 +497,6 @@ def core.slice.index.SliceIndexRangeToUsizeSlice.index_mut
 def core.slice.index.SliceIndexRangeToUsizeSlice (T : Type) :
   core.slice.index.SliceIndex (core.ops.range.RangeTo Usize) (Slice T) (Slice
   T) := {
-  sealedInst := core.slice.index.private_slice_index.SealedRangeToUsize
   get := core.slice.index.SliceIndexRangeToUsizeSlice.get
   get_mut := core.slice.index.SliceIndexRangeToUsizeSlice.get_mut
   get_unchecked := core.slice.index.SliceIndexRangeToUsizeSlice.get_unchecked
@@ -566,14 +551,9 @@ abbrev core.slice.index.Usize.index_mut {T : Type}
   (i : Usize) (s : Slice T) : Result (T × (T → (Slice T))) :=
   Slice.index_mut_usize s i
 
-@[rust_trait_impl "core::slice::index::private_slice_index::Sealed<usize>"]
-def core.slice.index.private_slice_index.SealedUsize
-  : core.slice.index.private_slice_index.Sealed Usize := {}
-
 @[reducible, rust_trait_impl "core::slice::index::SliceIndex<usize, [@T], @T>"]
 def core.slice.index.SliceIndexUsizeSlice (T : Type) :
   core.slice.index.SliceIndex Usize (Slice T) T := {
-  sealedInst := core.slice.index.private_slice_index.SealedUsize
   get := core.slice.index.Usize.get
   get_mut := core.slice.index.Usize.get_mut
   get_unchecked := core.slice.index.Usize.get_unchecked
@@ -655,16 +635,9 @@ theorem _SliceIndexRangeFromUsizeSlice.index_mut.test {T} (s : Slice T) (r : cor
   unfold core.slice.index.SliceIndexRangeFromUsizeSlice.index_mut
   simp [h]
 
-@[reducible, rust_trait_impl "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeFrom<usize>>"]
-def core.slice.index.private_slice_index.SealedRangeFromUsize :
-  core.slice.index.private_slice_index.Sealed (core.ops.range.RangeFrom Usize)
-  := {}
-
 @[reducible, rust_trait_impl "core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, [@T], [@T]>"]
 def core.slice.index.SliceIndexRangeFromUsizeSlice (T : Type) :
   core.slice.index.SliceIndex (core.ops.range.RangeFrom Usize) (Slice T) (Slice T) := {
-  sealedInst :=
-    core.slice.index.private_slice_index.SealedRangeFromUsize
   get := core.slice.index.SliceIndexRangeFromUsizeSlice.get
   get_mut := core.slice.index.SliceIndexRangeFromUsizeSlice.get_mut
   get_unchecked :=
diff --git a/charon-pin b/charon-pin
index dba00c2385..1d22f7f397 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.
-f5208b1c4ce287898a1fc015d41a20da3baf0974
+f5a61c8f2cb695213b427ab696f8088f357b5dea
diff --git a/flake.lock b/flake.lock
index b4720a3b0c..2ac414fd97 100644
--- a/flake.lock
+++ b/flake.lock
@@ -10,11 +10,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1787154936,
-        "narHash": "sha256-5NgTm1FpGhBRQOAUquBSaI1yZybqh5lCAcbGo/QBtE8=",
+        "lastModified": 1787216897,
+        "narHash": "sha256-2TiYoZ7v71EJ8Kx6/5cxOmlykNE/63Yp+TdsdpXRcF4=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "f5208b1c4ce287898a1fc015d41a20da3baf0974",
+        "rev": "f5a61c8f2cb695213b427ab696f8088f357b5dea",
         "type": "github"
       },
       "original": {
@@ -186,17 +186,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1780284119,
-        "narHash": "sha256-y2wR4Mk6D/N1ID4FZa2oUMStCUxyIoRzmgOOpLzoWmo=",
+        "lastModified": 1787022047,
+        "narHash": "sha256-wNlYM/obKOkkRELrOfto1JT5CRANR6hB/RjOELp223U=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "51390d0bfca0a68a8c337d215a4bbeddc2ca616e",
+        "rev": "b32685dd7c5a965aa8273adb7ddaf7f5b40d0faa",
         "type": "github"
       },
       "original": {
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "51390d0bfca0a68a8c337d215a4bbeddc2ca616e",
+        "rev": "b32685dd7c5a965aa8273adb7ddaf7f5b40d0faa",
         "type": "github"
       }
     },
diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml
index 6e28b984b6..e462aaa680 100644
--- a/src/extract/ExtractBuiltin.ml
+++ b/src/extract/ExtractBuiltin.ml
@@ -299,11 +299,8 @@ let builtin_trait_decls_info () =
       (* IndexMut *)
       mk_trait "core::ops::index::IndexMut" ~parent_clauses:[ "indexInst" ]
         ~methods:[ "index_mut" ] ();
-      (* Sealed *)
-      mk_trait "core::slice::index::private_slice_index::Sealed" ();
       (* SliceIndex *)
-      mk_trait "core::slice::index::SliceIndex" ~parent_clauses:[ "sealedInst" ]
-        ~types:[ "Output" ]
+      mk_trait "core::slice::index::SliceIndex" ~types:[ "Output" ]
         ~methods:
           [
             "get";
@@ -374,11 +371,6 @@ let builtin_trait_impls_info () : (pattern * Pure.builtin_trait_impl_info) list
       (* core::ops::index::IndexMut<[T], I> *)
       fmt "core::ops::index::IndexMut<[@T], @I, @O>"
         ~extract_name:(Some "core::ops::index::IndexMutSliceInst") ();
-      (* core::slice::index::private_slice_index::Sealed<Range<usize>> *)
-      fmt
-        "core::slice::index::private_slice_index::Sealed<core::ops::range::Range<usize>>"
-        ~extract_name:
-          (Some "core.slice.index.private_slice_index.SealedRangeUsizeInst") ();
       (* core::slice::index::SliceIndex<Range<usize>, [T]> *)
       fmt
         "core::slice::index::SliceIndex<core::ops::range::Range<usize>, [@T], \
@@ -391,10 +383,6 @@ let builtin_trait_impls_info () : (pattern * Pure.builtin_trait_impl_info) list
       (* core::ops::index::IndexMut<[T; N], I> *)
       fmt "core::ops::index::IndexMut<[@T; @N], @I, @O>"
         ~extract_name:(Some "core::ops::index::IndexMutArrayInst") ();
-      (* core::slice::index::private_slice_index::Sealed<usize> *)
-      fmt "core::slice::index::private_slice_index::Sealed<usize>"
-        ~extract_name:
-          (Some "core::slice::index::private_slice_index::SealedUsizeInst") ();
       (* core::slice::index::SliceIndex<usize, [T]> *)
       fmt "core::slice::index::SliceIndex<usize, [@T], @T>"
         ~extract_name:(Some "core::slice::index::SliceIndexUsizeSliceInst") ();
diff --git a/src/extract/ExtractBuiltinLean.ml b/src/extract/ExtractBuiltinLean.ml
index b26ba71365..4b02e2d3b1 100644
--- a/src/extract/ExtractBuiltinLean.ml
+++ b/src/extract/ExtractBuiltinLean.ml
@@ -926,130 +926,130 @@ let lean_builtin_funs =
     (* file: "Aeneas/Std/Array/ArraySlice.lean", line: 221 *)
     mk_fun "core::slice::cmp::{core::cmp::PartialEq<[@T], [@U]>}::ne"
       "core.slice.cmp.PartialEqSlice.ne";
-    (* file: "Aeneas/Std/Slice.lean", line: 350 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 346 *)
     mk_fun "core::slice::index::{core::ops::index::Index<[@T], @I, @O>}::index"
       "core.slice.index.Slice.index";
-    (* file: "Aeneas/Std/Slice.lean", line: 428 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 424 *)
     mk_fun
       "core::slice::index::{core::ops::index::IndexMut<[@T], @I, \
        @O>}::index_mut"
       "core.slice.index.Slice.index_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 376 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 372 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T], [@T]>}::get"
       "core.slice.index.SliceIndexRangeUsizeSlice.get";
-    (* file: "Aeneas/Std/Slice.lean", line: 383 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 379 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T], [@T]>}::get_mut"
       "core.slice.index.SliceIndexRangeUsizeSlice.get_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 397 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 393 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T], [@T]>}::get_unchecked"
       "core.slice.index.SliceIndexRangeUsizeSlice.get_unchecked";
-    (* file: "Aeneas/Std/Slice.lean", line: 403 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 399 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T], [@T]>}::get_unchecked_mut"
       "core.slice.index.SliceIndexRangeUsizeSlice.get_unchecked_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 409 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 405 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T], [@T]>}::index"
       "core.slice.index.SliceIndexRangeUsizeSlice.index";
-    (* file: "Aeneas/Std/Slice.lean", line: 415 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 411 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T], [@T]>}::index_mut"
       "core.slice.index.SliceIndexRangeUsizeSlice.index_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 598 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 578 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
        [@T], [@T]>}::get"
       "core.slice.index.SliceIndexRangeFromUsizeSlice.get";
-    (* file: "Aeneas/Std/Slice.lean", line: 604 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 584 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
        [@T], [@T]>}::get_mut"
       "core.slice.index.SliceIndexRangeFromUsizeSlice.get_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 618 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 598 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
        [@T], [@T]>}::get_unchecked"
       "core.slice.index.SliceIndexRangeFromUsizeSlice.get_unchecked";
-    (* file: "Aeneas/Std/Slice.lean", line: 624 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 604 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
        [@T], [@T]>}::get_unchecked_mut"
       "core.slice.index.SliceIndexRangeFromUsizeSlice.get_unchecked_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 630 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 610 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
        [@T], [@T]>}::index"
       "core.slice.index.SliceIndexRangeFromUsizeSlice.index";
-    (* file: "Aeneas/Std/Slice.lean", line: 637 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 617 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
        [@T], [@T]>}::index_mut"
       "core.slice.index.SliceIndexRangeFromUsizeSlice.index_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 455 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 441 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeTo<usize>, \
        [@T], [@T]>}::get"
       "core.slice.index.SliceIndexRangeToUsizeSlice.get";
-    (* file: "Aeneas/Std/Slice.lean", line: 462 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 448 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeTo<usize>, \
        [@T], [@T]>}::get_mut"
       "core.slice.index.SliceIndexRangeToUsizeSlice.get_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 477 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 463 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeTo<usize>, \
        [@T], [@T]>}::get_unchecked"
       "core.slice.index.SliceIndexRangeToUsizeSlice.get_unchecked";
-    (* file: "Aeneas/Std/Slice.lean", line: 483 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 469 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeTo<usize>, \
        [@T], [@T]>}::get_unchecked_mut"
       "core.slice.index.SliceIndexRangeToUsizeSlice.get_unchecked_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 490 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 476 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeTo<usize>, \
        [@T], [@T]>}::index"
       "core.slice.index.SliceIndexRangeToUsizeSlice.index";
-    (* file: "Aeneas/Std/Slice.lean", line: 497 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 483 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeTo<usize>, \
        [@T], [@T]>}::index_mut"
       "core.slice.index.SliceIndexRangeToUsizeSlice.index_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 538 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 523 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, [@T], \
        @T>}::get"
       "core.slice.index.Usize.get";
-    (* file: "Aeneas/Std/Slice.lean", line: 543 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 528 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, [@T], \
        @T>}::get_mut"
       "core.slice.index.Usize.get_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 548 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 533 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, [@T], \
        @T>}::get_unchecked"
       "core.slice.index.Usize.get_unchecked";
-    (* file: "Aeneas/Std/Slice.lean", line: 554 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 539 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, [@T], \
        @T>}::get_unchecked_mut"
       "core.slice.index.Usize.get_unchecked_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 560 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 545 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, [@T], \
        @T>}::index"
       "core.slice.index.Usize.index";
-    (* file: "Aeneas/Std/Slice.lean", line: 564 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 549 *)
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, [@T], \
        @T>}::index_mut"
@@ -1082,16 +1082,16 @@ let lean_builtin_funs =
     mk_fun "core::slice::{[@T]}::chunks_exact" "core.slice.Slice.chunks_exact";
     (* file: "Aeneas/Std/SliceIter.lean", line: 31 *)
     mk_fun "core::slice::{[@T]}::contains" "core.slice.Slice.contains";
-    (* file: "Aeneas/Std/Slice.lean", line: 592 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 572 *)
     mk_fun "core::slice::{[@T]}::copy_from_slice"
       "core.slice.Slice.copy_from_slice";
-    (* file: "Aeneas/Std/Slice.lean", line: 1057 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 1030 *)
     mk_fun "core::slice::{[@T]}::fill" "core.slice.Slice.fill";
-    (* file: "Aeneas/Std/Slice.lean", line: 356 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 352 *)
     mk_fun "core::slice::{[@T]}::get" "core.slice.Slice.get";
-    (* file: "Aeneas/Std/Slice.lean", line: 370 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 366 *)
     mk_fun "core::slice::{[@T]}::get_mut" "core.slice.Slice.get_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 362 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 358 *)
     mk_fun "core::slice::{[@T]}::get_unchecked" "core.slice.Slice.get_unchecked";
     (* file: "Aeneas/Std/Slice.lean", line: 123 *)
     mk_fun "core::slice::{[@T]}::is_empty" "core.slice.Slice.is_empty";
@@ -1104,11 +1104,11 @@ let lean_builtin_funs =
     (* file: "Aeneas/Std/Slice.lean", line: 333 *)
     mk_fun "core::slice::{[@T]}::reverse" "core.slice.Slice.reverse"
       ~can_fail:false;
-    (* file: "Aeneas/Std/Slice.lean", line: 701 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 674 *)
     mk_fun "core::slice::{[@T]}::split_at" "core.slice.Slice.split_at";
-    (* file: "Aeneas/Std/Slice.lean", line: 712 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 685 *)
     mk_fun "core::slice::{[@T]}::split_at_mut" "core.slice.Slice.split_at_mut";
-    (* file: "Aeneas/Std/Slice.lean", line: 772 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 745 *)
     mk_fun "core::slice::{[@T]}::swap" "core.slice.Slice.swap";
     (* file: "Aeneas/Std/StringIter.lean", line: 14 *)
     mk_fun
@@ -1311,9 +1311,8 @@ let lean_builtin_trait_decls =
     mk_trait_decl "core::ops::try_trait::Try" "core.ops.try_trait.Try"
       ~parent_clauses:[ "FromResidualInst" ]
       ~methods:[ ("from_output", "from_output"); ("branch", "branch") ];
-    (* file: "Aeneas/Std/Slice.lean", line: 340 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 337 *)
     mk_trait_decl "core::slice::index::SliceIndex" "core.slice.index.SliceIndex"
-      ~parent_clauses:[ "sealedInst" ]
       ~methods:
         [
           ("get", "get");
@@ -1323,9 +1322,6 @@ let lean_builtin_trait_decls =
           ("index", "index");
           ("index_mut", "index_mut");
         ];
-    (* file: "Aeneas/Std/Slice.lean", line: 337 *)
-    mk_trait_decl "core::slice::index::private_slice_index::Sealed"
-      "core.slice.index.private_slice_index.Sealed";
   ]
 
 let lean_builtin_trait_impls =
@@ -1554,7 +1550,7 @@ let lean_builtin_trait_impls =
     (* file: "Aeneas/Std/Array/ArraySlice.lean", line: 108 *)
     mk_trait_impl "core::ops::index::Index<[@T; @N], @I, @O>"
       "core.ops.index.IndexArray";
-    (* file: "Aeneas/Std/Slice.lean", line: 523 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 508 *)
     mk_trait_impl "core::ops::index::Index<[@T], @I, @O>"
       "core.ops.index.IndexSlice";
     (* file: "Aeneas/Std/Vec.lean", line: 209 *)
@@ -1564,44 +1560,29 @@ let lean_builtin_trait_impls =
     (* file: "Aeneas/Std/Array/ArraySlice.lean", line: 115 *)
     mk_trait_impl "core::ops::index::IndexMut<[@T; @N], @I, @O>"
       "core.ops.index.IndexMutArray";
-    (* file: "Aeneas/Std/Slice.lean", line: 530 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 515 *)
     mk_trait_impl "core::ops::index::IndexMut<[@T], @I, @O>"
       "core.ops.index.IndexMutSlice";
     (* file: "Aeneas/Std/Vec.lean", line: 217 *)
     mk_trait_impl "core::ops::index::IndexMut<alloc::vec::Vec<@T>, @T, @O>"
       "alloc.vec.Vec.IndexMut"
       ~keep_params:(Some [ true; true; false; true ]);
-    (* file: "Aeneas/Std/Slice.lean", line: 438 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 430 *)
     mk_trait_impl
       "core::slice::index::SliceIndex<core::ops::range::Range<usize>, [@T], \
        [@T]>"
       "core.slice.index.SliceIndexRangeUsizeSlice";
-    (* file: "Aeneas/Std/Slice.lean", line: 663 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 638 *)
     mk_trait_impl
       "core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
        [@T], [@T]>"
       "core.slice.index.SliceIndexRangeFromUsizeSlice";
-    (* file: "Aeneas/Std/Slice.lean", line: 510 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 496 *)
     mk_trait_impl
       "core::slice::index::SliceIndex<core::ops::range::RangeTo<usize>, [@T], \
        [@T]>"
       "core.slice.index.SliceIndexRangeToUsizeSlice";
-    (* file: "Aeneas/Std/Slice.lean", line: 573 *)
+    (* file: "Aeneas/Std/Slice.lean", line: 554 *)
     mk_trait_impl "core::slice::index::SliceIndex<usize, [@T], @T>"
       "core.slice.index.SliceIndexUsizeSlice";
-    (* file: "Aeneas/Std/Slice.lean", line: 434 *)
-    mk_trait_impl
-      "core::slice::index::private_slice_index::Sealed<core::ops::range::Range<usize>>"
-      "core.slice.index.private_slice_index.SealedRangeUsize";
-    (* file: "Aeneas/Std/Slice.lean", line: 658 *)
-    mk_trait_impl
-      "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeFrom<usize>>"
-      "core.slice.index.private_slice_index.SealedRangeFromUsize";
-    (* file: "Aeneas/Std/Slice.lean", line: 450 *)
-    mk_trait_impl
-      "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeTo<usize>>"
-      "core.slice.index.private_slice_index.SealedRangeToUsize";
-    (* file: "Aeneas/Std/Slice.lean", line: 569 *)
-    mk_trait_impl "core::slice::index::private_slice_index::Sealed<usize>"
-      "core.slice.index.private_slice_index.SealedUsize";
   ]
diff --git a/tests/coq/arrays/Primitives.v b/tests/coq/arrays/Primitives.v
index 48fde64e14..fcc56570e4 100644
--- a/tests/coq/arrays/Primitives.v
+++ b/tests/coq/arrays/Primitives.v
@@ -875,12 +875,8 @@ Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usi
   | Fail_ e => Fail_ e
   end.
 
-(* Trait declaration: [core::slice::index::private_slice_index::Sealed] *)
-Definition core_slice_index_private_slice_index_Sealed (self : Type) := unit.
-
 (* Trait declaration: [core::slice::index::SliceIndex] *)
 Record core_slice_index_SliceIndex (Self T Output : Type) := mk_core_slice_index_SliceIndex {
-  core_slice_index_SliceIndex_sealedInst : core_slice_index_private_slice_index_Sealed Self;
   core_slice_index_SliceIndex_get : Self -> T -> result (option Output);
   core_slice_index_SliceIndex_get_mut :
     Self -> T -> result (option Output * (option Output -> T));
@@ -891,7 +887,6 @@ Record core_slice_index_SliceIndex (Self T Output : Type) := mk_core_slice_index
     Self -> T -> result (Output * (Output -> T));
 }.
 Arguments mk_core_slice_index_SliceIndex {_ _ _}.
-Arguments core_slice_index_SliceIndex_sealedInst {_ _ _}.
 Arguments core_slice_index_SliceIndex_get {_ _ _}.
 Arguments core_slice_index_SliceIndex_get_mut {_ _ _}.
 Arguments core_slice_index_SliceIndex_get_unchecked {_ _ _}.
@@ -958,14 +953,9 @@ Axiom core_array_Array_index_mut :
   (a : array T N) (i : Idx),
   result (Output * (Output -> array T N)).
 
-(* Trait implementation: [core::slice::index::private_slice_index::Range] *)
-Definition core_slice_index_private_slice_index_SealedRangeUsizeInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt.
-
 (* Trait implementation: [core::slice::index::Range] *)
 Definition core_slice_index_SliceIndexRangeUsizeSliceInst (T : Type) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) (slice T) := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst;
   core_slice_index_SliceIndex_get := core_slice_index_SliceIndexRangeUsizeSlice_get;
   core_slice_index_SliceIndex_get_mut := core_slice_index_SliceIndexRangeUsizeSlice_get_mut;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_SliceIndexRangeUsizeSlice_get_unchecked;
@@ -1026,14 +1016,9 @@ Axiom core_slice_index_usize_index : forall {T : Type}, usize -> slice T -> resu
 Axiom core_slice_index_usize_index_mut :
   forall {T : Type}, usize -> slice T -> result (T * (T -> slice T)).
 
-(* Trait implementation: [core::slice::index::private_slice_index::usize] *)
-Definition core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize := tt.
-
 (* Trait implementation: [core::slice::index::usize] *)
 Definition core_slice_index_SliceIndexUsizeSliceInst (T : Type) :
   core_slice_index_SliceIndex usize (slice T) T := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
   core_slice_index_SliceIndex_get := core_slice_index_usize_get;
   core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_usize_get_unchecked;
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index ac8debe2c1..aef6a1b2ec 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 2583:8-2583:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2651:8-2651: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 2620:8-2620:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2688:8-2688: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/demo/Primitives.v b/tests/coq/demo/Primitives.v
index 48fde64e14..fcc56570e4 100644
--- a/tests/coq/demo/Primitives.v
+++ b/tests/coq/demo/Primitives.v
@@ -875,12 +875,8 @@ Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usi
   | Fail_ e => Fail_ e
   end.
 
-(* Trait declaration: [core::slice::index::private_slice_index::Sealed] *)
-Definition core_slice_index_private_slice_index_Sealed (self : Type) := unit.
-
 (* Trait declaration: [core::slice::index::SliceIndex] *)
 Record core_slice_index_SliceIndex (Self T Output : Type) := mk_core_slice_index_SliceIndex {
-  core_slice_index_SliceIndex_sealedInst : core_slice_index_private_slice_index_Sealed Self;
   core_slice_index_SliceIndex_get : Self -> T -> result (option Output);
   core_slice_index_SliceIndex_get_mut :
     Self -> T -> result (option Output * (option Output -> T));
@@ -891,7 +887,6 @@ Record core_slice_index_SliceIndex (Self T Output : Type) := mk_core_slice_index
     Self -> T -> result (Output * (Output -> T));
 }.
 Arguments mk_core_slice_index_SliceIndex {_ _ _}.
-Arguments core_slice_index_SliceIndex_sealedInst {_ _ _}.
 Arguments core_slice_index_SliceIndex_get {_ _ _}.
 Arguments core_slice_index_SliceIndex_get_mut {_ _ _}.
 Arguments core_slice_index_SliceIndex_get_unchecked {_ _ _}.
@@ -958,14 +953,9 @@ Axiom core_array_Array_index_mut :
   (a : array T N) (i : Idx),
   result (Output * (Output -> array T N)).
 
-(* Trait implementation: [core::slice::index::private_slice_index::Range] *)
-Definition core_slice_index_private_slice_index_SealedRangeUsizeInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt.
-
 (* Trait implementation: [core::slice::index::Range] *)
 Definition core_slice_index_SliceIndexRangeUsizeSliceInst (T : Type) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) (slice T) := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst;
   core_slice_index_SliceIndex_get := core_slice_index_SliceIndexRangeUsizeSlice_get;
   core_slice_index_SliceIndex_get_mut := core_slice_index_SliceIndexRangeUsizeSlice_get_mut;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_SliceIndexRangeUsizeSlice_get_unchecked;
@@ -1026,14 +1016,9 @@ Axiom core_slice_index_usize_index : forall {T : Type}, usize -> slice T -> resu
 Axiom core_slice_index_usize_index_mut :
   forall {T : Type}, usize -> slice T -> result (T * (T -> slice T)).
 
-(* Trait implementation: [core::slice::index::private_slice_index::usize] *)
-Definition core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize := tt.
-
 (* Trait implementation: [core::slice::index::usize] *)
 Definition core_slice_index_SliceIndexUsizeSliceInst (T : Type) :
   core_slice_index_SliceIndex usize (slice T) T := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
   core_slice_index_SliceIndex_get := core_slice_index_usize_get;
   core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_usize_get_unchecked;
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index 48fde64e14..fcc56570e4 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -875,12 +875,8 @@ Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usi
   | Fail_ e => Fail_ e
   end.
 
-(* Trait declaration: [core::slice::index::private_slice_index::Sealed] *)
-Definition core_slice_index_private_slice_index_Sealed (self : Type) := unit.
-
 (* Trait declaration: [core::slice::index::SliceIndex] *)
 Record core_slice_index_SliceIndex (Self T Output : Type) := mk_core_slice_index_SliceIndex {
-  core_slice_index_SliceIndex_sealedInst : core_slice_index_private_slice_index_Sealed Self;
   core_slice_index_SliceIndex_get : Self -> T -> result (option Output);
   core_slice_index_SliceIndex_get_mut :
     Self -> T -> result (option Output * (option Output -> T));
@@ -891,7 +887,6 @@ Record core_slice_index_SliceIndex (Self T Output : Type) := mk_core_slice_index
     Self -> T -> result (Output * (Output -> T));
 }.
 Arguments mk_core_slice_index_SliceIndex {_ _ _}.
-Arguments core_slice_index_SliceIndex_sealedInst {_ _ _}.
 Arguments core_slice_index_SliceIndex_get {_ _ _}.
 Arguments core_slice_index_SliceIndex_get_mut {_ _ _}.
 Arguments core_slice_index_SliceIndex_get_unchecked {_ _ _}.
@@ -958,14 +953,9 @@ Axiom core_array_Array_index_mut :
   (a : array T N) (i : Idx),
   result (Output * (Output -> array T N)).
 
-(* Trait implementation: [core::slice::index::private_slice_index::Range] *)
-Definition core_slice_index_private_slice_index_SealedRangeUsizeInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt.
-
 (* Trait implementation: [core::slice::index::Range] *)
 Definition core_slice_index_SliceIndexRangeUsizeSliceInst (T : Type) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) (slice T) := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst;
   core_slice_index_SliceIndex_get := core_slice_index_SliceIndexRangeUsizeSlice_get;
   core_slice_index_SliceIndex_get_mut := core_slice_index_SliceIndexRangeUsizeSlice_get_mut;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_SliceIndexRangeUsizeSlice_get_unchecked;
@@ -1026,14 +1016,9 @@ Axiom core_slice_index_usize_index : forall {T : Type}, usize -> slice T -> resu
 Axiom core_slice_index_usize_index_mut :
   forall {T : Type}, usize -> slice T -> result (T * (T -> slice T)).
 
-(* Trait implementation: [core::slice::index::private_slice_index::usize] *)
-Definition core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize := tt.
-
 (* Trait implementation: [core::slice::index::usize] *)
 Definition core_slice_index_SliceIndexUsizeSliceInst (T : Type) :
   core_slice_index_SliceIndex usize (slice T) T := {|
-  core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
   core_slice_index_SliceIndex_get := core_slice_index_usize_get;
   core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut;
   core_slice_index_SliceIndex_get_unchecked := core_slice_index_usize_get_unchecked;
diff --git a/tests/coq/misc/Traits.v b/tests/coq/misc/Traits.v
index 9476ce9070..a4df22ba17 100644
--- a/tests/coq/misc/Traits.v
+++ b/tests/coq/misc/Traits.v
@@ -9,7 +9,7 @@ Local Open Scope Primitives_scope.
 Module Traits.
 
 (** [core::result::Result]
-    Source: '/rustc/library/core/src/result.rs', lines 557:0-557:21
+    Source: '/rustc/library/core/src/result.rs', lines 558:0-558:21
     Name pattern: [core::result::Result]
     Visibility: public *)
 Inductive core_result_Result_t (T : Type) (E : Type) :=
diff --git a/tests/fstar/arrays/Primitives.fst b/tests/fstar/arrays/Primitives.fst
index 2a651c2911..0c208dbfe2 100644
--- a/tests/fstar/arrays/Primitives.fst
+++ b/tests/fstar/arrays/Primitives.fst
@@ -804,12 +804,8 @@ let alloc_vec_Vec_push (#a  : Type0) (v : alloc_vec_Vec a) (x : a) :
 let alloc_vec_Vec_insert (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
   if i < length v then Ok (list_update v i x) else Fail Failure
 
-// Trait declaration: [core::slice::index::private_slice_index::Sealed]
-type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
-
 // Trait declaration: [core::slice::index::SliceIndex]
 noeq type core_slice_index_SliceIndex (self t output : Type0) = {
-  sealedInst : core_slice_index_private_slice_index_Sealed self;
   get : self → t → result (option output);
   get_mut : self → t → result (option output & (option output -> t));
   get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
@@ -882,14 +878,9 @@ let core_array_Array_index_mut
   result (out & (out -> array t n)) =
   admit () // TODO
 
-// Trait implementation: [core::slice::index::private_slice_index::Range]
-let core_slice_index_private_slice_index_SealedSliceIndexRangeUsizeSliceInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()
-
 // Trait implementation: [core::slice::index::Range]
 let core_slice_index_SliceIndexRangeUsizeSliceInst (t : Type0) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) (slice t) = {
-  sealedInst = core_slice_index_private_slice_index_SealedSliceIndexRangeUsizeSliceInst;
   get = core_slice_index_SliceIndexRangeUsizeSlice_get #t;
   get_mut = core_slice_index_SliceIndexRangeUsizeSlice_get_mut #t;
   get_unchecked = core_slice_index_SliceIndexRangeUsizeSlice_get_unchecked #t;
@@ -957,14 +948,9 @@ let core_slice_index_usize_index_mut (#t : Type0) :
   usize → slice t → result (t & (t -> slice t)) =
   admit () // TODO
 
-// Trait implementation: [core::slice::index::private_slice_index::usize]
-let core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize = ()
-
 // Trait implementation: [core::slice::index::usize]
 let core_slice_index_SliceIndexUsizeSliceInst (t : Type0) :
   core_slice_index_SliceIndex usize (slice t) t = {
-  sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
   get = core_slice_index_usize_get #t;
   get_mut = core_slice_index_usize_get_mut #t;
   get_unchecked = core_slice_index_usize_get_unchecked #t;
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index f7ff392760..adc103f860 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 2583:8-2583:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2651:8-2651: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 2620:8-2620:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2688:8-2688: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/demo/Primitives.fst b/tests/fstar/demo/Primitives.fst
index 2a651c2911..0c208dbfe2 100644
--- a/tests/fstar/demo/Primitives.fst
+++ b/tests/fstar/demo/Primitives.fst
@@ -804,12 +804,8 @@ let alloc_vec_Vec_push (#a  : Type0) (v : alloc_vec_Vec a) (x : a) :
 let alloc_vec_Vec_insert (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
   if i < length v then Ok (list_update v i x) else Fail Failure
 
-// Trait declaration: [core::slice::index::private_slice_index::Sealed]
-type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
-
 // Trait declaration: [core::slice::index::SliceIndex]
 noeq type core_slice_index_SliceIndex (self t output : Type0) = {
-  sealedInst : core_slice_index_private_slice_index_Sealed self;
   get : self → t → result (option output);
   get_mut : self → t → result (option output & (option output -> t));
   get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
@@ -882,14 +878,9 @@ let core_array_Array_index_mut
   result (out & (out -> array t n)) =
   admit () // TODO
 
-// Trait implementation: [core::slice::index::private_slice_index::Range]
-let core_slice_index_private_slice_index_SealedSliceIndexRangeUsizeSliceInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()
-
 // Trait implementation: [core::slice::index::Range]
 let core_slice_index_SliceIndexRangeUsizeSliceInst (t : Type0) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) (slice t) = {
-  sealedInst = core_slice_index_private_slice_index_SealedSliceIndexRangeUsizeSliceInst;
   get = core_slice_index_SliceIndexRangeUsizeSlice_get #t;
   get_mut = core_slice_index_SliceIndexRangeUsizeSlice_get_mut #t;
   get_unchecked = core_slice_index_SliceIndexRangeUsizeSlice_get_unchecked #t;
@@ -957,14 +948,9 @@ let core_slice_index_usize_index_mut (#t : Type0) :
   usize → slice t → result (t & (t -> slice t)) =
   admit () // TODO
 
-// Trait implementation: [core::slice::index::private_slice_index::usize]
-let core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize = ()
-
 // Trait implementation: [core::slice::index::usize]
 let core_slice_index_SliceIndexUsizeSliceInst (t : Type0) :
   core_slice_index_SliceIndex usize (slice t) t = {
-  sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
   get = core_slice_index_usize_get #t;
   get_mut = core_slice_index_usize_get_mut #t;
   get_unchecked = core_slice_index_usize_get_unchecked #t;
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index 2a651c2911..0c208dbfe2 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -804,12 +804,8 @@ let alloc_vec_Vec_push (#a  : Type0) (v : alloc_vec_Vec a) (x : a) :
 let alloc_vec_Vec_insert (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
   if i < length v then Ok (list_update v i x) else Fail Failure
 
-// Trait declaration: [core::slice::index::private_slice_index::Sealed]
-type core_slice_index_private_slice_index_Sealed (self : Type0) = unit
-
 // Trait declaration: [core::slice::index::SliceIndex]
 noeq type core_slice_index_SliceIndex (self t output : Type0) = {
-  sealedInst : core_slice_index_private_slice_index_Sealed self;
   get : self → t → result (option output);
   get_mut : self → t → result (option output & (option output -> t));
   get_unchecked : self → const_raw_ptr t → result (const_raw_ptr output);
@@ -882,14 +878,9 @@ let core_array_Array_index_mut
   result (out & (out -> array t n)) =
   admit () // TODO
 
-// Trait implementation: [core::slice::index::private_slice_index::Range]
-let core_slice_index_private_slice_index_SealedSliceIndexRangeUsizeSliceInst
-  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()
-
 // Trait implementation: [core::slice::index::Range]
 let core_slice_index_SliceIndexRangeUsizeSliceInst (t : Type0) :
   core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) (slice t) = {
-  sealedInst = core_slice_index_private_slice_index_SealedSliceIndexRangeUsizeSliceInst;
   get = core_slice_index_SliceIndexRangeUsizeSlice_get #t;
   get_mut = core_slice_index_SliceIndexRangeUsizeSlice_get_mut #t;
   get_unchecked = core_slice_index_SliceIndexRangeUsizeSlice_get_unchecked #t;
@@ -957,14 +948,9 @@ let core_slice_index_usize_index_mut (#t : Type0) :
   usize → slice t → result (t & (t -> slice t)) =
   admit () // TODO
 
-// Trait implementation: [core::slice::index::private_slice_index::usize]
-let core_slice_index_private_slice_index_SealedUsizeInst
-  : core_slice_index_private_slice_index_Sealed usize = ()
-
 // Trait implementation: [core::slice::index::usize]
 let core_slice_index_SliceIndexUsizeSliceInst (t : Type0) :
   core_slice_index_SliceIndex usize (slice t) t = {
-  sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
   get = core_slice_index_usize_get #t;
   get_mut = core_slice_index_usize_get_mut #t;
   get_unchecked = core_slice_index_usize_get_unchecked #t;
diff --git a/tests/fstar/misc/Traits.fst b/tests/fstar/misc/Traits.fst
index 63de8b1eb3..bf333f9015 100644
--- a/tests/fstar/misc/Traits.fst
+++ b/tests/fstar/misc/Traits.fst
@@ -6,7 +6,7 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::result::Result]
-    Source: '/rustc/library/core/src/result.rs', lines 557:0-557:21
+    Source: '/rustc/library/core/src/result.rs', lines 558:0-558:21
     Name pattern: [core::result::Result]
     Visibility: public *)
 type core_result_Result_t (t : Type0) (e : Type0) =
diff --git a/tests/lean/AssertCfg.lean b/tests/lean/AssertCfg.lean
index 06bfb83fd2..2446a11e5e 100644
--- a/tests/lean/AssertCfg.lean
+++ b/tests/lean/AssertCfg.lean
@@ -12,8 +12,29 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace assert_cfg
 
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
 /-- [assert_cfg::get_b0]:
     Source: 'tests/src/assert-cfg.rs', lines 3:0-5:1 -/
 def get_b0 : Result Bool := do
diff --git a/tests/lean/BuiltinAuto.lean b/tests/lean/BuiltinAuto.lean
index 674dd52f26..8c18cf1481 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 854:0-854:55
+    Source: '/rustc/library/core/src/ptr/mod.rs', lines 876:0-876: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 6e44a4a24e..3dddc02b87 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 1880:16-1880:50
+    Source: '/rustc/library/core/src/cmp.rs', lines 2156:16-2156: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 2127:4-2127:38
+    Source: '/rustc/library/alloc/src/boxed.rs', lines 2170:4-2170: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"]
@@ -261,7 +261,8 @@ def CopyEnum.Insts.CoreMarkerCopy {T : Type} (coremarkerCopyInst :
 /-- Trait implementation: [derive::{impl core::marker::StructuralPartialEq for derive::CopyEnum<T>}]
     Source: 'tests/src/derive.rs', lines 16:22-16:31 -/
 @[reducible]
-def CopyEnum.Insts.CoreMarkerStructuralPartialEq (T : Type) :
+def CopyEnum.Insts.CoreMarkerStructuralPartialEq {T : Type}
+  (corecmpPartialEqInst : core.cmp.PartialEq T T) :
   core.marker.StructuralPartialEq (CopyEnum T) := {
 }
 
@@ -406,8 +407,8 @@ def Enum.Insts.CoreCloneClone {T : Type} (corecloneCloneInst : core.clone.Clone
 /-- Trait implementation: [derive::{impl core::marker::StructuralPartialEq for derive::Enum<T>}]
     Source: 'tests/src/derive.rs', lines 24:16-24:25 -/
 @[reducible]
-def Enum.Insts.CoreMarkerStructuralPartialEq (T : Type) :
-  core.marker.StructuralPartialEq (Enum T) := {
+def Enum.Insts.CoreMarkerStructuralPartialEq {T : Type} (corecmpPartialEqInst :
+  core.cmp.PartialEq T T) : core.marker.StructuralPartialEq (Enum T) := {
 }
 
 /-- [derive::{impl core::cmp::PartialEq<derive::Enum<T>> for derive::Enum<T>}::eq]:
@@ -556,8 +557,8 @@ def List.Insts.CoreCloneClone {T : Type} (corecloneCloneInst : core.clone.Clone
 /-- Trait implementation: [derive::{impl core::marker::StructuralPartialEq for derive::List<T>}]
     Source: 'tests/src/derive.rs', lines 34:16-34:25 -/
 @[reducible]
-def List.Insts.CoreMarkerStructuralPartialEq (T : Type) :
-  core.marker.StructuralPartialEq (List T) := {
+def List.Insts.CoreMarkerStructuralPartialEq {T : Type} (corecmpPartialEqInst :
+  core.cmp.PartialEq T T) : core.marker.StructuralPartialEq (List T) := {
 }
 
 /-- [derive::{impl core::cmp::PartialEq<derive::List<T>> for derive::List<T>}::eq]:
@@ -658,7 +659,8 @@ def CopyStruct.Insts.CoreMarkerCopy {T : Type} (coremarkerCopyInst :
 /-- Trait implementation: [derive::{impl core::marker::StructuralPartialEq for derive::CopyStruct<T>}]
     Source: 'tests/src/derive.rs', lines 41:22-41:31 -/
 @[reducible]
-def CopyStruct.Insts.CoreMarkerStructuralPartialEq (T : Type) :
+def CopyStruct.Insts.CoreMarkerStructuralPartialEq {T : Type}
+  (corecmpPartialEqInst : core.cmp.PartialEq T T) :
   core.marker.StructuralPartialEq (CopyStruct T) := {
 }
 
@@ -761,8 +763,8 @@ def Struct.Insts.CoreCloneClone {T : Type} (corecloneCloneInst :
 /-- Trait implementation: [derive::{impl core::marker::StructuralPartialEq for derive::Struct<T>}]
     Source: 'tests/src/derive.rs', lines 49:16-49:25 -/
 @[reducible]
-def Struct.Insts.CoreMarkerStructuralPartialEq (T : Type) :
-  core.marker.StructuralPartialEq (Struct T) := {
+def Struct.Insts.CoreMarkerStructuralPartialEq {T : Type} (corecmpPartialEqInst
+  : core.cmp.PartialEq T T) : core.marker.StructuralPartialEq (Struct T) := {
 }
 
 /-- [derive::{impl core::cmp::PartialEq<derive::Struct<T>> for derive::Struct<T>}::eq]:
diff --git a/tests/lean/Drop.lean b/tests/lean/Drop.lean
index a0119232eb..3f3ce69e89 100644
--- a/tests/lean/Drop.lean
+++ b/tests/lean/Drop.lean
@@ -12,8 +12,29 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace drop
 
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
 /-- [drop::fill]: loop body 0:
     Source: 'tests/src/drop.rs', lines 7:4-9:5 -/
 @[rust_loop_body]
diff --git a/tests/lean/Issue807MissingSymbolicValue.lean b/tests/lean/Issue807MissingSymbolicValue.lean
index 4e0f074a35..bee6a141c3 100644
--- a/tests/lean/Issue807MissingSymbolicValue.lean
+++ b/tests/lean/Issue807MissingSymbolicValue.lean
@@ -12,8 +12,29 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace issue_807_missing_symbolic_value
 
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
 /-- [issue_807_missing_symbolic_value::PortableVector]
     Source: 'tests/src/issue-807-missing-symbolic-value.rs', lines 4:0-6:1 -/
 structure PortableVector where
diff --git a/tests/lean/IterAdapters.lean b/tests/lean/IterAdapters.lean
index f1aee05264..c1b3e4390d 100644
--- a/tests/lean/IterAdapters.lean
+++ b/tests/lean/IterAdapters.lean
@@ -12,8 +12,101 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace iter_adapters
 
+/-- [core::iter::range::{impl core::iter::range::Step for u8}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<u8>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u8>}::backward_overflowing"]
+axiom U8.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.U8 → Std.Usize → Result (Std.U8 × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u8}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<u8>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u8>}::forward_overflowing"]
+axiom U8.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.U8 → Std.Usize → Result (Std.U8 × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u16}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<u16>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u16>}::backward_overflowing"]
+axiom U16.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.U16 → Std.Usize → Result (Std.U16 × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u16}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<u16>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u16>}::forward_overflowing"]
+axiom U16.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.U16 → Std.Usize → Result (Std.U16 × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u32}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u32>}::backward_overflowing"]
+axiom U32.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.U32 → Std.Usize → Result (Std.U32 × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u32}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u32>}::forward_overflowing"]
+axiom U32.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.U32 → Std.Usize → Result (Std.U32 × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u64}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<u64>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u64>}::backward_overflowing"]
+axiom U64.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.U64 → Std.Usize → Result (Std.U64 × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u64}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<u64>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u64>}::forward_overflowing"]
+axiom U64.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.U64 → Std.Usize → Result (Std.U64 × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
 /-- [iter_adapters::test_enumerate_slice]:
     Source: 'tests/src/iter_adapters.rs', lines 14:0-24:1
     Visibility: public -/
diff --git a/tests/lean/Iterators.lean b/tests/lean/Iterators.lean
index cbf8daac38..830139ff4e 100644
--- a/tests/lean/Iterators.lean
+++ b/tests/lean/Iterators.lean
@@ -12,8 +12,29 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace iterators
 
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
 /-- [iterators::iter_range]: loop body 0:
     Source: 'tests/src/iterators.rs', lines 5:4-5:28 -/
 @[rust_loop_body]
diff --git a/tests/lean/IteratorsScalar.lean b/tests/lean/IteratorsScalar.lean
index f1cd2ce7af..4675674bf8 100644
--- a/tests/lean/IteratorsScalar.lean
+++ b/tests/lean/IteratorsScalar.lean
@@ -12,8 +12,29 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace iterators_scalar
 
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
 /-- [iterators_scalar::iter]: loop body 0:
     Source: 'tests/src/iterators-scalar.rs', lines 5:4-7:5 -/
 @[rust_loop_body]
diff --git a/tests/lean/LoopSharedBorrowProj.lean b/tests/lean/LoopSharedBorrowProj.lean
index d8a9334e10..7bcdd1a647 100644
--- a/tests/lean/LoopSharedBorrowProj.lean
+++ b/tests/lean/LoopSharedBorrowProj.lean
@@ -18,7 +18,7 @@ noncomputable section
 namespace loop_shared_borrow_proj
 
 /-- [alloc::vec::{impl core::iter::traits::collect::IntoIterator<&'a T, core::slice::iter::Iter<'a, T>> for &'a alloc::vec::Vec<T>}::into_iter]:
-    Source: '/rustc/library/alloc/src/vec/mod.rs', lines 3981:4-3981:40
+    Source: '/rustc/library/alloc/src/vec/mod.rs', lines 4047:4-4047:40
     Name pattern: [alloc::vec::{core::iter::traits::collect::IntoIterator<&'a alloc::vec::Vec<@T>, &'a @T, core::slice::iter::Iter<'a, @T>>}::into_iter]
     Visibility: public -/
 @[rust_fun
diff --git a/tests/lean/LoopSharedLoanInJoin.lean b/tests/lean/LoopSharedLoanInJoin.lean
index aab74d8065..199a276bbb 100644
--- a/tests/lean/LoopSharedLoanInJoin.lean
+++ b/tests/lean/LoopSharedLoanInJoin.lean
@@ -12,8 +12,29 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace loop_shared_loan_in_join
 
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
 /-- [loop_shared_loan_in_join::State]
     Source: 'tests/src/loop_shared_loan_in_join.rs', lines 16:0-22:1
     Visibility: public -/
diff --git a/tests/lean/LoopsIssues.lean b/tests/lean/LoopsIssues.lean
index 93dd4b5483..d15aa74cb2 100644
--- a/tests/lean/LoopsIssues.lean
+++ b/tests/lean/LoopsIssues.lean
@@ -12,8 +12,29 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace loops_issues
 
+/-- [core::iter::range::{impl core::iter::range::Step for i32}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 442:16-442:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<i32>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<i32>}::backward_overflowing"]
+axiom I32.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.I32 → Std.Usize → Result (Std.I32 × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for i32}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 431:16-431:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<i32>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<i32>}::forward_overflowing"]
+axiom I32.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.I32 → Std.Usize → Result (Std.I32 × Bool)
+
 /-- [loops_issues::write]:
     Source: 'tests/src/loops-issues.rs', lines 5:0-5:28 -/
 def write (a : Array Std.U8 4#usize) : Result (Array Std.U8 4#usize) := do
diff --git a/tests/lean/LoopsNested.lean b/tests/lean/LoopsNested.lean
index dfc2dd8f0e..4149aead16 100644
--- a/tests/lean/LoopsNested.lean
+++ b/tests/lean/LoopsNested.lean
@@ -12,8 +12,29 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace loops_nested
 
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
 /-- [loops_nested::iter]: loop body 1:
     Source: 'tests/src/loops-nested.rs', lines 7:8-9:9
     Visibility: public -/
diff --git a/tests/lean/LoopsNestedRec.lean b/tests/lean/LoopsNestedRec.lean
index 128ff93427..195535c717 100644
--- a/tests/lean/LoopsNestedRec.lean
+++ b/tests/lean/LoopsNestedRec.lean
@@ -12,8 +12,29 @@ set_option maxHeartbeats 1000000
 /- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
 set_option maxRecDepth 2048
 
+/- You can remove the following line by using the CLI option `-all-computable`: -/
+noncomputable section
+
 namespace loops_nested_rec
 
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::backward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 357:16-357:78
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::backward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.backward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
+/-- [core::iter::range::{impl core::iter::range::Step for usize}::forward_overflowing]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 348:16-348:77
+    Name pattern: [core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<usize>}::forward_overflowing"]
+axiom Usize.Insts.CoreIterRangeStep.forward_overflowing
+  : Std.Usize → Std.Usize → Result (Std.Usize × Bool)
+
 /-- [loops_nested_rec::iter]: loop 1:
     Source: 'tests/src/loops-nested-rec.rs', lines 8:8-10:9
     Visibility: public -/
diff --git a/tests/lean/NestedSharedBorrows.lean b/tests/lean/NestedSharedBorrows.lean
index 00aa471c6f..8cacf249ba 100644
--- a/tests/lean/NestedSharedBorrows.lean
+++ b/tests/lean/NestedSharedBorrows.lean
@@ -18,7 +18,7 @@ noncomputable section
 namespace nested_shared_borrows
 
 /-- [core::option::{impl core::ops::try_trait::Try for core::option::Option<T>}::branch]:
-    Source: '/rustc/library/core/src/option.rs', lines 2779:4-2779:64
+    Source: '/rustc/library/core/src/option.rs', lines 2868:4-2868:64
     Name pattern: [core::option::{core::ops::try_trait::Try<core::option::Option<@T>>}::branch]
     Visibility: public -/
 @[rust_fun
@@ -29,7 +29,7 @@ axiom core.option.Option.Insts.CoreOpsTry_traitTry.branch
     core.convert.Infallible) T)
 
 /-- [core::option::{impl core::ops::try_trait::FromResidual<core::option::Option<core::convert::Infallible>> for core::option::Option<T>}::from_residual]:
-    Source: '/rustc/library/core/src/option.rs', lines 2793:4-2793:67
+    Source: '/rustc/library/core/src/option.rs', lines 2882:4-2882:67
     Name pattern: [core::option::{core::ops::try_trait::FromResidual<core::option::Option<@T>, core::option::Option<core::convert::Infallible>>}::from_residual]
     Visibility: public -/
 @[rust_fun
diff --git a/tests/lean/RustBorrowCheckIssues.lean b/tests/lean/RustBorrowCheckIssues.lean
index c2d0c0cc13..9f11bbdc05 100644
--- a/tests/lean/RustBorrowCheckIssues.lean
+++ b/tests/lean/RustBorrowCheckIssues.lean
@@ -18,14 +18,14 @@ noncomputable section
 namespace rust_borrow_check_issues
 
 /-- [core::mem::drop]:
-    Source: '/rustc/library/core/src/mem/mod.rs', lines 1000:0-1002:24
+    Source: '/rustc/library/core/src/mem/mod.rs', lines 1045:0-1047:24
     Name pattern: [core::mem::drop]
     Visibility: public -/
 @[rust_fun "core::mem::drop"]
 axiom core.mem.drop {T : Type} : T → Result Unit
 
 /-- [core::option::{core::option::Option<T>}::as_mut]:
-    Source: '/rustc/library/core/src/option.rs', lines 763:4-763:52
+    Source: '/rustc/library/core/src/option.rs', lines 764:4-764:52
     Name pattern: [core::option::{core::option::Option<@T>}::as_mut]
     Visibility: public -/
 @[rust_fun "core::option::{core::option::Option<@T>}::as_mut"]
diff --git a/tests/lean/VecIter.lean b/tests/lean/VecIter.lean
index b2468dc8c5..06595a23a7 100644
--- a/tests/lean/VecIter.lean
+++ b/tests/lean/VecIter.lean
@@ -18,7 +18,7 @@ noncomputable section
 namespace vec_iter
 
 /-- [alloc::vec::{impl core::iter::traits::collect::IntoIterator<&'a T, core::slice::iter::Iter<'a, T>> for &'a alloc::vec::Vec<T>}::into_iter]:
-    Source: '/rustc/library/alloc/src/vec/mod.rs', lines 3981:4-3981:40
+    Source: '/rustc/library/alloc/src/vec/mod.rs', lines 4047:4-4047:40
     Name pattern: [alloc::vec::{core::iter::traits::collect::IntoIterator<&'a alloc::vec::Vec<@T>, &'a @T, core::slice::iter::Iter<'a, @T>>}::into_iter]
     Visibility: public -/
 @[rust_fun