diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 3b84397..e45ada8 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -10,7 +10,7 @@ on:
 env:
   RUST_TOOLCHAIN: nightly-2026-02-07
   CHARON_REV:    a535e914f74db4fd9e6be7048f4233270d8945c0
-  AENEAS_REV:    8d2077ce4946b52d2d199fe9d2f2d520a4bf8184
+  AENEAS_REV:    157c25e0010dd4a010813fa5094cd0055ac055b1
   # Where the cache step stages the charon / aeneas binaries.
   AENEAS_DIR: ${{ github.workspace }}/.tools/aeneas
 
diff --git a/Makefile b/Makefile
index 26ae3de..afe384e 100644
--- a/Makefile
+++ b/Makefile
@@ -35,11 +35,11 @@ ALLOC_CHARON_EXCLUDES = \
     --exclude '{impl alloc_models::collections::binary_heap::BinaryHeap<_, _>}::*' \
     --exclude 'alloc_models::string::*' \
     --exclude '{impl alloc_models::string::String}::*' \
-    --exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::vec::Vec<_, _>}' \
-    --exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::vec::Vec<_, _>}::*' \
-    --exclude 'alloc_models::slice::_::sort_by' \
-    --exclude '{impl core::ops::index::Index<_> for alloc_models::vec::Vec<_, _>}' \
-    --exclude '{impl core::ops::index::Index<_> for alloc_models::vec::Vec<_, _>}::*'
+    --exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::vec::Vec<_>}' \
+    --exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::vec::Vec<_>}::*' \
+    --exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::collections::vec_deque::VecDeque<_, _>}' \
+    --exclude '{impl core::iter::traits::collect::FromIterator<_> for alloc_models::collections::vec_deque::VecDeque<_, _>}::*' \
+    --exclude 'alloc_models::slice::_::sort_by'
 
 .PHONY: all llbc extract patch lean build clean clean-generated tests \
         tests-clean alloc-stage alloc-llbc alloc-extract alloc-clean
@@ -66,8 +66,7 @@ CHARON_EXCLUDES = \
     --exclude 'core_models::option::_::is_some' \
     --exclude 'core_models::option::_::is_none' \
     --exclude 'core_models::option::_::unwrap_or' \
-    --exclude 'core_models::option::_::take' \
-    --exclude 'core_models::slice::index::*'
+    --exclude 'core_models::option::_::take' 
 
 llbc: $(LLBC_FILE)
 
@@ -82,9 +81,7 @@ $(LLBC_FILE): $(CORE_MODELS_DIR)/src/**/*.rs $(CORE_MODELS_DIR)/Cargo.toml
 #    $(LEAN_DIR)/Aeneas/ is left untouched.
 extract: $(LLBC_FILE) alloc-extract
 	mkdir -p $(LEAN_DIR)
-	# Aeneas may exit non-zero while still producing partial files; that's OK,
-	# our patcher and the surrounding hand-written library handle the gaps.
-	-$(AENEAS) -core-models-lib -backend lean $(LLBC_FILE) -split-files -dest $(LEAN_DIR) \
+	$(AENEAS) -core-models-lib -backend lean $(LLBC_FILE) -split-files -dest $(LEAN_DIR) \
 	-subdir CoreModels/Core -all-computable
 
 # -----------------------------------------------------------------------------
@@ -119,7 +116,7 @@ alloc-llbc: $(ALLOC_LLBC_FILE)
 # `-subdir CoreModels/Alloc` makes Aeneas emit `import CoreModels.Alloc.<X>` rather
 # than the auto-derived `Alloc_models.<X>` prefix.
 alloc-extract: $(ALLOC_LLBC_FILE)
-	-$(AENEAS) -core-models-lib -backend lean $(ALLOC_LLBC_FILE) -split-files \
+	$(AENEAS) -core-models-lib -backend lean $(ALLOC_LLBC_FILE) -split-files \
 	    -dest $(LEAN_DIR) -subdir CoreModels/Alloc -all-computable
 
 # 3. Move generated files into $(LEAN_DIR)/CoreModels/ and apply our patches
diff --git a/alloc/src/lib.rs b/alloc/src/lib.rs
index d77b966..dbf2efc 100644
--- a/alloc/src/lib.rs
+++ b/alloc/src/lib.rs
@@ -9,8 +9,17 @@ mod testing {
 }
 
 mod alloc {
+    pub trait Allocator {
+        fn dummy();
+    }
+
     #[cfg_attr(test, derive(PartialEq, Debug))]
+    #[derive(Clone)]
     pub struct Global;
+
+    impl Allocator for Global {
+        fn dummy() {}
+    }
 }
 
 mod borrow {
@@ -42,7 +51,7 @@ mod collections {
     mod binary_heap {
         #[hax_lib::fstar::before("open Rust_primitives.Notations")]
         use crate::vec::*;
-        struct BinaryHeap<T, A>(Vec<T, A>);
+        struct BinaryHeap<T, A>(Vec<T>, std::marker::PhantomData<A>);
 
         impl BinaryHeap<(), ()> {}
         impl BinaryHeap<(), ()> {}
@@ -56,12 +65,12 @@ mod collections {
         impl BinaryHeap<(), ()> {}
 
         #[hax_lib::attributes]
-        impl<T: Ord, A> BinaryHeap<T, A> {
+        impl<T: Ord, A: crate::alloc::Allocator> BinaryHeap<T, A> {
             fn new() -> BinaryHeap<T, A> {
-                BinaryHeap(Vec(
-                    rust_primitives::sequence::seq_empty(),
+                BinaryHeap(
+                    Vec(rust_primitives::sequence::seq_empty()),
                     std::marker::PhantomData::<A>,
-                ))
+                )
             }
             #[hax_lib::requires(self.len() < core::primitive::usize::MAX)]
             fn push(&mut self, v: T) {
@@ -87,7 +96,7 @@ mod collections {
         }
 
         #[hax_lib::attributes]
-        impl<T: Ord, A> BinaryHeap<T, A> {
+        impl<T: Ord, A: crate::alloc::Allocator> BinaryHeap<T, A> {
             fn len(&self) -> usize {
                 self.0.len()
             }
@@ -216,6 +225,52 @@ assume val lemma_peek_pop: #t:Type -> (#a: Type) -> (#i: Core_models.Cmp.t_Ord t
                 seq_index(&self.0, i)
             }
         }
+
+        pub mod into_iter {
+            use rust_primitives::sequence::*;
+            pub struct IntoIter<T, A>(pub Seq<T>, pub std::marker::PhantomData<A>);
+            impl<T, A> Iterator for IntoIter<T, A> {
+                type Item = T;
+                fn next(&mut self) -> Option<Self::Item> {
+                    if seq_len(&self.0) == 0 {
+                        None
+                    } else {
+                        Some(seq_remove(&mut self.0, 0))
+                    }
+                }
+            }
+        }
+
+        impl<T, A> IntoIterator for VecDeque<T, A> {
+            type Item = T;
+            type IntoIter = into_iter::IntoIter<T, A>;
+            fn into_iter(self) -> Self::IntoIter {
+                into_iter::IntoIter(self.0, std::marker::PhantomData)
+            }
+        }
+
+        // Like `Vec`, `FromIterator` is only implemented for the `Global`
+        // allocator (std has no way to thread an allocator through
+        // `from_iter`), so `Self` is `VecDeque<T, Global>` — matching the
+        // `VecDequeTGlobal` impl name downstream expects.
+        #[hax_lib::attributes]
+        #[hax_lib::opaque]
+        impl<T> std::iter::FromIterator<T> for VecDeque<T, crate::alloc::Global> {
+            fn from_iter<I>(iter: I) -> Self
+            where
+                I: IntoIterator<Item = T>,
+            {
+                // The impl is `#[opaque]`, so this body is axiomatised and need
+                // not actually consume `iter`. We deliberately avoid a `for`
+                // loop: hax hoists the loop into a separate function that is
+                // *not* covered by `#[opaque]`, and Aeneas then fails to
+                // extract it (`type_var_id: 1` — the iterator type `I`). A
+                // straight-line construction extracts cleanly. (`Vec`'s
+                // analogous impl sidesteps this by being `--exclude`d in the
+                // Makefile, but we need this symbol to exist.)
+                VecDeque(seq_empty(), std::marker::PhantomData)
+            }
+        }
     }
 }
 
@@ -234,16 +289,16 @@ mod slice {
     use rust_primitives::sequence::*;
 
     impl<T> Dummy<T> {
-        fn to_vec(s: &[T]) -> Vec<T, crate::alloc::Global>
+        fn to_vec(s: &[T]) -> Vec<T>
         where
             T: Clone,
         {
             let mut seq = seq_empty();
             seq_extend(&mut seq, s);
-            Vec(seq, std::marker::PhantomData::<crate::alloc::Global>)
+            Vec(seq)
         }
-        fn into_vec<A>(s: Box<[T]>) -> Vec<T, A> {
-            Vec(seq_from_boxed_slice(s), std::marker::PhantomData::<A>)
+        fn into_vec(s: Box<[T]>) -> Vec<T> {
+            Vec(seq_from_boxed_slice(s))
         }
         #[hax_lib::opaque]
         fn sort_by<F: Fn(&T, &T) -> core::cmp::Ordering>(s: &mut [T], compare: F) {}
@@ -263,7 +318,7 @@ mod slice {
             #[test]
             fn test_into_vec(v in prop::collection::vec(any::<u8>(), 0..100)) {
                 let boxed: Box<[u8]> = v.clone().into_boxed_slice();
-                let model: crate::vec::Vec<u8, crate::alloc::Global> = super::Dummy::<u8>::into_vec(boxed);
+                let model: crate::vec::Vec<u8> = super::Dummy::<u8>::into_vec(boxed);
                 prop_assert_eq!(model.as_slice(), v.as_slice());
             }
         }
@@ -335,7 +390,35 @@ pub mod vec {
 
     #[cfg_attr(test, derive(Debug))]
     #[hax_lib::fstar::before("open Rust_primitives.Notations")]
-    pub struct Vec<T, A>(pub Seq<T>, pub std::marker::PhantomData<A>);
+    pub struct Vec<T>(pub Seq<T>);
+
+    impl<T: Clone> Clone for Vec<T> {
+        fn clone(&self) -> Self {
+            let mut new_vec = seq_empty();
+            for it in self.iter() {
+                seq_push(&mut new_vec, it.clone());
+            }
+            Vec(new_vec)
+        }
+    }
+    impl<T, U> PartialEq<Vec<U>> for Vec<T>
+    where
+        T: PartialEq<U>,
+    {
+        fn eq(&self, other: &Vec<U>) -> bool {
+            if !(self.len() == other.len()) {
+                false
+            } else {
+                let mut res = true;
+                for i in 0..self.len() {
+                    if !(self[i] == other[i]) {
+                        res = false
+                    }
+                }
+                res
+            }
+        }
+    }
 
     /// Opaque model of `std::vec::IntoIter<T, A>`. Downstream Aeneas
     /// extractions reference this type via its full path
@@ -343,31 +426,43 @@ pub mod vec {
     /// matching submodule.
     pub mod into_iter {
         use rust_primitives::sequence::*;
-        pub struct IntoIter<T, A>(pub Seq<T>, pub std::marker::PhantomData<A>);
+        pub struct IntoIter<T>(pub Seq<T>);
+        impl<T> Iterator for IntoIter<T> {
+            type Item = T;
+            fn next(&mut self) -> Option<Self::Item> {
+                if seq_len(&self.0) == 0 {
+                    None
+                } else {
+                    Some(seq_remove(&mut self.0, 0))
+                }
+            }
+        }
     }
 
-    fn from_elem<T: Clone>(item: T, len: usize) -> Vec<T, crate::alloc::Global> {
-        Vec(
-            seq_create(item, len),
-            std::marker::PhantomData::<crate::alloc::Global>,
-        )
+    impl<T> IntoIterator for Vec<T> {
+        type Item = T;
+        type IntoIter = into_iter::IntoIter<T>;
+        fn into_iter(self) -> Self::IntoIter {
+            into_iter::IntoIter(self.0)
+        }
+    }
+
+    fn from_elem<T: Clone>(item: T, len: usize) -> Vec<T> {
+        Vec(seq_create(item, len))
     }
 
     #[hax_lib::attributes]
-    impl<T> Vec<T, crate::alloc::Global> {
-        pub fn new() -> Vec<T, crate::alloc::Global> {
-            Vec(
-                seq_empty(),
-                std::marker::PhantomData::<crate::alloc::Global>,
-            )
+    impl<T> Vec<T> {
+        pub fn new() -> Vec<T> {
+            Vec(seq_empty())
         }
-        pub fn with_capacity(_c: usize) -> Vec<T, crate::alloc::Global> {
+        pub fn with_capacity(_c: usize) -> Vec<T> {
             Vec::new()
         }
     }
 
     #[hax_lib::attributes]
-    impl<T, A> Vec<T, A> {
+    impl<T> Vec<T> {
         pub fn len(&self) -> usize {
             seq_len(&self.0)
         }
@@ -405,7 +500,11 @@ pub mod vec {
         }
         #[hax_lib::opaque]
         #[hax_lib::ensures(|_| future(self).len() == new_size)]
-        pub fn resize(&mut self, new_size: usize, value: &T) {}
+        pub fn resize(&mut self, new_size: usize, value: &T)
+        where
+            T: Clone,
+        {
+        }
         #[hax_lib::opaque]
         pub fn remove(&mut self, index: usize) -> T {
             seq_remove(&mut self.0, index)
@@ -413,14 +512,20 @@ pub mod vec {
         #[hax_lib::opaque]
         pub fn clear(&mut self) {}
         #[hax_lib::requires(self.len().to_int() + other.len().to_int() <= usize::MAX.to_int())]
-        pub fn append(&mut self, other: &mut Vec<T, A>) {
+        pub fn append(&mut self, other: &mut Vec<T>) {
             seq_concat(&mut self.0, &mut other.0);
             other.0 = seq_empty()
         }
         #[hax_lib::opaque]
-        pub fn drain<R /* : RangeBounds<usize> */>(&mut self, _range: R) -> drain::Drain<T, A> {
+        pub fn drain<R /* : RangeBounds<usize> */>(
+            &mut self,
+            _range: R,
+        ) -> drain::Drain<T, crate::alloc::Global> {
             let l = seq_len(&self.0);
-            drain::Drain(seq_drain(&mut self.0, 0, l), std::marker::PhantomData::<A>) // TODO use range bounds
+            drain::Drain(
+                seq_drain(&mut self.0, 0, l),
+                std::marker::PhantomData::<crate::alloc::Global>,
+            ) // TODO use range bounds
         }
     }
     pub mod drain {
@@ -440,7 +545,7 @@ pub mod vec {
     }
 
     #[hax_lib::attributes]
-    impl<T: Clone, A> Vec<T, A> {
+    impl<T: Clone> Vec<T> {
         #[hax_lib::requires(seq_len(&self.0).to_int() + other.len().to_int() <= usize::MAX.to_int())]
         fn extend_from_slice(&mut self, other: &[T]) {
             seq_extend(&mut self.0, other)
@@ -460,7 +565,7 @@ pub mod vec {
     /// with `core_models`'s SliceIndex extraction (both extract under
     /// `core.slice.index.SliceIndex`).
     #[hax_lib::attributes]
-    impl<T, I, A> std::ops::Index<I> for Vec<T, A>
+    impl<T, I> std::ops::Index<I> for Vec<T>
     where
         I: std::slice::SliceIndex<[T]>,
     {
@@ -472,7 +577,7 @@ pub mod vec {
     }
 
     #[hax_lib::attributes]
-    impl<T, A> core::ops::Deref for Vec<T, A> {
+    impl<T> core::ops::Deref for Vec<T> {
         type Target = [T];
 
         fn deref(&self) -> &[T] {
@@ -482,7 +587,7 @@ pub mod vec {
 
     #[hax_lib::attributes]
     #[hax_lib::opaque]
-    impl<T> std::iter::FromIterator<T> for Vec<T, crate::alloc::Global> {
+    impl<T> std::iter::FromIterator<T> for Vec<T> {
         fn from_iter<I>(iter: I) -> Self
         where
             I: IntoIterator<Item = T>,
@@ -501,20 +606,11 @@ pub mod vec {
         use proptest::prelude::*;
 
         impl<T: Clone> Inject for Vec<T> {
-            type Model = super::Vec<T, crate::alloc::Global>;
-            fn inject(&self) -> super::Vec<T, crate::alloc::Global> {
-                super::Vec::<T, crate::alloc::Global>(
-                    rust_primitives::sequence::seq_from_boxed_slice(
-                        self.clone().into_boxed_slice(),
-                    ),
-                    std::marker::PhantomData::<crate::alloc::Global>,
-                )
-            }
-        }
-
-        impl<T: PartialEq, A> PartialEq for super::Vec<T, A> {
-            fn eq(&self, other: &Self) -> bool {
-                self.0 == other.0
+            type Model = super::Vec<T>;
+            fn inject(&self) -> super::Vec<T> {
+                super::Vec::<T>(rust_primitives::sequence::seq_from_boxed_slice(
+                    self.clone().into_boxed_slice(),
+                ))
             }
         }
 
@@ -604,18 +700,46 @@ pub mod vec {
                 let model = super::from_elem(x, len);
                 prop_assert_eq!(model, vec![x; len].inject());
             }
+
+            // ----- Clone / PartialEq / IntoIterator -------
+
+            #[test]
+            fn test_vec_clone(v in prop::collection::vec(any::<u8>(), 0..30)) {
+                // Compare the clone's contents to std directly (independent of
+                // the model's own `PartialEq`, which is tested separately).
+                let cloned = v.inject().clone();
+                prop_assert_eq!(cloned.as_slice(), v.as_slice());
+            }
+
+            #[test]
+            fn test_vec_eq(
+                a in prop::collection::vec(any::<u8>(), 0..15),
+                b in prop::collection::vec(any::<u8>(), 0..15),
+            ) {
+                prop_assert_eq!(a.inject() == b.inject(), a == b);
+            }
+
+            #[test]
+            fn test_vec_into_iter(v in prop::collection::vec(any::<u8>(), 0..30)) {
+                let mut it = v.inject().into_iter();
+                let mut collected: std::vec::Vec<u8> = std::vec::Vec::new();
+                while let Some(x) = it.next() {
+                    collected.push(x);
+                }
+                prop_assert_eq!(collected.as_slice(), v.as_slice());
+            }
         }
 
         #[test]
         fn test_new() {
-            let model: super::Vec<u8, crate::alloc::Global> = super::Vec::new();
+            let model: super::Vec<u8> = super::Vec::new();
             let std_v: std::vec::Vec<u8> = std::vec::Vec::new();
             assert_eq!(model, std_v.inject());
         }
 
         #[test]
         fn test_with_capacity() {
-            let model: super::Vec<u8, crate::alloc::Global> = super::Vec::with_capacity(10);
+            let model: super::Vec<u8> = super::Vec::with_capacity(10);
             let std_v: std::vec::Vec<u8> = std::vec::Vec::with_capacity(10);
             assert_eq!(model, std_v.inject());
         }
diff --git a/core-models/src/core/array.rs b/core-models/src/core/array.rs
index 836b357..dc4c393 100644
--- a/core-models/src/core/array.rs
+++ b/core-models/src/core/array.rs
@@ -5,34 +5,34 @@ pub struct TryFromSliceError;
 
 // Dummy type to allow impls
 #[hax_lib::exclude]
-struct Dummy<T, const N: usize>([T; N]);
-
-// Dummy impls to get the right disambiguator (https://github.com/cryspen/hax/issues/828)
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-impl<T> Dummy<T, 0> {}
-
-impl<T, const N: usize> Dummy<T, N> {
+struct Array<T, const N: usize>([T; N]);
+
+// Array impls to get the right disambiguator (https://github.com/cryspen/hax/issues/828)
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+impl<T> Array<T, 0> {}
+
+impl<T, const N: usize> Array<T, N> {
     /// See [`std::array::map`]
     pub fn map<F: Fn(T) -> U, U>(s: [T; N], f: F) -> [U; N] {
         array_map(s, f)
@@ -71,6 +71,19 @@ use crate::ops::{
 
 #[hax_lib::attributes]
 #[cfg_attr(hax_backend_lean, hax_lib::exclude)]
+impl<T, I, const N: usize> crate::ops::index::Index<I> for [T; N]
+where
+    [T]: Index<I>,
+{
+    type Output = <[T] as Index<I>>::Output;
+    #[hax_lib::requires(i.get(self).is_some())]
+    fn index(&self, i: I) -> &Self::Output {
+        self.as_slice().index(i)
+    }
+}
+
+/* #[hax_lib::attributes]
+#[cfg_attr(hax_backend_lean, hax_lib::exclude)]
 impl<T, const N: usize> Index<usize> for [T; N] {
     type Output = T;
     #[hax_lib::requires(i < self.len())]
@@ -113,7 +126,7 @@ impl<T, const N: usize> Index<RangeFull> for [T; N] {
     fn index(&self, i: RangeFull) -> &[T] {
         array_slice(self, 0, N)
     }
-}
+} */
 
 #[cfg(not(hax))]
 impl<T: crate::clone::Clone, const N: usize> crate::clone::Clone for [T; N] {
@@ -177,7 +190,7 @@ mod tests {
         fn test_as_slice(arr in any::<[u8; 4]>()) {
             let model_arr = arr.inject();
             prop_assert_eq!(
-                super::Dummy::<u8, 4>::as_slice(&model_arr),
+                super::Array::<u8, 4>::as_slice(&model_arr),
                 arr.as_slice()
             );
         }
@@ -216,7 +229,7 @@ mod tests {
         #[test]
         fn test_each_ref(arr in any::<[u8; 4]>()) {
             let model_arr = arr.inject();
-            let model_refs = super::Dummy::<u8, 4>::each_ref(&model_arr);
+            let model_refs = super::Array::<u8, 4>::each_ref(&model_arr);
             let std_refs = arr.each_ref();
             for i in 0..4 {
                 prop_assert_eq!(*model_refs[i], *std_refs[i]);
diff --git a/core-models/src/core/fmt.rs b/core-models/src/core/fmt.rs
index 8eaff73..c84fe49 100644
--- a/core-models/src/core/fmt.rs
+++ b/core-models/src/core/fmt.rs
@@ -9,6 +9,12 @@ pub type Result = super::result::Result<(), Error>;
 /// See [`std::fmt::Formatter`]
 pub struct Formatter;
 
+impl Formatter {
+    pub fn write_str(&mut self, data: &str) -> Result {
+        Result::Ok(())
+    }
+}
+
 /// See [`std::fmt::Display`]
 pub trait Display {
     /// See [`std::fmt::Display::fmt`]
@@ -18,14 +24,14 @@ pub trait Display {
 /// See [`std::fmt::Debug`]
 pub trait Debug {
     /// See [`std::fmt::Debug::fmt`]
-    fn dbg_fmt(&self, f: &mut Formatter) -> Result;
+    fn fmt(&self, f: &mut Formatter) -> Result;
 }
 
 /// See [`std::fmt::Arguments`]
 pub struct Arguments<'a>(&'a ());
 
 impl<T> Debug for T {
-    fn dbg_fmt(&self, f: &mut Formatter) -> Result {
+    fn fmt(&self, f: &mut Formatter) -> Result {
         Result::Ok(())
     }
 }
diff --git a/core-models/src/core/iter.rs b/core-models/src/core/iter.rs
index f1e2d15..b1483f1 100644
--- a/core-models/src/core/iter.rs
+++ b/core-models/src/core/iter.rs
@@ -443,7 +443,7 @@ pub mod adapters {
             iter: I,
             step: usize,
         }
-        #[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
+
         impl<I> StepBy<I> {
             pub fn new(iter: I, step: usize) -> Self {
                 StepBy { iter, step }
@@ -451,7 +451,6 @@ pub mod adapters {
         }
 
         #[hax_lib::opaque]
-        #[cfg_attr(charon, aeneas::exclude)]
         impl<I: Iterator> Iterator for StepBy<I> {
             type Item = <I as Iterator>::Item;
 
@@ -471,7 +470,7 @@ pub mod adapters {
             iter: I,
             f: F,
         }
-        #[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
+
         impl<I, F> Map<I, F> {
             pub fn new(iter: I, f: F) -> Self {
                 Self { iter, f }
diff --git a/core-models/src/core/ops.rs b/core-models/src/core/ops.rs
index c99038e..30ab65e 100644
--- a/core-models/src/core/ops.rs
+++ b/core-models/src/core/ops.rs
@@ -242,18 +242,18 @@ pub mod function {
     } */
 }
 
-mod try_trait {
+pub mod try_trait {
     /// See [`std::ops::FromResidual`]
     trait FromResidual<R> {
         fn from_residual(x: R) -> Self;
     }
 
     /// See [`std::ops::Try`]
-    trait Try {
+    pub trait Try {
         type Output;
         type Residual;
         fn from_output(x: Self::Output) -> Self;
-        fn branch(&self) -> super::control_flow::ControlFlow<Self::Residual, Self::Output>;
+        fn branch(self) -> super::control_flow::ControlFlow<Self::Residual, Self::Output>;
     }
 }
 
diff --git a/core-models/src/core/option.rs b/core-models/src/core/option.rs
index 47d79b5..a59ed01 100644
--- a/core-models/src/core/option.rs
+++ b/core-models/src/core/option.rs
@@ -254,6 +254,25 @@ impl<T> Default for Option<T> {
     }
 }
 
+impl<T: super::clone::Clone> super::clone::Clone for Option<T> {
+    fn clone(self) -> Self {
+        match self {
+            Self::Some(arg0) => Self::Some(arg0.clone()),
+            Self::None => Self::None,
+        }
+    }
+}
+
+impl<T: super::cmp::PartialEq<T>> super::cmp::PartialEq<Option<T>> for Option<T> {
+    fn eq(&self, other: &Self) -> bool {
+        match (self, other) {
+            (Self::Some(a), Self::Some(b)) => a.eq(b),
+            (Self::None, Self::None) => true,
+            _ => false,
+        }
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use crate::testing::Inject;
@@ -409,6 +428,25 @@ mod tests {
             prop_assert!(remaining_model == remaining_std.inject());
             prop_assert!(taken_model == taken_std.inject());
         }
+
+        #[test]
+        fn test_option_eq(x in any::<Option<u8>>(), y in any::<Option<u8>>()) {
+            prop_assert_eq!(
+                <super::Option<u8> as crate::cmp::PartialEq<super::Option<u8>>>::eq(
+                    &x.inject(), &y.inject()
+                ),
+                x == y
+            );
+        }
+
+        #[test]
+        fn test_option_clone(x in any::<Option<u8>>()) {
+            // `core_models`' `Clone::clone` takes `self` by value.
+            prop_assert_eq!(
+                <super::Option<u8> as crate::clone::Clone>::clone(x.inject()),
+                x.clone().inject()
+            );
+        }
     }
 
     #[test]
diff --git a/core-models/src/core/result.rs b/core-models/src/core/result.rs
index b8e0ebe..026f2f1 100644
--- a/core-models/src/core/result.rs
+++ b/core-models/src/core/result.rs
@@ -283,6 +283,42 @@ impl<T, E> Result<Result<T, E>, E> {
     }
 }
 
+/// Models the std impl `FromIterator<Result<A, E>> for Result<V, E>`: collect
+/// an iterator of `Result`s into a `Result` of a collection, short-circuiting
+/// on the first `Err`.
+///
+/// Opaque: our `FromIterator::from_iter` signature deliberately omits the
+/// `Item = ...` bound (to avoid the associated-type constraint), so the
+/// short-circuiting body cannot be written in terms of the iterator's items;
+/// the behaviour is axiomatised. The body below exists only to typecheck —
+/// it delegates to `V`'s own `from_iter`.
+#[hax_lib::opaque]
+impl<A, E, V: crate::iter::traits::collect::FromIterator<A>>
+    crate::iter::traits::collect::FromIterator<Result<A, E>> for Result<V, E>
+{
+    fn from_iter<T: crate::iter::traits::collect::IntoIterator>(iter: T) -> Result<V, E> {
+        Ok(<V as crate::iter::traits::collect::FromIterator<A>>::from_iter(iter))
+    }
+}
+
+impl<T, E> crate::ops::try_trait::Try for Result<T, E> {
+    type Output = T;
+    type Residual = Result<crate::convert::Infallible, E>;
+
+    #[inline]
+    fn from_output(output: Self::Output) -> Self {
+        Ok(output)
+    }
+
+    #[inline]
+    fn branch(self) -> crate::ops::control_flow::ControlFlow<Self::Residual, Self::Output> {
+        match self {
+            Ok(v) => crate::ops::control_flow::ControlFlow::Continue(v),
+            Err(e) => crate::ops::control_flow::ControlFlow::Break(Err(e)),
+        }
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use crate::testing::Inject;
@@ -444,5 +480,43 @@ mod tests {
         fn test_flatten(x in any::<Result<Result<u8, u8>, u8>>(), is_ok in any::<bool>()) {
             prop_assert!(x.inject().flatten() == x.flatten().inject());
         }
+
+        // ----- Try (from_output / branch) -----------------------------------
+        // std's `Try` is unstable, so these pin the model's documented
+        // semantics (which mirror `?`): `from_output` injects into `Ok`,
+        // `branch` sends `Ok(v)` to `Continue(v)` and `Err(e)` to `Break(Err(e))`.
+
+        #[test]
+        fn test_try_from_output(v in any::<u8>()) {
+            use crate::ops::try_trait::Try;
+            prop_assert_eq!(
+                <super::Result<u8, u8> as Try>::from_output(v),
+                super::Result::Ok(v)
+            );
+        }
+
+        #[test]
+        fn test_try_branch_ok(v in any::<u8>()) {
+            use crate::ops::try_trait::Try;
+            use crate::ops::control_flow::ControlFlow;
+            let r: super::Result<u8, u8> = super::Result::Ok(v);
+            match r.branch() {
+                ControlFlow::Continue(c) => prop_assert_eq!(c, v),
+                ControlFlow::Break(_) => prop_assert!(false, "Ok should Continue"),
+            }
+        }
+
+        #[test]
+        fn test_try_branch_err(e in any::<u8>()) {
+            use crate::ops::try_trait::Try;
+            use crate::ops::control_flow::ControlFlow;
+            let r: super::Result<u8, u8> = super::Result::Err(e);
+            match r.branch() {
+                // `Break` carries the residual `Result<Infallible, u8>`; match
+                // the `Err` arm to read the error without needing `Infallible: Eq`.
+                ControlFlow::Break(super::Result::Err(ee)) => prop_assert_eq!(ee, e),
+                _ => prop_assert!(false, "Err should Break(Err(e))"),
+            }
+        }
     }
 }
diff --git a/core-models/src/core/slice.rs b/core-models/src/core/slice.rs
index 80afcb8..fe1c6f2 100644
--- a/core-models/src/core/slice.rs
+++ b/core-models/src/core/slice.rs
@@ -2,7 +2,7 @@ use crate::result::Result;
 
 // Dummy type to allow impls
 #[hax_lib::exclude]
-struct Slice<T>(T);
+struct Slice<T>([T]);
 
 pub mod iter {
     use crate::option::Option;
@@ -252,6 +252,76 @@ impl<T> Slice<T> {
     }
 }
 
+impl<U, T: crate::cmp::PartialEq<U>> crate::cmp::PartialEq<[U]> for [T] {
+    fn eq(&self, other: &[U]) -> bool {
+        if self.len() != other.len() {
+            false
+        } else {
+            let mut res = true;
+            for i in 0..self.len() {
+                if !self[i].eq(&other[i]) {
+                    res = false;
+                }
+            }
+            res
+        }
+    }
+}
+
+impl<T: crate::cmp::Eq> crate::cmp::Eq for [T] {}
+
+impl<T: crate::cmp::PartialOrd<T>> crate::cmp::PartialOrd<[T]> for [T] {
+    fn partial_cmp(&self, other: &[T]) -> crate::option::Option<crate::cmp::Ordering> {
+        // Lexicographic order: compare elements pairwise up to the shorter
+        // length; the first non-`Equal` result (including `None`) decides.
+        let l = if self.len() < other.len() {
+            self.len()
+        } else {
+            other.len()
+        };
+        for i in 0..l {
+            match self[i].partial_cmp(&other[i]) {
+                crate::option::Option::Some(crate::cmp::Ordering::Equal) => (),
+                non_eq => return non_eq,
+            }
+        }
+        // All common elements are equal: the shorter slice is smaller.
+        if self.len() < other.len() {
+            crate::option::Option::Some(crate::cmp::Ordering::Less)
+        } else if self.len() > other.len() {
+            crate::option::Option::Some(crate::cmp::Ordering::Greater)
+        } else {
+            crate::option::Option::Some(crate::cmp::Ordering::Equal)
+        }
+    }
+}
+
+impl<T: crate::cmp::Ord> crate::cmp::Ord for [T] {
+    fn cmp(&self, other: &[T]) -> crate::cmp::Ordering {
+        // Lexicographic order: compare elements pairwise up to the shorter
+        // length; the first non-`Equal` result decides.
+        let l = if self.len() < other.len() {
+            self.len()
+        } else {
+            other.len()
+        };
+        for i in 0..l {
+            match self[i].cmp(&other[i]) {
+                crate::cmp::Ordering::Equal => (),
+                non_eq => return non_eq,
+            }
+        }
+        // All common elements are equal: the shorter slice is smaller.
+        if self.len() < other.len() {
+            crate::cmp::Ordering::Less
+        } else if self.len() > other.len() {
+            crate::cmp::Ordering::Greater
+        } else {
+            crate::cmp::Ordering::Equal
+        }
+    }
+}
+
 #[hax_lib::attributes]
 #[cfg_attr(hax_backend_lean, hax_lib::exclude)]
 #[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/805
@@ -647,5 +717,52 @@ mod tests {
                 &slice[..]
             );
         }
+
+        // ----- PartialEq / PartialOrd / Ord (lexicographic) ------------------
+
+        #[test]
+        fn test_slice_eq(
+            a in prop::collection::vec(any::<u8>(), 0..=8),
+            b in prop::collection::vec(any::<u8>(), 0..=8),
+        ) {
+            prop_assert_eq!(
+                <[u8] as crate::cmp::PartialEq<[u8]>>::eq(&a[..], &b[..]),
+                a == b
+            );
+        }
+
+        // Equal-length pairs make the per-element comparison the deciding factor
+        // more often than two independent (usually different-length) slices.
+        #[test]
+        fn test_slice_eq_same_len(pairs in prop::collection::vec((any::<u8>(), any::<u8>()), 0..=8)) {
+            let a: Vec<u8> = pairs.iter().map(|p| p.0).collect();
+            let b: Vec<u8> = pairs.iter().map(|p| p.1).collect();
+            prop_assert_eq!(
+                <[u8] as crate::cmp::PartialEq<[u8]>>::eq(&a[..], &b[..]),
+                a == b
+            );
+        }
+
+        #[test]
+        fn test_slice_partial_cmp(
+            a in prop::collection::vec(any::<u8>(), 0..=8),
+            b in prop::collection::vec(any::<u8>(), 0..=8),
+        ) {
+            prop_assert_eq!(
+                <[u8] as crate::cmp::PartialOrd<[u8]>>::partial_cmp(&a[..], &b[..]),
+                a[..].partial_cmp(&b[..]).inject()
+            );
+        }
+
+        #[test]
+        fn test_slice_cmp(
+            a in prop::collection::vec(any::<u8>(), 0..=8),
+            b in prop::collection::vec(any::<u8>(), 0..=8),
+        ) {
+            prop_assert_eq!(
+                <[u8] as crate::cmp::Ord>::cmp(&a[..], &b[..]),
+                a[..].cmp(&b[..]).inject()
+            );
+        }
     }
 }
diff --git a/lean/CoreModels/Alloc/Funs.lean b/lean/CoreModels/Alloc/Funs.lean
index 6cf93bf..b6bf4b9 100644
--- a/lean/CoreModels/Alloc/Funs.lean
+++ b/lean/CoreModels/Alloc/Funs.lean
@@ -23,32 +23,60 @@ set_option maxRecDepth 2048
 
 namespace CoreModels.alloc
 
+/-- [alloc::alloc::{impl core::clone::Clone for alloc::alloc::Global}::clone]:
+    Source: 'src/lib.rs', lines 17:13-17:18
+    Visibility: public -/
+def alloc.Global.Insts.CoreCloneClone.clone
+  (self : alloc.Global) : Result alloc.Global := do
+  ok ()
+
+/-- Trait implementation: [alloc::alloc::{impl core::clone::Clone for alloc::alloc::Global}]
+    Source: 'src/lib.rs', lines 17:13-17:18 -/
+@[reducible]
+def alloc.Global.Insts.CoreCloneClone : core.clone.Clone alloc.Global := {
+  clone := alloc.Global.Insts.CoreCloneClone.clone
+}
+
+/-- [alloc::alloc::{impl alloc::alloc::Allocator for alloc::alloc::Global}::dummy]:
+    Source: 'src/lib.rs', lines 21:8-21:21
+    Visibility: public -/
+def alloc.Global.Insts.AllocAllocAllocator.dummy : Result Unit := do
+  ok ()
+
+/-- Trait implementation: [alloc::alloc::{impl alloc::alloc::Allocator for alloc::alloc::Global}]
+    Source: 'src/lib.rs', lines 20:4-22:5 -/
+@[reducible]
+def alloc.Global.Insts.AllocAllocAllocator : alloc.Allocator
+  alloc.Global := {
+  dummy := alloc.Global.Insts.AllocAllocAllocator.dummy
+}
+
 /-- [alloc::borrow::{impl alloc::borrow::ToOwned for T}::to_owned]:
-    Source: 'src/lib.rs', lines 23:8-25:9
+    Source: 'src/lib.rs', lines 32:8-34:9
     Visibility: public -/
 def borrow.ToOwned.Blanket.to_owned {T : Type} (self : T) : Result T := do
   ok self
 
 /-- Trait implementation: [alloc::borrow::{impl alloc::borrow::ToOwned for T}]
-    Source: 'src/lib.rs', lines 22:4-26:5 -/
+    Source: 'src/lib.rs', lines 31:4-35:5 -/
 @[reducible]
 def borrow.ToOwned.Blanket (T : Type) : borrow.ToOwned T := {
   to_owned := borrow.ToOwned.Blanket.to_owned
 }
 
 /-- [alloc::boxed::{alloc::boxed::Box<T>}::new]:
-    Source: 'src/lib.rs', lines 33:8-35:9 -/
+    Source: 'src/lib.rs', lines 42:8-44:9 -/
 def boxed.Box.new {T : Type} (v : T) : Result T := do
   ok v
 
 /-- [alloc::collections::btree::set::{alloc::collections::btree::set::BTreeSet<T, U>}::new]:
-    Source: 'src/lib.rs', lines 180:16-182:17 -/
+    Source: 'src/lib.rs', lines 189:16-191:17 -/
 def collections.btree.set.BTreeSet.new
   (T : Type) (U : Type) : Result (collections.btree.set.BTreeSet T U) := do
   ok (core.option.Option.None, core.option.Option.None)
 
 /-- [alloc::collections::vec_deque::{alloc::collections::vec_deque::VecDeque<T, A>}::push_back]:
-    Source: 'src/lib.rs', lines 198:12-198:44 -/
+    Source: 'src/lib.rs', lines 207:12-207:44 -/
 def collections.vec_deque.VecDeque.push_back
   {T : Type} {A : Type} (self : collections.vec_deque.VecDeque T A) (x : T) :
   Result (collections.vec_deque.VecDeque T A)
@@ -56,7 +84,7 @@ def collections.vec_deque.VecDeque.push_back
   ok self
 
 /-- [alloc::collections::vec_deque::{alloc::collections::vec_deque::VecDeque<T, A>}::len]:
-    Source: 'src/lib.rs', lines 199:12-201:13 -/
+    Source: 'src/lib.rs', lines 208:12-210:13 -/
 def collections.vec_deque.VecDeque.len
   {T : Type} {A : Type} (self : collections.vec_deque.VecDeque T A) :
   Result Std.Usize
@@ -65,7 +93,7 @@ def collections.vec_deque.VecDeque.len
   rust_primitives.sequence.seq_len s
 
 /-- [alloc::collections::vec_deque::{alloc::collections::vec_deque::VecDeque<T, A>}::pop_front]:
-    Source: 'src/lib.rs', lines 202:12-208:13 -/
+    Source: 'src/lib.rs', lines 211:12-217:13 -/
 def collections.vec_deque.VecDeque.pop_front
   {T : Type} {A : Type} (self : collections.vec_deque.VecDeque T A) :
   Result ((core.option.Option T) × (collections.vec_deque.VecDeque T A))
@@ -79,7 +107,7 @@ def collections.vec_deque.VecDeque.pop_front
     ok (core.option.Option.Some t, (s1, pd))
 
 /-- [alloc::collections::vec_deque::{impl core::ops::index::Index<usize, T> for alloc::collections::vec_deque::VecDeque<T, A>}::index]:
-    Source: 'src/lib.rs', lines 215:12-217:13
+    Source: 'src/lib.rs', lines 224:12-226:13
     Visibility: public -/
 def collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT.index
   {T : Type} {A : Type} (self : collections.vec_deque.VecDeque T A)
@@ -90,7 +118,7 @@ def collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT.index
   rust_primitives.sequence.seq_index s i
 
 /-- Trait implementation: [alloc::collections::vec_deque::{impl core::ops::index::Index<usize, T> for alloc::collections::vec_deque::VecDeque<T, A>}]
-    Source: 'src/lib.rs', lines 212:8-218:9 -/
+    Source: 'src/lib.rs', lines 221:8-227:9 -/
 @[reducible]
 def collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT (T : Type) (A
   : Type) : core.ops.index.Index (collections.vec_deque.VecDeque T A) Std.Usize
@@ -98,194 +126,406 @@ def collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT (T : Type) (A
   index := collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT.index
 }
 
+/-- [alloc::collections::vec_deque::into_iter::{impl core::iter::traits::iterator::Iterator<T> for alloc::collections::vec_deque::into_iter::IntoIter<T, A>}::next]:
+    Source: 'src/lib.rs', lines 234:16-240:17
+    Visibility: public -/
+def
+  collections.vec_deque.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next
+  {T : Type} {A : Type} (self : collections.vec_deque.into_iter.IntoIter T A) :
+  Result ((core.option.Option T) × (collections.vec_deque.into_iter.IntoIter T
+    A))
+  := do
+  let (s, pd) := self
+  let i ← rust_primitives.sequence.seq_len s
+  if i = 0#usize
+  then ok (core.option.Option.None, self)
+  else
+    let (t, s1) ← rust_primitives.sequence.seq_remove s 0#usize
+    ok (core.option.Option.Some t, (s1, pd))
+
+/-- Trait implementation: [alloc::collections::vec_deque::into_iter::{impl core::iter::traits::iterator::Iterator<T> for alloc::collections::vec_deque::into_iter::IntoIter<T, A>}]
+    Source: 'src/lib.rs', lines 232:12-241:13 -/
+@[reducible]
+def
+  collections.vec_deque.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator
+  (T : Type) (A : Type) : core.iter.traits.iterator.Iterator
+  (collections.vec_deque.into_iter.IntoIter T A) T := {
+  next :=
+    collections.vec_deque.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next
+}
+
+/-- [alloc::collections::vec_deque::{impl core::iter::traits::collect::IntoIterator<T, alloc::collections::vec_deque::into_iter::IntoIter<T, A>> for alloc::collections::vec_deque::VecDeque<T, A>}::into_iter]:
+    Source: 'src/lib.rs', lines 247:12-249:13
+    Visibility: public -/
+def
+  collections.vec_deque.VecDeque.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter.into_iter
+  {T : Type} {A : Type} (self : collections.vec_deque.VecDeque T A) :
+  Result (collections.vec_deque.into_iter.IntoIter T A)
+  := do
+  let (s, _) := self
+  ok (s, core.marker.PhantomData.mk)
+
+/-- Trait implementation: [alloc::collections::vec_deque::{impl core::iter::traits::collect::IntoIterator<T, alloc::collections::vec_deque::into_iter::IntoIter<T, A>> for alloc::collections::vec_deque::VecDeque<T, A>}]
+    Source: 'src/lib.rs', lines 244:8-250:9 -/
+@[reducible]
+def
+  collections.vec_deque.VecDeque.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter
+  (T : Type) (A : Type) : core.iter.traits.collect.IntoIterator
+  (collections.vec_deque.VecDeque T A) T
+  (collections.vec_deque.into_iter.IntoIter T A) := {
+  into_iter :=
+    collections.vec_deque.VecDeque.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter.into_iter
+}
+
 /-- [alloc::fmt::format]:
-    Source: 'src/lib.rs', lines 224:4-226:5 -/
+    Source: 'src/lib.rs', lines 279:4-281:5 -/
 def fmt.format (args : core.fmt.Arguments) : Result alloc.string.String := do
   alloc.string.String.new
 
 /-- [alloc::slice::{alloc::slice::Dummy<T>}::to_vec]:
-    Source: 'src/lib.rs', lines 237:8-244:9 -/
+    Source: 'src/lib.rs', lines 292:8-299:9 -/
 def slice.Dummy.to_vec
   {T : Type} (corecloneCloneInst : core.clone.Clone T) (s : Slice T) :
-  Result (vec.Vec T alloc.Global)
+  Result (vec.Vec T)
   := do
   let seq ← rust_primitives.sequence.seq_empty T
   let seq1 ← rust_primitives.sequence.seq_extend corecloneCloneInst seq s
-  ok (seq1, core.marker.PhantomData.mk)
+  ok seq1
 
 /-- [alloc::slice::{alloc::slice::Dummy<T>}::into_vec]:
-    Source: 'src/lib.rs', lines 245:8-247:9 -/
-def slice.Dummy.into_vec
-  {T : Type} (A : Type) (s : Slice T) : Result (vec.Vec T A) := do
+    Source: 'src/lib.rs', lines 300:8-302:9 -/
+def slice.Dummy.into_vec {T : Type} (s : Slice T) : Result (vec.Vec T) := do
   let s1 ← rust_primitives.sequence.seq_from_boxed_slice s
-  ok (s1, core.marker.PhantomData.mk)
+  ok s1
+
+/-- [alloc::vec::{alloc::vec::Vec<T>}::as_slice]:
+    Source: 'src/lib.rs', lines 492:8-494:9
+    Visibility: public -/
+def vec.Vec.as_slice {T : Type} (self : vec.Vec T) : Result (Slice T) := do
+  rust_primitives.sequence.seq_to_slice self
+
+/-- [alloc::vec::{impl core::ops::deref::Deref<[T]> for alloc::vec::Vec<T>}::deref]:
+    Source: 'src/lib.rs', lines 583:8-585:9
+    Visibility: public -/
+def vec.Vec.Insts.CoreOpsDerefDerefSlice.deref
+  {T : Type} (self : vec.Vec T) : Result (Slice T) := do
+  vec.Vec.as_slice self
+
+/-- [alloc::vec::{impl core::clone::Clone for alloc::vec::Vec<T>}::clone]: loop body 0:
+    Source: 'src/lib.rs', lines 398:12-400:13
+    Visibility: public -/
+@[rust_loop_body]
+def vec.Vec.Insts.CoreCloneClone.clone_loop.body
+  {T : Type} (corecloneCloneInst : core.clone.Clone T)
+  (iter_ : core.slice.iter.Iter T) (new_vec : rust_primitives.sequence.Seq T) :
+  Result (ControlFlow ((core.slice.iter.Iter T) ×
+    (rust_primitives.sequence.Seq T)) (rust_primitives.sequence.Seq T))
+  := do
+  let (o, iter1) ←
+    core.slice.iter.Iter.Insts.CoreIterTraitsIteratorIteratorSharedAT.next iter_
+  match o with
+  | core.option.Option.None => ok (done new_vec)
+  | core.option.Option.Some it =>
+    let t ← corecloneCloneInst.clone it
+    let new_vec1 ← rust_primitives.sequence.seq_push new_vec t
+    ok (cont (iter1, new_vec1))
+
+/-- [alloc::vec::{impl core::clone::Clone for alloc::vec::Vec<T>}::clone]: loop 0:
+    Source: 'src/lib.rs', lines 398:12-400:13
+    Visibility: public -/
+@[rust_loop]
+def vec.Vec.Insts.CoreCloneClone.clone_loop
+  {T : Type} (corecloneCloneInst : core.clone.Clone T)
+  (iter_ : core.slice.iter.Iter T) (new_vec : rust_primitives.sequence.Seq T) :
+  Result (rust_primitives.sequence.Seq T)
+  := do
+  loop
+    (fun (iter1, new_vec1) => vec.Vec.Insts.CoreCloneClone.clone_loop.body
+      corecloneCloneInst iter1 new_vec1)
+    (iter_, new_vec)
+
+/-- [alloc::vec::{impl core::clone::Clone for alloc::vec::Vec<T>}::clone]:
+    Source: 'src/lib.rs', lines 396:8-402:9
+    Visibility: public -/
+def vec.Vec.Insts.CoreCloneClone.clone
+  {T : Type} (corecloneCloneInst : core.clone.Clone T) (self : vec.Vec T) :
+  Result (vec.Vec T)
+  := do
+  let new_vec ← rust_primitives.sequence.seq_empty T
+  let s ← vec.Vec.Insts.CoreOpsDerefDerefSlice.deref self
+  let iter ← core.slice.Slice.iter s
+  let new_vec1 ←
+    vec.Vec.Insts.CoreCloneClone.clone_loop corecloneCloneInst iter new_vec
+  ok new_vec1
+
+/-- Trait implementation: [alloc::vec::{impl core::clone::Clone for alloc::vec::Vec<T>}]
+    Source: 'src/lib.rs', lines 395:4-403:5 -/
+@[reducible]
+def vec.Vec.Insts.CoreCloneClone {T : Type} (corecloneCloneInst :
+  core.clone.Clone T) : core.clone.Clone (vec.Vec T) := {
+  clone := vec.Vec.Insts.CoreCloneClone.clone corecloneCloneInst
+}
+
+/-- [alloc::vec::{impl core::ops::index::Index<I, Clause0_Output> for alloc::vec::Vec<T>}::index]:
+    Source: 'src/lib.rs', lines 574:8-576:9
+    Visibility: public -/
+def vec.Vec.Insts.CoreOpsIndexIndex.index
+  {T : Type} {I : Type} {Clause0_Output : Type}
+  (coresliceindexSliceIndexISliceClause0_OutputInst :
+  core.slice.index.SliceIndex I (Slice T) Clause0_Output) (self : vec.Vec T)
+  (i : I) :
+  Result Clause0_Output
+  := do
+  let s ← vec.Vec.Insts.CoreOpsDerefDerefSlice.deref self
+  core.Slice.Insts.CoreOpsIndexIndex.index
+    coresliceindexSliceIndexISliceClause0_OutputInst s i
+
+/-- [alloc::vec::{alloc::vec::Vec<T>}::len]:
+    Source: 'src/lib.rs', lines 466:8-468:9
+    Visibility: public -/
+def vec.Vec.len {T : Type} (self : vec.Vec T) : Result Std.Usize := do
+  rust_primitives.sequence.seq_len self
+
+/-- [alloc::vec::{impl core::cmp::PartialEq<alloc::vec::Vec<U>> for alloc::vec::Vec<T>}::eq]: loop body 0:
+    Source: 'src/lib.rs', lines 413:16-417:17
+    Visibility: public -/
+@[rust_loop_body]
+def vec.Vec.Insts.CoreCmpPartialEqVec.eq_loop.body
+  {T : Type} {U : Type} (corecmpPartialEqInst : core.cmp.PartialEq T U)
+  (self : vec.Vec T) (other : vec.Vec U)
+  (iter_ : core.ops.range.Range Std.Usize) (res : Bool) :
+  Result (ControlFlow ((core.ops.range.Range Std.Usize) × Bool) Bool)
+  := do
+  let (o, iter1) ←
+    core.ops.range.Range.Insts.CoreIterTraitsIteratorIterator.next
+      core.Usize.Insts.CoreIterRangeStep iter_
+  match o with
+  | core.option.Option.None => ok (done res)
+  | core.option.Option.Some i =>
+    let t ←
+      vec.Vec.Insts.CoreOpsIndexIndex.index
+        (core.Usize.Insts.CoreSliceIndexSliceIndexSliceT T) self i
+    let t1 ←
+      vec.Vec.Insts.CoreOpsIndexIndex.index
+        (core.Usize.Insts.CoreSliceIndexSliceIndexSliceT U) other i
+    let b ← corecmpPartialEqInst.eq t t1
+    if b
+    then ok (cont (iter1, res))
+    else ok (cont (iter1, false))
+
+/-- [alloc::vec::{impl core::cmp::PartialEq<alloc::vec::Vec<U>> for alloc::vec::Vec<T>}::eq]: loop 0:
+    Source: 'src/lib.rs', lines 413:16-417:17
+    Visibility: public -/
+@[rust_loop]
+def vec.Vec.Insts.CoreCmpPartialEqVec.eq_loop
+  {T : Type} {U : Type} (corecmpPartialEqInst : core.cmp.PartialEq T U)
+  (iter_ : core.ops.range.Range Std.Usize) (self : vec.Vec T)
+  (other : vec.Vec U) (res : Bool) :
+  Result Bool
+  := do
+  loop
+    (fun (iter1, res1) => vec.Vec.Insts.CoreCmpPartialEqVec.eq_loop.body
+      corecmpPartialEqInst self other iter1 res1)
+    (iter_, res)
+
+/-- [alloc::vec::{impl core::cmp::PartialEq<alloc::vec::Vec<U>> for alloc::vec::Vec<T>}::eq]:
+    Source: 'src/lib.rs', lines 408:8-420:9
+    Visibility: public -/
+def vec.Vec.Insts.CoreCmpPartialEqVec.eq
+  {T : Type} {U : Type} (corecmpPartialEqInst : core.cmp.PartialEq T U)
+  (self : vec.Vec T) (other : vec.Vec U) :
+  Result Bool
+  := do
+  let i ← vec.Vec.len self
+  let i1 ← vec.Vec.len other
+  if i = i1
+  then
+    vec.Vec.Insts.CoreCmpPartialEqVec.eq_loop corecmpPartialEqInst
+      { start := 0#usize, «end» := i } self other true
+  else ok false
+
+/-- Trait implementation: [alloc::vec::{impl core::cmp::PartialEq<alloc::vec::Vec<U>> for alloc::vec::Vec<T>}]
+    Source: 'src/lib.rs', lines 404:4-421:5 -/
+@[reducible]
+def vec.Vec.Insts.CoreCmpPartialEqVec {T : Type} {U : Type}
+  (corecmpPartialEqInst : core.cmp.PartialEq T U) : core.cmp.PartialEq (vec.Vec
+  T) (vec.Vec U) := {
+  eq := vec.Vec.Insts.CoreCmpPartialEqVec.eq corecmpPartialEqInst
+}
+
+/-- [alloc::vec::into_iter::{impl core::iter::traits::iterator::Iterator<T> for alloc::vec::into_iter::IntoIter<T>}::next]:
+    Source: 'src/lib.rs', lines 432:12-438:13
+    Visibility: public -/
+def vec.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next
+  {T : Type} (self : vec.into_iter.IntoIter T) :
+  Result ((core.option.Option T) × (vec.into_iter.IntoIter T))
+  := do
+  let i ← rust_primitives.sequence.seq_len self
+  if i = 0#usize
+  then ok (core.option.Option.None, self)
+  else
+    let (t, s) ← rust_primitives.sequence.seq_remove self 0#usize
+    ok (core.option.Option.Some t, s)
+
+/-- Trait implementation: [alloc::vec::into_iter::{impl core::iter::traits::iterator::Iterator<T> for alloc::vec::into_iter::IntoIter<T>}]
+    Source: 'src/lib.rs', lines 430:8-439:9 -/
+@[reducible]
+def vec.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator (T : Type) :
+  core.iter.traits.iterator.Iterator (vec.into_iter.IntoIter T) T := {
+  next := vec.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next
+}
+
+/-- [alloc::vec::{impl core::iter::traits::collect::IntoIterator<T, alloc::vec::into_iter::IntoIter<T>> for alloc::vec::Vec<T>}::into_iter]:
+    Source: 'src/lib.rs', lines 445:8-447:9
+    Visibility: public -/
+def vec.Vec.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter.into_iter
+  {T : Type} (self : vec.Vec T) : Result (vec.into_iter.IntoIter T) := do
+  ok self
+
+/-- Trait implementation: [alloc::vec::{impl core::iter::traits::collect::IntoIterator<T, alloc::vec::into_iter::IntoIter<T>> for alloc::vec::Vec<T>}]
+    Source: 'src/lib.rs', lines 442:4-448:5 -/
+@[reducible]
+def vec.Vec.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter (T : Type) :
+  core.iter.traits.collect.IntoIterator (vec.Vec T) T (vec.into_iter.IntoIter
+  T) := {
+  into_iter :=
+    vec.Vec.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter.into_iter
+}
 
 /-- [alloc::vec::from_elem]:
-    Source: 'src/lib.rs', lines 349:4-354:5 -/
+    Source: 'src/lib.rs', lines 450:4-452:5 -/
 def vec.from_elem
   {T : Type} (corecloneCloneInst : core.clone.Clone T) (item : T)
   (len : Std.Usize) :
-  Result (vec.Vec T alloc.Global)
+  Result (vec.Vec T)
   := do
   let s ← rust_primitives.sequence.seq_create corecloneCloneInst item len
-  ok (s, core.marker.PhantomData.mk)
+  ok s
 
-/-- [alloc::vec::{alloc::vec::Vec<T, alloc::alloc::Global>}::new]:
-    Source: 'src/lib.rs', lines 358:8-363:9
+/-- [alloc::vec::{alloc::vec::Vec<T>}::new]:
+    Source: 'src/lib.rs', lines 456:8-458:9
     Visibility: public -/
-def vec.VecTGlobal.new (T : Type) : Result (vec.Vec T alloc.Global) := do
+def vec.Vec.new (T : Type) : Result (vec.Vec T) := do
   let s ← rust_primitives.sequence.seq_empty T
-  ok (s, core.marker.PhantomData.mk)
+  ok s
 
-/-- [alloc::vec::{alloc::vec::Vec<T, alloc::alloc::Global>}::with_capacity]:
-    Source: 'src/lib.rs', lines 364:8-366:9
+/-- [alloc::vec::{alloc::vec::Vec<T>}::with_capacity]:
+    Source: 'src/lib.rs', lines 459:8-461:9
     Visibility: public -/
-def vec.VecTGlobal.with_capacity
-  (T : Type) (_c : Std.Usize) : Result (vec.Vec T alloc.Global) := do
-  vec.VecTGlobal.new T
+def vec.Vec.with_capacity
+  (T : Type) (_c : Std.Usize) : Result (vec.Vec T) := do
+  vec.Vec.new T
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::len]:
-    Source: 'src/lib.rs', lines 371:8-373:9
-    Visibility: public -/
-def vec.Vec.len
-  {T : Type} {A : Type} (self : vec.Vec T A) : Result Std.Usize := do
-  let (s, _) := self
-  rust_primitives.sequence.seq_len s
-
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::push]:
-    Source: 'src/lib.rs', lines 375:8-377:9
+/-- [alloc::vec::{alloc::vec::Vec<T>}::push]:
+    Source: 'src/lib.rs', lines 470:8-472:9
     Visibility: public -/
 def vec.Vec.push
-  {T : Type} {A : Type} (self : vec.Vec T A) (x : T) :
-  Result (vec.Vec T A)
-  := do
-  let (s, pd) := self
-  let s1 ← rust_primitives.sequence.seq_push s x
-  ok (s1, pd)
+  {T : Type} (self : vec.Vec T) (x : T) : Result (vec.Vec T) := do
+  let s ← rust_primitives.sequence.seq_push self x
+  ok s
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::pop]:
-    Source: 'src/lib.rs', lines 378:8-386:9
+/-- [alloc::vec::{alloc::vec::Vec<T>}::pop]:
+    Source: 'src/lib.rs', lines 473:8-481:9
     Visibility: public -/
 def vec.Vec.pop
-  {T : Type} {A : Type} (self : vec.Vec T A) :
-  Result ((core.option.Option T) × (vec.Vec T A))
+  {T : Type} (self : vec.Vec T) :
+  Result ((core.option.Option T) × (vec.Vec T))
   := do
-  let (s, pd) := self
-  let l ← rust_primitives.sequence.seq_len s
+  let l ← rust_primitives.sequence.seq_len self
   if l > 0#usize
   then
     let i ← l - 1#usize
-    let (last, s1) ← rust_primitives.sequence.seq_remove s i
-    ok (core.option.Option.Some last, (s1, pd))
+    let (last, s) ← rust_primitives.sequence.seq_remove self i
+    ok (core.option.Option.Some last, s)
   else ok (core.option.Option.None, self)
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::is_empty]:
-    Source: 'src/lib.rs', lines 387:8-389:9
+/-- [alloc::vec::{alloc::vec::Vec<T>}::is_empty]:
+    Source: 'src/lib.rs', lines 482:8-484:9
     Visibility: public -/
-def vec.Vec.is_empty
-  {T : Type} {A : Type} (self : vec.Vec T A) : Result Bool := do
-  let (s, _) := self
-  let i ← rust_primitives.sequence.seq_len s
+def vec.Vec.is_empty {T : Type} (self : vec.Vec T) : Result Bool := do
+  let i ← rust_primitives.sequence.seq_len self
   ok (i = 0#usize)
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::insert]:
-    Source: 'src/lib.rs', lines 391:8-396:9
+/-- [alloc::vec::{alloc::vec::Vec<T>}::insert]:
+    Source: 'src/lib.rs', lines 486:8-491:9
     Visibility: public -/
 def vec.Vec.insert
-  {T : Type} {A : Type} (self : vec.Vec T A) (index : Std.Usize) (element : T)
-  :
-  Result (vec.Vec T A)
+  {T : Type} (self : vec.Vec T) (index : Std.Usize) (element : T) :
+  Result (vec.Vec T)
   := do
-  let (s, pd) := self
-  let l ← rust_primitives.sequence.seq_len s
-  let (right, s1) ← rust_primitives.sequence.seq_drain s index l
-  let s2 ← rust_primitives.sequence.seq_push s1 element
-  let (s3, _) ← rust_primitives.sequence.seq_concat s2 right
-  ok (s3, pd)
-
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::as_slice]:
-    Source: 'src/lib.rs', lines 397:8-399:9
-    Visibility: public -/
-def vec.Vec.as_slice
-  {T : Type} {A : Type} (self : vec.Vec T A) : Result (Slice T) := do
-  let (s, _) := self
-  rust_primitives.sequence.seq_to_slice s
-
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::truncate]:
-    Source: 'src/lib.rs', lines 401:8-401:47
+  let l ← rust_primitives.sequence.seq_len self
+  let (right, s) ← rust_primitives.sequence.seq_drain self index l
+  let s1 ← rust_primitives.sequence.seq_push s element
+  let (s2, _) ← rust_primitives.sequence.seq_concat s1 right
+  ok s2
+
+/-- [alloc::vec::{alloc::vec::Vec<T>}::truncate]:
+    Source: 'src/lib.rs', lines 496:8-496:47
     Visibility: public -/
 def vec.Vec.truncate
-  {T : Type} {A : Type} (self : vec.Vec T A) (n : Std.Usize) :
-  Result (vec.Vec T A)
-  := do
+  {T : Type} (self : vec.Vec T) (n : Std.Usize) : Result (vec.Vec T) := do
   ok self
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::swap_remove]:
-    Source: 'src/lib.rs', lines 403:8-405:9
+/-- [alloc::vec::{alloc::vec::Vec<T>}::swap_remove]:
+    Source: 'src/lib.rs', lines 498:8-500:9
     Visibility: public -/
 def vec.Vec.swap_remove
-  {T : Type} {A : Type} (self : vec.Vec T A) (n : Std.Usize) :
-  Result (T × (vec.Vec T A))
+  {T : Type} (self : vec.Vec T) (n : Std.Usize) :
+  Result (T × (vec.Vec T))
   := do
-  let (s, pd) := self
-  let (t, s1) ← rust_primitives.sequence.seq_remove s n
-  ok (t, (s1, pd))
+  let (t, s) ← rust_primitives.sequence.seq_remove self n
+  ok (t, s)
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::resize]:
-    Source: 'src/lib.rs', lines 408:8-408:63
+/-- [alloc::vec::{alloc::vec::Vec<T>}::resize]:
+    Source: 'src/lib.rs', lines 503:8-507:9
     Visibility: public -/
 def vec.Vec.resize
-  {T : Type} {A : Type} (self : vec.Vec T A) (new_size : Std.Usize) (value : T)
-  :
-  Result (vec.Vec T A)
+  {T : Type} (corecloneCloneInst : core.clone.Clone T) (self : vec.Vec T)
+  (new_size : Std.Usize) (value : T) :
+  Result (vec.Vec T)
   := do
   ok self
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::remove]:
-    Source: 'src/lib.rs', lines 410:8-412:9
+/-- [alloc::vec::{alloc::vec::Vec<T>}::remove]:
+    Source: 'src/lib.rs', lines 509:8-511:9
     Visibility: public -/
 def vec.Vec.remove
-  {T : Type} {A : Type} (self : vec.Vec T A) (index : Std.Usize) :
-  Result (T × (vec.Vec T A))
+  {T : Type} (self : vec.Vec T) (index : Std.Usize) :
+  Result (T × (vec.Vec T))
   := do
-  let (s, pd) := self
-  let (t, s1) ← rust_primitives.sequence.seq_remove s index
-  ok (t, (s1, pd))
+  let (t, s) ← rust_primitives.sequence.seq_remove self index
+  ok (t, s)
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::clear]:
-    Source: 'src/lib.rs', lines 414:8-414:34
+/-- [alloc::vec::{alloc::vec::Vec<T>}::clear]:
+    Source: 'src/lib.rs', lines 513:8-513:34
     Visibility: public -/
-def vec.Vec.clear
-  {T : Type} {A : Type} (self : vec.Vec T A) : Result (vec.Vec T A) := do
+def vec.Vec.clear {T : Type} (self : vec.Vec T) : Result (vec.Vec T) := do
   ok self
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::append]:
-    Source: 'src/lib.rs', lines 416:8-419:9
+/-- [alloc::vec::{alloc::vec::Vec<T>}::append]:
+    Source: 'src/lib.rs', lines 515:8-518:9
     Visibility: public -/
 def vec.Vec.append
-  {T : Type} {A : Type} (self : vec.Vec T A) (other : vec.Vec T A) :
-  Result ((vec.Vec T A) × (vec.Vec T A))
+  {T : Type} (self : vec.Vec T) (other : vec.Vec T) :
+  Result ((vec.Vec T) × (vec.Vec T))
   := do
-  let (s, pd) := self
-  let (s1, pd1) := other
-  let (s2, _) ← rust_primitives.sequence.seq_concat s s1
-  let s3 ← rust_primitives.sequence.seq_empty T
-  ok ((s2, pd), (s3, pd1))
+  let (s, _) ← rust_primitives.sequence.seq_concat self other
+  let s1 ← rust_primitives.sequence.seq_empty T
+  ok (s, s1)
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::drain]:
-    Source: 'src/lib.rs', lines 421:8-424:9
+/-- [alloc::vec::{alloc::vec::Vec<T>}::drain]:
+    Source: 'src/lib.rs', lines 520:8-529:9
     Visibility: public -/
 def vec.Vec.drain
-  {T : Type} {A : Type} {R : Type} (self : vec.Vec T A) (_range : R) :
-  Result ((vec.drain.Drain T A) × (vec.Vec T A))
+  {T : Type} {R : Type} (self : vec.Vec T) (_range : R) :
+  Result ((vec.drain.Drain T alloc.Global) × (vec.Vec T))
   := do
-  let (s, pd) := self
-  let l ← rust_primitives.sequence.seq_len s
-  let (s1, s2) ← rust_primitives.sequence.seq_drain s 0#usize l
-  ok ((s1, core.marker.PhantomData.mk), (s2, pd))
+  let l ← rust_primitives.sequence.seq_len self
+  let (s, s1) ← rust_primitives.sequence.seq_drain self 0#usize l
+  ok ((s, core.marker.PhantomData.mk), s1)
 
 /-- [alloc::vec::drain::{impl core::iter::traits::iterator::Iterator<T> for alloc::vec::drain::Drain<T, A>}::next]:
-    Source: 'src/lib.rs', lines 431:12-438:13
+    Source: 'src/lib.rs', lines 536:12-543:13
     Visibility: public -/
 def vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator.next
   {T : Type} {A : Type} (self : vec.drain.Drain T A) :
@@ -300,36 +540,39 @@ def vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator.next
     ok (core.option.Option.Some res, (s1, pd))
 
 /-- Trait implementation: [alloc::vec::drain::{impl core::iter::traits::iterator::Iterator<T> for alloc::vec::drain::Drain<T, A>}]
-    Source: 'src/lib.rs', lines 429:8-439:9 -/
+    Source: 'src/lib.rs', lines 534:8-544:9 -/
 @[reducible]
 def vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator (T : Type) (A : Type)
   : core.iter.traits.iterator.Iterator (vec.drain.Drain T A) T := {
   next := vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator.next
 }
 
-/-- [alloc::vec::{alloc::vec::Vec<T, A>}::extend_from_slice]:
-    Source: 'src/lib.rs', lines 445:8-447:9 -/
+/-- [alloc::vec::{alloc::vec::Vec<T>}::extend_from_slice]:
+    Source: 'src/lib.rs', lines 550:8-552:9 -/
 def vec.Vec.extend_from_slice
-  {T : Type} {A : Type} (corecloneCloneInst : core.clone.Clone T)
-  (self : vec.Vec T A) (other : Slice T) :
-  Result (vec.Vec T A)
+  {T : Type} (corecloneCloneInst : core.clone.Clone T) (self : vec.Vec T)
+  (other : Slice T) :
+  Result (vec.Vec T)
   := do
-  let (s, pd) := self
-  let s1 ← rust_primitives.sequence.seq_extend corecloneCloneInst s other
-  ok (s1, pd)
+  let s ← rust_primitives.sequence.seq_extend corecloneCloneInst self other
+  ok s
 
-/-- [alloc::vec::{impl core::ops::deref::Deref<[T]> for alloc::vec::Vec<T, A>}::deref]:
-    Source: 'src/lib.rs', lines 478:8-480:9
-    Visibility: public -/
-def vec.Vec.Insts.CoreOpsDerefDerefSlice.deref
-  {T : Type} {A : Type} (self : vec.Vec T A) : Result (Slice T) := do
-  vec.Vec.as_slice self
+/-- Trait implementation: [alloc::vec::{impl core::ops::index::Index<I, Clause0_Output> for alloc::vec::Vec<T>}]
+    Source: 'src/lib.rs', lines 568:4-577:5 -/
+@[reducible]
+def vec.Vec.Insts.CoreOpsIndexIndex {T : Type} {I : Type} {Clause0_Output :
+  Type} (coresliceindexSliceIndexISliceClause0_OutputInst :
+  core.slice.index.SliceIndex I (Slice T) Clause0_Output) :
+  core.ops.index.Index (vec.Vec T) I Clause0_Output := {
+  index := vec.Vec.Insts.CoreOpsIndexIndex.index
+    coresliceindexSliceIndexISliceClause0_OutputInst
+}
 
-/-- Trait implementation: [alloc::vec::{impl core::ops::deref::Deref<[T]> for alloc::vec::Vec<T, A>}]
-    Source: 'src/lib.rs', lines 475:4-481:5 -/
+/-- Trait implementation: [alloc::vec::{impl core::ops::deref::Deref<[T]> for alloc::vec::Vec<T>}]
+    Source: 'src/lib.rs', lines 580:4-586:5 -/
 @[reducible]
-def vec.Vec.Insts.CoreOpsDerefDerefSlice (T : Type) (A : Type) :
-  core.ops.deref.Deref (vec.Vec T A) (Slice T) := {
+def vec.Vec.Insts.CoreOpsDerefDerefSlice (T : Type) : core.ops.deref.Deref
+  (vec.Vec T) (Slice T) := {
   deref := vec.Vec.Insts.CoreOpsDerefDerefSlice.deref
 }
 
diff --git a/lean/CoreModels/Alloc/Types.lean b/lean/CoreModels/Alloc/Types.lean
index efbc7a4..c306d23 100644
--- a/lean/CoreModels/Alloc/Types.lean
+++ b/lean/CoreModels/Alloc/Types.lean
@@ -20,61 +20,73 @@ set_option maxRecDepth 2048
 
 namespace CoreModels.alloc
 
+/-- Trait declaration: [alloc::alloc::Allocator]
+    Source: 'src/lib.rs', lines 12:4-14:5
+    Visibility: public -/
+structure alloc.Allocator (Self : Type) where
+  dummy : Result Unit
+
 /-- [alloc::alloc::Global]
-    Source: 'src/lib.rs', lines 13:4-13:22
+    Source: 'src/lib.rs', lines 18:4-18:22
     Visibility: public -/
 @[reducible]
 def alloc.Global := Unit
 
 /-- [alloc::borrow::Cow]
-    Source: 'src/lib.rs', lines 17:4-17:21 -/
+    Source: 'src/lib.rs', lines 26:4-26:21 -/
 @[reducible]
 def borrow.Cow (T : Type) := T
 
 /-- Trait declaration: [alloc::borrow::ToOwned]
-    Source: 'src/lib.rs', lines 19:4-21:5
+    Source: 'src/lib.rs', lines 28:4-30:5
     Visibility: public -/
 structure borrow.ToOwned (Self : Type) where
   to_owned : Self → Result Self
 
 /-- [alloc::boxed::Box]
-    Source: 'src/lib.rs', lines 30:4-30:29
+    Source: 'src/lib.rs', lines 39:4-39:29
     Visibility: public -/
 @[reducible]
 def boxed.Box (T : Type) := T
 
 /-- [alloc::collections::btree::set::BTreeSet]
-    Source: 'src/lib.rs', lines 164:12-164:56 -/
+    Source: 'src/lib.rs', lines 173:12-173:56 -/
 def collections.btree.set.BTreeSet (T : Type) (U : Type) :=
   core.option.Option T × core.option.Option U
 
 /-- [alloc::collections::vec_deque::VecDeque]
-    Source: 'src/lib.rs', lines 188:8-188:75
+    Source: 'src/lib.rs', lines 197:8-197:75
     Visibility: public -/
 def collections.vec_deque.VecDeque (T : Type) (A : Type) :=
   rust_primitives.sequence.Seq T × core.marker.PhantomData A
 
+/-- [alloc::collections::vec_deque::into_iter::IntoIter]
+    Source: 'src/lib.rs', lines 231:12-231:83
+    Visibility: public -/
+def collections.vec_deque.into_iter.IntoIter (T : Type) (A : Type) :=
+  rust_primitives.sequence.Seq T × core.marker.PhantomData A
+
 /-- [alloc::slice::Dummy]
-    Source: 'src/lib.rs', lines 231:4-231:23 -/
+    Source: 'src/lib.rs', lines 286:4-286:23 -/
 @[reducible]
 def slice.Dummy (T : Type) := T
 
 /-- [alloc::vec::Vec]
-    Source: 'src/lib.rs', lines 338:4-338:70
+    Source: 'src/lib.rs', lines 393:4-393:34
     Visibility: public -/
-def vec.Vec (T : Type) (A : Type := alloc.Global) :=
-  rust_primitives.sequence.Seq T × core.marker.PhantomData A
+@[reducible]
+def vec.Vec (T : Type) := rust_primitives.sequence.Seq T
 
 /-- [alloc::vec::into_iter::IntoIter]
-    Source: 'src/lib.rs', lines 346:8-346:79
+    Source: 'src/lib.rs', lines 429:8-429:43
     Visibility: public -/
-def vec.into_iter.IntoIter (T : Type) (A : Type := alloc.Global) :=
-  rust_primitives.sequence.Seq T × core.marker.PhantomData A
+@[reducible]
+def vec.into_iter.IntoIter (T : Type) := rust_primitives.sequence.Seq T
 
 /-- [alloc::vec::drain::Drain]
-    Source: 'src/lib.rs', lines 428:8-428:76
+    Source: 'src/lib.rs', lines 533:8-533:76
     Visibility: public -/
-def vec.drain.Drain (T : Type) (A : Type := alloc.Global) :=
+def vec.drain.Drain (T : Type) (A : Type) :=
   rust_primitives.sequence.Seq T × core.marker.PhantomData A
 
 end CoreModels.alloc
diff --git a/lean/CoreModels/Core/Funs.lean b/lean/CoreModels/Core/Funs.lean
index 17b7afe..b17c7cc 100644
--- a/lean/CoreModels/Core/Funs.lean
+++ b/lean/CoreModels/Core/Funs.lean
@@ -21,10 +21,10 @@ set_option maxRecDepth 2048
 
 namespace CoreModels.core
 
-/-- [core_models::array::{core_models::array::Dummy<T, N>}::map]:
+/-- [core_models::array::{core_models::array::Array<T, N>}::map]:
     Source: 'core-models/src/core/array.rs', lines 37:4-39:5
     Visibility: public -/
-def array.Dummy.map
+def array.Array.map
   {T : Type} {F : Type} {U : Type} {N : Std.Usize}
   (coreopsfunctionFnFTupleTUInst : core.ops.function.Fn F T U) (s : Array T N)
   (f : F) :
@@ -32,67 +32,67 @@ def array.Dummy.map
   := do
   rust_primitives.slice.array_map coreopsfunctionFnFTupleTUInst s f
 
-/-- [core_models::array::{core_models::array::Dummy<T, N>}::as_slice]:
+/-- [core_models::array::{core_models::array::Array<T, N>}::as_slice]:
     Source: 'core-models/src/core/array.rs', lines 41:4-43:5
     Visibility: public -/
-def array.Dummy.as_slice
+def array.Array.as_slice
   {T : Type} {N : Std.Usize} (s : Array T N) : Result (Slice T) := do
   rust_primitives.slice.array_as_slice s
 
-/-- [core_models::array::{core_models::array::Dummy<T, N>}::each_ref::{impl core::ops::function::FnMut<(usize,), &'_ T> for core_models::array::{core_models::array::Dummy<T, N>}::each_ref::closure<'_0, T, N>}::call_mut]:
+/-- [core_models::array::{core_models::array::Array<T, N>}::each_ref::{impl core::ops::function::FnMut<(usize,), &'_ T> for core_models::array::{core_models::array::Array<T, N>}::each_ref::closure<'_0, T, N>}::call_mut]:
     Source: 'core-models/src/core/array.rs', lines 46:22-46:43 -/
 def
-  array.Dummy.each_ref.closure.Insts.CoreOpsFunctionFnMutTupleUsizeSharedT.call_mut
-  {T : Type} {N : Std.Usize} (c : array.Dummy.each_ref.closure T N)
+  array.Array.each_ref.closure.Insts.CoreOpsFunctionFnMutTupleUsizeSharedT.call_mut
+  {T : Type} {N : Std.Usize} (c : array.Array.each_ref.closure T N)
   (tupled_args : Std.Usize) :
-  Result (T × (array.Dummy.each_ref.closure T N))
+  Result (T × (array.Array.each_ref.closure T N))
   := do
   let t ← rust_primitives.slice.array_index c tupled_args
   ok (t, c)
 
-/-- [core_models::array::{core_models::array::Dummy<T, N>}::each_ref::{impl core::ops::function::FnOnce<(usize,), &'_ T> for core_models::array::{core_models::array::Dummy<T, N>}::each_ref::closure<'_0, T, N>}::call_once]:
+/-- [core_models::array::{core_models::array::Array<T, N>}::each_ref::{impl core::ops::function::FnOnce<(usize,), &'_ T> for core_models::array::{core_models::array::Array<T, N>}::each_ref::closure<'_0, T, N>}::call_once]:
     Source: 'core-models/src/core/array.rs', lines 46:22-46:43 -/
 def
-  array.Dummy.each_ref.closure.Insts.CoreOpsFunctionFnOnceTupleUsizeSharedT.call_once
-  {T : Type} {N : Std.Usize} (c : array.Dummy.each_ref.closure T N)
+  array.Array.each_ref.closure.Insts.CoreOpsFunctionFnOnceTupleUsizeSharedT.call_once
+  {T : Type} {N : Std.Usize} (c : array.Array.each_ref.closure T N)
   (i : Std.Usize) :
   Result T
   := do
   let (t, _) ←
-    array.Dummy.each_ref.closure.Insts.CoreOpsFunctionFnMutTupleUsizeSharedT.call_mut
+    array.Array.each_ref.closure.Insts.CoreOpsFunctionFnMutTupleUsizeSharedT.call_mut
       c i
   ok t
 
-/-- Trait implementation: [core_models::array::{core_models::array::Dummy<T, N>}::each_ref::{impl core::ops::function::FnOnce<(usize,), &'_ T> for core_models::array::{core_models::array::Dummy<T, N>}::each_ref::closure<'_0, T, N>}]
+/-- Trait implementation: [core_models::array::{core_models::array::Array<T, N>}::each_ref::{impl core::ops::function::FnOnce<(usize,), &'_ T> for core_models::array::{core_models::array::Array<T, N>}::each_ref::closure<'_0, T, N>}]
     Source: 'core-models/src/core/array.rs', lines 46:22-46:43 -/
 @[reducible]
-def array.Dummy.each_ref.closure.Insts.CoreOpsFunctionFnOnceTupleUsizeSharedT
+def array.Array.each_ref.closure.Insts.CoreOpsFunctionFnOnceTupleUsizeSharedT
   (T : Type) (N : Std.Usize) : core.ops.function.FnOnce
-  (array.Dummy.each_ref.closure T N) Std.Usize T := {
+  (array.Array.each_ref.closure T N) Std.Usize T := {
   call_once :=
-    array.Dummy.each_ref.closure.Insts.CoreOpsFunctionFnOnceTupleUsizeSharedT.call_once
+    array.Array.each_ref.closure.Insts.CoreOpsFunctionFnOnceTupleUsizeSharedT.call_once
 }
 
-/-- Trait implementation: [core_models::array::{core_models::array::Dummy<T, N>}::each_ref::{impl core::ops::function::FnMut<(usize,), &'_ T> for core_models::array::{core_models::array::Dummy<T, N>}::each_ref::closure<'_0, T, N>}]
+/-- Trait implementation: [core_models::array::{core_models::array::Array<T, N>}::each_ref::{impl core::ops::function::FnMut<(usize,), &'_ T> for core_models::array::{core_models::array::Array<T, N>}::each_ref::closure<'_0, T, N>}]
     Source: 'core-models/src/core/array.rs', lines 46:22-46:43 -/
 @[reducible]
-def array.Dummy.each_ref.closure.Insts.CoreOpsFunctionFnMutTupleUsizeSharedT (T
+def array.Array.each_ref.closure.Insts.CoreOpsFunctionFnMutTupleUsizeSharedT (T
   : Type) (N : Std.Usize) : core.ops.function.FnMut
-  (array.Dummy.each_ref.closure T N) Std.Usize T := {
+  (array.Array.each_ref.closure T N) Std.Usize T := {
   FnOnceInst :=
-    array.Dummy.each_ref.closure.Insts.CoreOpsFunctionFnOnceTupleUsizeSharedT T
+    array.Array.each_ref.closure.Insts.CoreOpsFunctionFnOnceTupleUsizeSharedT T
     N
   call_mut :=
-    array.Dummy.each_ref.closure.Insts.CoreOpsFunctionFnMutTupleUsizeSharedT.call_mut
+    array.Array.each_ref.closure.Insts.CoreOpsFunctionFnMutTupleUsizeSharedT.call_mut
 }
 
-/-- [core_models::array::{core_models::array::Dummy<T, N>}::each_ref]:
+/-- [core_models::array::{core_models::array::Array<T, N>}::each_ref]:
     Source: 'core-models/src/core/array.rs', lines 45:4-47:5
     Visibility: public -/
-def array.Dummy.each_ref
+def array.Array.each_ref
   {T : Type} {N : Std.Usize} (s : Array T N) : Result (Array T N) := do
   rust_primitives.slice.array_from_fn N
-    (array.Dummy.each_ref.closure.Insts.CoreOpsFunctionFnMutTupleUsizeSharedT T
+    (array.Array.each_ref.closure.Insts.CoreOpsFunctionFnMutTupleUsizeSharedT T
     N) s
 
 /-- [core_models::array::from_fn]:
@@ -125,99 +125,31 @@ def Array.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter (T : Type) (N
     Array.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter.into_iter
 }
 
-/-- [core_models::array::{impl core_models::ops::index::Index<usize, T> for [T; N]}::index]:
-    Source: 'core-models/src/core/array.rs', lines 77:4-79:5
+/-- [core_models::array::{impl core_models::ops::index::Index<I, Clause0_Output> for [T; N]}::index]:
+    Source: 'core-models/src/core/array.rs', lines 80:4-82:5
     Visibility: public -/
-def Array.Insts.CoreOpsIndexIndexUsizeT.index
-  {T : Type} {N : Std.Usize} (self : Array T N) (i : Std.Usize) :
-  Result T
-  := do
-  rust_primitives.slice.array_index self i
-
-/-- Trait implementation: [core_models::array::{impl core_models::ops::index::Index<usize, T> for [T; N]}]
-    Source: 'core-models/src/core/array.rs', lines 74:0-80:1 -/
-@[reducible]
-def Array.Insts.CoreOpsIndexIndexUsizeT (T : Type) (N : Std.Usize) :
-  ops.index.Index (Array T N) Std.Usize T := {
-  index := Array.Insts.CoreOpsIndexIndexUsizeT.index
-}
-
-/-- [core_models::array::{impl core_models::ops::index::Index<core_models::ops::range::Range<usize>, [T]> for [T; N]}::index]:
-    Source: 'core-models/src/core/array.rs', lines 87:4-89:5
-    Visibility: public -/
-def Array.Insts.CoreOpsIndexIndexRangeUsizeSlice.index
-  {T : Type} {N : Std.Usize} (self : Array T N) (i : ops.range.Range Std.Usize)
-  :
-  Result (Slice T)
-  := do
-  rust_primitives.slice.array_slice self i.start i.«end»
-
-/-- Trait implementation: [core_models::array::{impl core_models::ops::index::Index<core_models::ops::range::Range<usize>, [T]> for [T; N]}]
-    Source: 'core-models/src/core/array.rs', lines 84:0-90:1 -/
-@[reducible]
-def Array.Insts.CoreOpsIndexIndexRangeUsizeSlice (T : Type) (N :
-  Std.Usize) : ops.index.Index (Array T N) (ops.range.Range Std.Usize) (Slice
-  T) := {
-  index := Array.Insts.CoreOpsIndexIndexRangeUsizeSlice.index
-}
-
-/-- [core_models::array::{impl core_models::ops::index::Index<core_models::ops::range::RangeTo<usize>, [T]> for [T; N]}::index]:
-    Source: 'core-models/src/core/array.rs', lines 96:4-98:5
-    Visibility: public -/
-def Array.Insts.CoreOpsIndexIndexRangeToUsizeSlice.index
-  {T : Type} {N : Std.Usize} (self : Array T N)
-  (i : ops.range.RangeTo Std.Usize) :
-  Result (Slice T)
-  := do
-  rust_primitives.slice.array_slice self 0#usize i.«end»
-
-/-- Trait implementation: [core_models::array::{impl core_models::ops::index::Index<core_models::ops::range::RangeTo<usize>, [T]> for [T; N]}]
-    Source: 'core-models/src/core/array.rs', lines 93:0-99:1 -/
-@[reducible]
-def Array.Insts.CoreOpsIndexIndexRangeToUsizeSlice (T : Type) (N :
-  Std.Usize) : ops.index.Index (Array T N) (ops.range.RangeTo Std.Usize) (Slice
-  T) := {
-  index := Array.Insts.CoreOpsIndexIndexRangeToUsizeSlice.index
-}
-
-/-- [core_models::array::{impl core_models::ops::index::Index<core_models::ops::range::RangeFrom<usize>, [T]> for [T; N]}::index]:
-    Source: 'core-models/src/core/array.rs', lines 105:4-107:5
-    Visibility: public -/
-def Array.Insts.CoreOpsIndexIndexRangeFromUsizeSlice.index
-  {T : Type} {N : Std.Usize} (self : Array T N)
-  (i : ops.range.RangeFrom Std.Usize) :
-  Result (Slice T)
-  := do
-  rust_primitives.slice.array_slice self i.start N
-
-/-- Trait implementation: [core_models::array::{impl core_models::ops::index::Index<core_models::ops::range::RangeFrom<usize>, [T]> for [T; N]}]
-    Source: 'core-models/src/core/array.rs', lines 102:0-108:1 -/
-@[reducible]
-def Array.Insts.CoreOpsIndexIndexRangeFromUsizeSlice (T : Type) (N :
-  Std.Usize) : ops.index.Index (Array T N) (ops.range.RangeFrom Std.Usize)
-  (Slice T) := {
-  index := Array.Insts.CoreOpsIndexIndexRangeFromUsizeSlice.index
-}
-
-/-- [core_models::array::{impl core_models::ops::index::Index<core_models::ops::range::RangeFull, [T]> for [T; N]}::index]:
-    Source: 'core-models/src/core/array.rs', lines 113:4-115:5
-    Visibility: public -/
-def Array.Insts.CoreOpsIndexIndexRangeFullSlice.index
-  {T : Type} {N : Std.Usize} (self : Array T N) (i : ops.range.RangeFull) :
-  Result (Slice T)
+def Array.Insts.CoreOpsIndexIndex.index
+  {T : Type} {I : Type} {Clause0_Output : Type} {N : Std.Usize}
+  (opsindexIndexSliceIClause0_OutputInst : ops.index.Index (Slice T) I
+  Clause0_Output) (self : Array T N) (i : I) :
+  Result Clause0_Output
   := do
-  rust_primitives.slice.array_slice self 0#usize N
+  let s ← core.array.Array.as_slice self
+  opsindexIndexSliceIClause0_OutputInst.index s i
 
-/-- Trait implementation: [core_models::array::{impl core_models::ops::index::Index<core_models::ops::range::RangeFull, [T]> for [T; N]}]
-    Source: 'core-models/src/core/array.rs', lines 111:0-116:1 -/
+/-- Trait implementation: [core_models::array::{impl core_models::ops::index::Index<I, Clause0_Output> for [T; N]}]
+    Source: 'core-models/src/core/array.rs', lines 74:0-83:1 -/
 @[reducible]
-def Array.Insts.CoreOpsIndexIndexRangeFullSlice (T : Type) (N :
-  Std.Usize) : ops.index.Index (Array T N) ops.range.RangeFull (Slice T) := {
-  index := Array.Insts.CoreOpsIndexIndexRangeFullSlice.index
+def Array.Insts.CoreOpsIndexIndex {T : Type} {I : Type} {Clause0_Output
+  : Type} (N : Std.Usize) (opsindexIndexSliceIClause0_OutputInst :
+  ops.index.Index (Slice T) I Clause0_Output) : ops.index.Index (Array T N) I
+  Clause0_Output := {
+  index := Array.Insts.CoreOpsIndexIndex.index
+    opsindexIndexSliceIClause0_OutputInst
 }
 
 /-- [core_models::array::{impl core_models::clone::Clone for [T; N]}::clone]:
-    Source: 'core-models/src/core/array.rs', lines 120:4-122:5
+    Source: 'core-models/src/core/array.rs', lines 133:4-135:5
     Visibility: public -/
 def Array.Insts.CoreCloneClone.clone
   {T : Type} {N : Std.Usize} (cloneCloneInst : clone.Clone T)
@@ -227,7 +159,7 @@ def Array.Insts.CoreCloneClone.clone
   ok self
 
 /-- Trait implementation: [core_models::array::{impl core_models::clone::Clone for [T; N]}]
-    Source: 'core-models/src/core/array.rs', lines 119:0-123:1 -/
+    Source: 'core-models/src/core/array.rs', lines 132:0-136:1 -/
 @[reducible]
 def Array.Insts.CoreCloneClone {T : Type} (N : Std.Usize)
   (cloneCloneInst : clone.Clone T) : clone.Clone (Array T N) := {
@@ -235,7 +167,7 @@ def Array.Insts.CoreCloneClone {T : Type} (N : Std.Usize)
 }
 
 /-- [core_models::array::equality::{impl core_models::cmp::PartialEq<[U; N]> for [T; N]}::eq]: loop body 0:
-    Source: 'core-models/src/core/array.rs', lines 131:12-138:9
+    Source: 'core-models/src/core/array.rs', lines 144:12-151:9
     Visibility: public -/
 @[rust_loop_body]
 def Array.Insts.CoreCmpPartialEqArray.eq_loop.body
@@ -255,7 +187,7 @@ def Array.Insts.CoreCmpPartialEqArray.eq_loop.body
   else ok (done true)
 
 /-- [core_models::array::equality::{impl core_models::cmp::PartialEq<[U; N]> for [T; N]}::eq]: loop 0:
-    Source: 'core-models/src/core/array.rs', lines 131:12-138:9
+    Source: 'core-models/src/core/array.rs', lines 144:12-151:9
     Visibility: public -/
 @[rust_loop]
 def Array.Insts.CoreCmpPartialEqArray.eq_loop
@@ -269,7 +201,7 @@ def Array.Insts.CoreCmpPartialEqArray.eq_loop
     i
 
 /-- [core_models::array::equality::{impl core_models::cmp::PartialEq<[U; N]> for [T; N]}::eq]:
-    Source: 'core-models/src/core/array.rs', lines 129:8-138:9
+    Source: 'core-models/src/core/array.rs', lines 142:8-151:9
     Visibility: public -/
 @[reducible]
 def Array.Insts.CoreCmpPartialEqArray.eq
@@ -281,7 +213,7 @@ def Array.Insts.CoreCmpPartialEqArray.eq
     0#usize
 
 /-- Trait implementation: [core_models::array::equality::{impl core_models::cmp::PartialEq<[U; N]> for [T; N]}]
-    Source: 'core-models/src/core/array.rs', lines 128:4-139:5 -/
+    Source: 'core-models/src/core/array.rs', lines 141:4-152:5 -/
 @[reducible]
 def Array.Insts.CoreCmpPartialEqArray {T : Type} {U : Type} (N :
   Std.Usize) (cmpPartialEqInst : cmp.PartialEq T U) : cmp.PartialEq (Array T N)
@@ -290,7 +222,7 @@ def Array.Insts.CoreCmpPartialEqArray {T : Type} {U : Type} (N :
 }
 
 /-- [core_models::array::iter::{impl core_models::iter::traits::iterator::Iterator<T> for core_models::array::iter::IntoIter<T, N>}::next]:
-    Source: 'core-models/src/core/array.rs', lines 149:8-156:9
+    Source: 'core-models/src/core/array.rs', lines 162:8-169:9
     Visibility: public -/
 def array.iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next
   {T : Type} {N : Std.Usize} (self : array.iter.IntoIter T N) :
@@ -304,7 +236,7 @@ def array.iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next
     ok (option.Option.Some res, s)
 
 /-- Trait implementation: [core_models::array::iter::{impl core_models::iter::traits::iterator::Iterator<T> for core_models::array::iter::IntoIter<T, N>}]
-    Source: 'core-models/src/core/array.rs', lines 147:4-157:5 -/
+    Source: 'core-models/src/core/array.rs', lines 160:4-170:5 -/
 @[reducible]
 def array.iter.IntoIter.Insts.CoreIterTraitsIteratorIterator (T : Type)
   (N : Std.Usize) : iter.traits.iterator.Iterator (array.iter.IntoIter T N) T
@@ -3549,24 +3481,33 @@ def Usize.Insts.CoreConvertTryFromIsizeTryFromIntError : convert.TryFrom
 def f32.f32.abs (x : F64) : Result F64 := do
   fail Error.panic
 
-/-- [core_models::fmt::{impl core_models::fmt::Debug for T}::dbg_fmt]:
-    Source: 'core-models/src/core/fmt.rs', lines 28:4-30:5
+/-- [core_models::fmt::{core_models::fmt::Formatter}::write_str]:
+    Source: 'core-models/src/core/fmt.rs', lines 13:4-15:5
     Visibility: public -/
-def fmt.Debug.Blanket.dbg_fmt
+def fmt.Formatter.write_str
+  (self : fmt.Formatter) (data : Str) :
+  Result ((result.Result Unit fmt.Error) × fmt.Formatter)
+  := do
+  ok (result.Result.Ok (), self)
+
+/-- [core_models::fmt::{impl core_models::fmt::Debug for T}::fmt]:
+    Source: 'core-models/src/core/fmt.rs', lines 34:4-36:5
+    Visibility: public -/
+def fmt.Debug.Blanket.fmt
   {T : Type} (self : T) (f : fmt.Formatter) :
   Result ((result.Result Unit fmt.Error) × fmt.Formatter)
   := do
   ok (result.Result.Ok (), f)
 
 /-- Trait implementation: [core_models::fmt::{impl core_models::fmt::Debug for T}]
-    Source: 'core-models/src/core/fmt.rs', lines 27:0-31:1 -/
+    Source: 'core-models/src/core/fmt.rs', lines 33:0-37:1 -/
 @[reducible]
 def fmt.Debug.Blanket (T : Type) : fmt.Debug T := {
-  dbg_fmt := fmt.Debug.Blanket.dbg_fmt
+  fmt := fmt.Debug.Blanket.fmt
 }
 
 /-- [core_models::fmt::{core_models::fmt::Arguments<'a>}::write_fmt]:
-    Source: 'core-models/src/core/fmt.rs', lines 44:4-46:5 -/
+    Source: 'core-models/src/core/fmt.rs', lines 50:4-52:5 -/
 def fmt.Arguments.write_fmt
   (f : fmt.Formatter) (args : fmt.Arguments) :
   Result ((result.Result Unit fmt.Error) × fmt.Formatter)
@@ -3574,41 +3515,41 @@ def fmt.Arguments.write_fmt
   ok (result.Result.Ok (), f)
 
 /-- [core_models::fmt::rt::{core_models::fmt::rt::Argument<'_0>}::new_display]:
-    Source: 'core-models/src/core/fmt.rs', lines 67:8-69:9 -/
+    Source: 'core-models/src/core/fmt.rs', lines 73:8-75:9 -/
 def fmt.rt.Argument.new_display
   {T : Type} (x : T) : Result fmt.rt.Argument := do
   let _ ← panicking.internal.panic fmt.rt.Argument
   ok { ty := (fmt.rt.ArgumentType.Placeholder core.marker.PhantomData.mk) }
 
 /-- [core_models::fmt::rt::{core_models::fmt::rt::Argument<'_0>}::new_debug]:
-    Source: 'core-models/src/core/fmt.rs', lines 71:8-73:9 -/
+    Source: 'core-models/src/core/fmt.rs', lines 77:8-79:9 -/
 def fmt.rt.Argument.new_debug {T : Type} (x : T) : Result fmt.rt.Argument := do
   let _ ← panicking.internal.panic fmt.rt.Argument
   ok { ty := (fmt.rt.ArgumentType.Placeholder core.marker.PhantomData.mk) }
 
 /-- [core_models::fmt::rt::{core_models::fmt::rt::Argument<'_0>}::new_lower_hex]:
-    Source: 'core-models/src/core/fmt.rs', lines 75:8-77:9 -/
+    Source: 'core-models/src/core/fmt.rs', lines 81:8-83:9 -/
 def fmt.rt.Argument.new_lower_hex
   {T : Type} (x : T) : Result fmt.rt.Argument := do
   let _ ← panicking.internal.panic fmt.rt.Argument
   ok { ty := (fmt.rt.ArgumentType.Placeholder core.marker.PhantomData.mk) }
 
 /-- [core_models::fmt::rt::{core_models::fmt::rt::Argument<'a>}::new_binary]:
-    Source: 'core-models/src/core/fmt.rs', lines 81:8-83:9 -/
+    Source: 'core-models/src/core/fmt.rs', lines 87:8-89:9 -/
 def fmt.rt.Argument.new_binary
   {T : Type} (x : T) : Result fmt.rt.Argument := do
   let _ ← panicking.internal.panic fmt.rt.Argument
   ok { ty := (fmt.rt.ArgumentType.Placeholder core.marker.PhantomData.mk) }
 
 /-- [core_models::fmt::rt::{core_models::fmt::rt::Argument<'a>}::new_const]:
-    Source: 'core-models/src/core/fmt.rs', lines 85:8-87:9 -/
+    Source: 'core-models/src/core/fmt.rs', lines 91:8-93:9 -/
 def fmt.rt.Argument.new_const
   {T : Type} {U : Type} (x : T) (y : U) : Result fmt.Arguments := do
   let _ ← panicking.internal.panic fmt.Arguments
   ok ()
 
 /-- [core_models::fmt::rt::{core_models::fmt::rt::Argument<'a>}::new_v1]:
-    Source: 'core-models/src/core/fmt.rs', lines 89:8-91:9 -/
+    Source: 'core-models/src/core/fmt.rs', lines 95:8-97:9 -/
 def fmt.rt.Argument.new_v1
   {T : Type} {U : Type} {V : Type} {W : Type} (x : T) (y : U) (z : V) (t : W) :
   Result fmt.Arguments
@@ -3617,12 +3558,12 @@ def fmt.rt.Argument.new_v1
   ok ()
 
 /-- [core_models::fmt::rt::{core_models::fmt::rt::Argument<'a>}::none]:
-    Source: 'core-models/src/core/fmt.rs', lines 92:8-94:9 -/
+    Source: 'core-models/src/core/fmt.rs', lines 98:8-100:9 -/
 def fmt.rt.Argument.none : Result (Array fmt.rt.Argument 0#usize) := do
   ok (Std.Array.empty fmt.rt.Argument)
 
 /-- [core_models::fmt::rt::{core_models::fmt::rt::Argument<'a>}::new_v1_formatted]:
-    Source: 'core-models/src/core/fmt.rs', lines 96:8-98:9 -/
+    Source: 'core-models/src/core/fmt.rs', lines 102:8-104:9 -/
 def fmt.rt.Argument.new_v1_formatted
   {T : Type} {U : Type} {V : Type} (x : T) (y : U) (z : V) :
   Result fmt.Arguments
@@ -3709,8 +3650,34 @@ def
     traitsiteratorIteratorInst
 }
 
+/-- [core_models::iter::adapters::step_by::{core_models::iter::adapters::step_by::StepBy<I>}::new]:
+    Source: 'core-models/src/core/iter.rs', lines 448:12-450:13
+    Visibility: public -/
+def iter.adapters.step_by.StepBy.new
+  {I : Type} (iter_ : I) (step : Std.Usize) :
+  Result (iter.adapters.step_by.StepBy I)
+  := do
+  ok { iter := iter_, step }
+
+
+
+
+
+
+
+
+
+/-- [core_models::iter::adapters::map::{core_models::iter::adapters::map::Map<I, F>}::new]:
+    Source: 'core-models/src/core/iter.rs', lines 475:12-477:13
+    Visibility: public -/
+def iter.adapters.map.Map.new
+  {I : Type} {F : Type} (iter_ : I) (f : F) :
+  Result (iter.adapters.map.Map I F)
+  := do
+  ok { iter := iter_, f }
+
 /-- [core_models::iter::adapters::map::{impl core_models::iter::traits::iterator::Iterator<O> for core_models::iter::adapters::map::Map<I, F>}::next]:
-    Source: 'core-models/src/core/iter.rs', lines 485:12-490:13
+    Source: 'core-models/src/core/iter.rs', lines 484:12-489:13
     Visibility: public -/
 def iter.adapters.map.Map.Insts.CoreIterTraitsIteratorIterator.next
   {I : Type} {O : Type} {F : Type} {Clause0_Item : Type}
@@ -3727,7 +3694,7 @@ def iter.adapters.map.Map.Insts.CoreIterTraitsIteratorIterator.next
   | option.Option.None => ok (option.Option.None, { self with iter := t })
 
 /-- Trait implementation: [core_models::iter::adapters::map::{impl core_models::iter::traits::iterator::Iterator<O> for core_models::iter::adapters::map::Map<I, F>}]
-    Source: 'core-models/src/core/iter.rs', lines 482:8-491:9 -/
+    Source: 'core-models/src/core/iter.rs', lines 481:8-490:9 -/
 @[reducible]
 def iter.adapters.map.Map.Insts.CoreIterTraitsIteratorIterator {I :
   Type} {O : Type} {F : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst
@@ -3741,7 +3708,7 @@ def iter.adapters.map.Map.Insts.CoreIterTraitsIteratorIterator {I :
 }
 
 /-- [core_models::iter::adapters::take::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::take::Take<I>}::next]:
-    Source: 'core-models/src/core/iter.rs', lines 510:12-517:13
+    Source: 'core-models/src/core/iter.rs', lines 509:12-516:13
     Visibility: public -/
 def iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator.next
   {I : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
@@ -3757,7 +3724,7 @@ def iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator.next
   else ok (option.Option.None, self)
 
 /-- Trait implementation: [core_models::iter::adapters::take::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::take::Take<I>}]
-    Source: 'core-models/src/core/iter.rs', lines 507:8-518:9 -/
+    Source: 'core-models/src/core/iter.rs', lines 506:8-517:9 -/
 @[reducible]
 def iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator {I :
   Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
@@ -3769,7 +3736,7 @@ def iter.adapters.take.Take.Insts.CoreIterTraitsIteratorIterator {I :
 }
 
 /-- [core_models::iter::adapters::flat_map::{core_models::iter::adapters::flat_map::FlatMap<I, U, F>}::new]:
-    Source: 'core-models/src/core/iter.rs', lines 530:12-536:13
+    Source: 'core-models/src/core/iter.rs', lines 529:12-535:13
     Visibility: public -/
 def iter.adapters.flat_map.FlatMap.new
   {I : Type} {U : Type} {F : Type} {Clause0_Item : Type} {Clause1_Item : Type}
@@ -3782,7 +3749,7 @@ def iter.adapters.flat_map.FlatMap.new
   ok { it, f, current := option.Option.None }
 
 /-- [core_models::iter::adapters::flat_map::{impl core_models::iter::traits::iterator::Iterator<Clause1_Item> for core_models::iter::adapters::flat_map::FlatMap<I, U, F>}::next]: loop body 0:
-    Source: 'core-models/src/core/iter.rs', lines 543:20-552:21
+    Source: 'core-models/src/core/iter.rs', lines 542:20-551:21
     Visibility: public -/
 @[rust_loop_body]
 def
@@ -3820,7 +3787,7 @@ def
       ok (done (option.Option.None, t, self.f, option.Option.None))
 
 /-- [core_models::iter::adapters::flat_map::{impl core_models::iter::traits::iterator::Iterator<Clause1_Item> for core_models::iter::adapters::flat_map::FlatMap<I, U, F>}::next]: loop 0:
-    Source: 'core-models/src/core/iter.rs', lines 543:20-552:21
+    Source: 'core-models/src/core/iter.rs', lines 542:20-551:21
     Visibility: public -/
 @[rust_loop]
 def
@@ -3840,7 +3807,7 @@ def
     self
 
 /-- [core_models::iter::adapters::flat_map::{impl core_models::iter::traits::iterator::Iterator<Clause1_Item> for core_models::iter::adapters::flat_map::FlatMap<I, U, F>}::next]:
-    Source: 'core-models/src/core/iter.rs', lines 541:12-554:13
+    Source: 'core-models/src/core/iter.rs', lines 540:12-553:13
     Visibility: public -/
 def
   iter.adapters.flat_map.FlatMap.Insts.CoreIterTraitsIteratorIterator.next
@@ -3859,7 +3826,7 @@ def
   ok (o, { it := t, f := t1, current := o1 })
 
 /-- Trait implementation: [core_models::iter::adapters::flat_map::{impl core_models::iter::traits::iterator::Iterator<Clause1_Item> for core_models::iter::adapters::flat_map::FlatMap<I, U, F>}]
-    Source: 'core-models/src/core/iter.rs', lines 539:8-555:9 -/
+    Source: 'core-models/src/core/iter.rs', lines 538:8-554:9 -/
 @[reducible]
 def iter.adapters.flat_map.FlatMap.Insts.CoreIterTraitsIteratorIterator
   {I : Type} {U : Type} {F : Type} {Clause0_Item : Type} {Clause1_Item : Type}
@@ -3875,7 +3842,7 @@ def iter.adapters.flat_map.FlatMap.Insts.CoreIterTraitsIteratorIterator
 }
 
 /-- [core_models::iter::adapters::flatten::{core_models::iter::adapters::flatten::Flatten<I, Clause0_Item, Clause1_Item>}::new]:
-    Source: 'core-models/src/core/iter.rs', lines 573:12-578:13
+    Source: 'core-models/src/core/iter.rs', lines 572:12-577:13
     Visibility: public -/
 def iter.adapters.flatten.Flatten.new
   {I : Type} {Clause0_Item : Type} {Clause1_Item : Type}
@@ -3887,7 +3854,7 @@ def iter.adapters.flatten.Flatten.new
   ok { it, current := option.Option.None }
 
 /-- [core_models::iter::adapters::flatten::{impl core_models::iter::traits::iterator::Iterator<Clause1_Item> for core_models::iter::adapters::flatten::Flatten<I, Clause0_Item, Clause1_Item>}::next]: loop body 0:
-    Source: 'core-models/src/core/iter.rs', lines 588:20-597:21
+    Source: 'core-models/src/core/iter.rs', lines 587:20-596:21
     Visibility: public -/
 @[rust_loop_body]
 def
@@ -3921,7 +3888,7 @@ def
       ok (done (option.Option.None, t, option.Option.None))
 
 /-- [core_models::iter::adapters::flatten::{impl core_models::iter::traits::iterator::Iterator<Clause1_Item> for core_models::iter::adapters::flatten::Flatten<I, Clause0_Item, Clause1_Item>}::next]: loop 0:
-    Source: 'core-models/src/core/iter.rs', lines 588:20-597:21
+    Source: 'core-models/src/core/iter.rs', lines 587:20-596:21
     Visibility: public -/
 @[rust_loop]
 def
@@ -3940,7 +3907,7 @@ def
     self
 
 /-- [core_models::iter::adapters::flatten::{impl core_models::iter::traits::iterator::Iterator<Clause1_Item> for core_models::iter::adapters::flatten::Flatten<I, Clause0_Item, Clause1_Item>}::next]:
-    Source: 'core-models/src/core/iter.rs', lines 586:12-599:13
+    Source: 'core-models/src/core/iter.rs', lines 585:12-598:13
     Visibility: public -/
 def
   iter.adapters.flatten.Flatten.Insts.CoreIterTraitsIteratorIterator.next
@@ -3958,7 +3925,7 @@ def
   ok (o, { it := t, current := o1 })
 
 /-- Trait implementation: [core_models::iter::adapters::flatten::{impl core_models::iter::traits::iterator::Iterator<Clause1_Item> for core_models::iter::adapters::flatten::Flatten<I, Clause0_Item, Clause1_Item>}]
-    Source: 'core-models/src/core/iter.rs', lines 581:8-600:9 -/
+    Source: 'core-models/src/core/iter.rs', lines 580:8-599:9 -/
 @[reducible]
 def iter.adapters.flatten.Flatten.Insts.CoreIterTraitsIteratorIterator
   {I : Type} {Clause0_Item : Type} {Clause1_Item : Type}
@@ -3972,7 +3939,7 @@ def iter.adapters.flatten.Flatten.Insts.CoreIterTraitsIteratorIterator
 }
 
 /-- [core_models::iter::adapters::zip::{core_models::iter::adapters::zip::Zip<I1, I2>}::new]:
-    Source: 'core-models/src/core/iter.rs', lines 611:12-613:13
+    Source: 'core-models/src/core/iter.rs', lines 610:12-612:13
     Visibility: public -/
 def iter.adapters.zip.Zip.new
   {I1 : Type} {I2 : Type} {Clause0_Item : Type} {Clause1_Item : Type}
@@ -3984,7 +3951,7 @@ def iter.adapters.zip.Zip.new
   ok { it1, it2 }
 
 /-- [core_models::iter::adapters::zip::{impl core_models::iter::traits::iterator::Iterator<(Clause0_Item, Clause1_Item)> for core_models::iter::adapters::zip::Zip<I1, I2>}::next]:
-    Source: 'core-models/src/core/iter.rs', lines 618:12-626:13
+    Source: 'core-models/src/core/iter.rs', lines 617:12-625:13
     Visibility: public -/
 def iter.adapters.zip.Zip.Insts.CoreIterTraitsIteratorIteratorPair.next
   {I1 : Type} {I2 : Type} {Clause0_Item : Type} {Clause1_Item : Type}
@@ -4005,7 +3972,7 @@ def iter.adapters.zip.Zip.Insts.CoreIterTraitsIteratorIteratorPair.next
   | option.Option.None => ok (option.Option.None, { self with it1 := t })
 
 /-- Trait implementation: [core_models::iter::adapters::zip::{impl core_models::iter::traits::iterator::Iterator<(Clause0_Item, Clause1_Item)> for core_models::iter::adapters::zip::Zip<I1, I2>}]
-    Source: 'core-models/src/core/iter.rs', lines 616:8-627:9 -/
+    Source: 'core-models/src/core/iter.rs', lines 615:8-626:9 -/
 @[reducible]
 def iter.adapters.zip.Zip.Insts.CoreIterTraitsIteratorIteratorPair {I1 :
   Type} {I2 : Type} {Clause0_Item : Type} {Clause1_Item : Type}
@@ -4019,7 +3986,7 @@ def iter.adapters.zip.Zip.Insts.CoreIterTraitsIteratorIteratorPair {I1 :
 }
 
 /-- [core_models::iter::adapters::chain::{core_models::iter::adapters::chain::Chain<A, B>}::new]:
-    Source: 'core-models/src/core/iter.rs', lines 671:12-676:13
+    Source: 'core-models/src/core/iter.rs', lines 670:12-675:13
     Visibility: public -/
 def iter.adapters.chain.Chain.new
   {A : Type} {B : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
@@ -4030,7 +3997,7 @@ def iter.adapters.chain.Chain.new
   ok { a := (option.Option.Some a), b }
 
 /-- [core_models::iter::adapters::chain::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::chain::Chain<A, B>}::next]:
-    Source: 'core-models/src/core/iter.rs', lines 682:12-690:13
+    Source: 'core-models/src/core/iter.rs', lines 681:12-689:13
     Visibility: public -/
 def iter.adapters.chain.Chain.Insts.CoreIterTraitsIteratorIterator.next
   {A : Type} {B : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
@@ -4053,7 +4020,7 @@ def iter.adapters.chain.Chain.Insts.CoreIterTraitsIteratorIterator.next
     ok (o, { a := option.Option.None, b := t })
 
 /-- Trait implementation: [core_models::iter::adapters::chain::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::chain::Chain<A, B>}]
-    Source: 'core-models/src/core/iter.rs', lines 680:8-691:9 -/
+    Source: 'core-models/src/core/iter.rs', lines 679:8-690:9 -/
 @[reducible]
 def iter.adapters.chain.Chain.Insts.CoreIterTraitsIteratorIterator {A :
   Type} {B : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
@@ -4066,7 +4033,7 @@ def iter.adapters.chain.Chain.Insts.CoreIterTraitsIteratorIterator {A :
 }
 
 /-- [core_models::iter::adapters::skip::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::skip::Skip<I>}::next]: loop body 0:
-    Source: 'core-models/src/core/iter.rs', lines 712:16-719:13
+    Source: 'core-models/src/core/iter.rs', lines 711:16-718:13
     Visibility: public -/
 @[rust_loop_body]
 def
@@ -4089,7 +4056,7 @@ def
     ok (done (o, t, self.n))
 
 /-- [core_models::iter::adapters::skip::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::skip::Skip<I>}::next]: loop 0:
-    Source: 'core-models/src/core/iter.rs', lines 712:16-719:13
+    Source: 'core-models/src/core/iter.rs', lines 711:16-718:13
     Visibility: public -/
 @[rust_loop]
 def
@@ -4106,7 +4073,7 @@ def
     self
 
 /-- [core_models::iter::adapters::skip::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::skip::Skip<I>}::next]:
-    Source: 'core-models/src/core/iter.rs', lines 711:12-719:13
+    Source: 'core-models/src/core/iter.rs', lines 710:12-718:13
     Visibility: public -/
 def iter.adapters.skip.Skip.Insts.CoreIterTraitsIteratorIterator.next
   {I : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
@@ -4120,7 +4087,7 @@ def iter.adapters.skip.Skip.Insts.CoreIterTraitsIteratorIterator.next
   ok (o, { iter := t, n := i })
 
 /-- Trait implementation: [core_models::iter::adapters::skip::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::skip::Skip<I>}]
-    Source: 'core-models/src/core/iter.rs', lines 709:8-720:9 -/
+    Source: 'core-models/src/core/iter.rs', lines 708:8-719:9 -/
 @[reducible]
 def iter.adapters.skip.Skip.Insts.CoreIterTraitsIteratorIterator {I :
   Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
@@ -4141,7 +4108,7 @@ def option.Option.expect
   | option.Option.None => panicking.internal.panic T
 
 /-- [core_models::iter::range::Step::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 737:8-739:9
+    Source: 'core-models/src/core/iter.rs', lines 736:8-738:9
     Visibility: public -/
 def iter.range.Step.forward.default
   {Self : Type} (StepInst : iter.range.Step Self) (start : Self)
@@ -4152,7 +4119,7 @@ def iter.range.Step.forward.default
   option.Option.expect o (toStr "overflow in `Step::forward`")
 
 /-- [core_models::iter::range::Step::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 741:8-743:9
+    Source: 'core-models/src/core/iter.rs', lines 740:8-742:9
     Visibility: public -/
 def iter.range.Step.forward_unchecked.default
   {Self : Type} (StepInst : iter.range.Step Self) (start : Self)
@@ -4162,7 +4129,7 @@ def iter.range.Step.forward_unchecked.default
   StepInst.forward start count
 
 /-- [core_models::iter::range::Step::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 745:8-747:9
+    Source: 'core-models/src/core/iter.rs', lines 744:8-746:9
     Visibility: public -/
 def iter.range.Step.backward.default
   {Self : Type} (StepInst : iter.range.Step Self) (start : Self)
@@ -4173,7 +4140,7 @@ def iter.range.Step.backward.default
   option.Option.expect o (toStr "overflow in `Step::backward`")
 
 /-- [core_models::iter::range::Step::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 749:8-751:9
+    Source: 'core-models/src/core/iter.rs', lines 748:8-750:9
     Visibility: public -/
 def iter.range.Step.backward_unchecked.default
   {Self : Type} (StepInst : iter.range.Step Self) (start : Self)
@@ -4217,7 +4184,7 @@ def num.I8.checked_add_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i8}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 756:12-758:13
+    Source: 'core-models/src/core/iter.rs', lines 755:12-757:13
     Visibility: public -/
 def I8.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.I8) (n : Std.Usize) : Result Std.I8 := do
@@ -4252,7 +4219,7 @@ def num.I16.checked_add_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i16}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 756:12-758:13
+    Source: 'core-models/src/core/iter.rs', lines 755:12-757:13
     Visibility: public -/
 def I16.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.I16) (n : Std.Usize) : Result Std.I16 := do
@@ -4287,7 +4254,7 @@ def num.I32.checked_add_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i32}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 756:12-758:13
+    Source: 'core-models/src/core/iter.rs', lines 755:12-757:13
     Visibility: public -/
 def I32.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.I32) (n : Std.Usize) : Result Std.I32 := do
@@ -4323,7 +4290,7 @@ def num.I64.checked_add_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i64}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 756:12-758:13
+    Source: 'core-models/src/core/iter.rs', lines 755:12-757:13
     Visibility: public -/
 def I64.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.I64) (n : Std.Usize) : Result Std.I64 := do
@@ -4360,7 +4327,7 @@ def num.Isize.checked_add_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for isize}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 756:12-758:13
+    Source: 'core-models/src/core/iter.rs', lines 755:12-757:13
     Visibility: public -/
 def Isize.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.Isize) (n : Std.Usize) : Result Std.Isize := do
@@ -4395,7 +4362,7 @@ def num.I128.checked_add_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i128}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 756:12-758:13
+    Source: 'core-models/src/core/iter.rs', lines 755:12-757:13
     Visibility: public -/
 def I128.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.I128) (n : Std.Usize) : Result Std.I128 := do
@@ -4423,7 +4390,7 @@ def num.I8.checked_sub_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i8}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 760:12-762:13
+    Source: 'core-models/src/core/iter.rs', lines 759:12-761:13
     Visibility: public -/
 def I8.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.I8) (n : Std.Usize) : Result Std.I8 := do
@@ -4451,7 +4418,7 @@ def num.I16.checked_sub_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i16}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 760:12-762:13
+    Source: 'core-models/src/core/iter.rs', lines 759:12-761:13
     Visibility: public -/
 def I16.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.I16) (n : Std.Usize) : Result Std.I16 := do
@@ -4479,7 +4446,7 @@ def num.I32.checked_sub_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i32}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 760:12-762:13
+    Source: 'core-models/src/core/iter.rs', lines 759:12-761:13
     Visibility: public -/
 def I32.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.I32) (n : Std.Usize) : Result Std.I32 := do
@@ -4507,7 +4474,7 @@ def num.I64.checked_sub_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i64}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 760:12-762:13
+    Source: 'core-models/src/core/iter.rs', lines 759:12-761:13
     Visibility: public -/
 def I64.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.I64) (n : Std.Usize) : Result Std.I64 := do
@@ -4536,7 +4503,7 @@ def num.Isize.checked_sub_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for isize}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 760:12-762:13
+    Source: 'core-models/src/core/iter.rs', lines 759:12-761:13
     Visibility: public -/
 def Isize.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.Isize) (n : Std.Usize) : Result Std.Isize := do
@@ -4563,7 +4530,7 @@ def num.I128.checked_sub_unsigned
   else ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i128}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 760:12-762:13
+    Source: 'core-models/src/core/iter.rs', lines 759:12-761:13
     Visibility: public -/
 def I128.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.I128) (n : Std.Usize) : Result Std.I128 := do
@@ -4578,7 +4545,7 @@ def num.U8.unchecked_add (x : Std.U8) (y : Std.U8) : Result Std.U8 := do
   x + y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u8}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 768:12-770:13
+    Source: 'core-models/src/core/iter.rs', lines 767:12-769:13
     Visibility: public -/
 def U8.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.U8) (n : Std.Usize) : Result Std.U8 := do
@@ -4592,7 +4559,7 @@ def num.U16.unchecked_add (x : Std.U16) (y : Std.U16) : Result Std.U16 := do
   x + y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u16}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 768:12-770:13
+    Source: 'core-models/src/core/iter.rs', lines 767:12-769:13
     Visibility: public -/
 def U16.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.U16) (n : Std.Usize) : Result Std.U16 := do
@@ -4606,7 +4573,7 @@ def num.U32.unchecked_add (x : Std.U32) (y : Std.U32) : Result Std.U32 := do
   x + y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u32}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 768:12-770:13
+    Source: 'core-models/src/core/iter.rs', lines 767:12-769:13
     Visibility: public -/
 def U32.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.U32) (n : Std.Usize) : Result Std.U32 := do
@@ -4620,7 +4587,7 @@ def num.U64.unchecked_add (x : Std.U64) (y : Std.U64) : Result Std.U64 := do
   x + y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u64}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 768:12-770:13
+    Source: 'core-models/src/core/iter.rs', lines 767:12-769:13
     Visibility: public -/
 def U64.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.U64) (n : Std.Usize) : Result Std.U64 := do
@@ -4635,7 +4602,7 @@ def num.Usize.unchecked_add
   x + y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for usize}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 768:12-770:13
+    Source: 'core-models/src/core/iter.rs', lines 767:12-769:13
     Visibility: public -/
 def Usize.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.Usize) (n : Std.Usize) : Result Std.Usize := do
@@ -4649,7 +4616,7 @@ def num.U128.unchecked_add
   x + y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u128}::forward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 768:12-770:13
+    Source: 'core-models/src/core/iter.rs', lines 767:12-769:13
     Visibility: public -/
 def U128.Insts.CoreIterRangeStep.forward_unchecked
   (start : Std.U128) (n : Std.Usize) : Result Std.U128 := do
@@ -4663,7 +4630,7 @@ def num.U8.unchecked_sub (x : Std.U8) (y : Std.U8) : Result Std.U8 := do
   x - y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u8}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 772:12-774:13
+    Source: 'core-models/src/core/iter.rs', lines 771:12-773:13
     Visibility: public -/
 def U8.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.U8) (n : Std.Usize) : Result Std.U8 := do
@@ -4677,7 +4644,7 @@ def num.U16.unchecked_sub (x : Std.U16) (y : Std.U16) : Result Std.U16 := do
   x - y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u16}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 772:12-774:13
+    Source: 'core-models/src/core/iter.rs', lines 771:12-773:13
     Visibility: public -/
 def U16.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.U16) (n : Std.Usize) : Result Std.U16 := do
@@ -4691,7 +4658,7 @@ def num.U32.unchecked_sub (x : Std.U32) (y : Std.U32) : Result Std.U32 := do
   x - y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u32}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 772:12-774:13
+    Source: 'core-models/src/core/iter.rs', lines 771:12-773:13
     Visibility: public -/
 def U32.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.U32) (n : Std.Usize) : Result Std.U32 := do
@@ -4705,7 +4672,7 @@ def num.U64.unchecked_sub (x : Std.U64) (y : Std.U64) : Result Std.U64 := do
   x - y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u64}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 772:12-774:13
+    Source: 'core-models/src/core/iter.rs', lines 771:12-773:13
     Visibility: public -/
 def U64.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.U64) (n : Std.Usize) : Result Std.U64 := do
@@ -4720,7 +4687,7 @@ def num.Usize.unchecked_sub
   x - y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for usize}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 772:12-774:13
+    Source: 'core-models/src/core/iter.rs', lines 771:12-773:13
     Visibility: public -/
 def Usize.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.Usize) (n : Std.Usize) : Result Std.Usize := do
@@ -4734,7 +4701,7 @@ def num.U128.unchecked_sub
   x - y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u128}::backward_unchecked]:
-    Source: 'core-models/src/core/iter.rs', lines 772:12-774:13
+    Source: 'core-models/src/core/iter.rs', lines 771:12-773:13
     Visibility: public -/
 def U128.Insts.CoreIterRangeStep.backward_unchecked
   (start : Std.U128) (n : Std.Usize) : Result Std.U128 := do
@@ -4759,7 +4726,7 @@ def num.U8.checked_add
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u8}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 812:20-817:21
+    Source: 'core-models/src/core/iter.rs', lines 811:20-816:21
     Visibility: public -/
 def U8.Insts.CoreIterRangeStep.forward_checked
   (start : Std.U8) (n : Std.Usize) : Result (option.Option Std.U8) := do
@@ -4769,7 +4736,7 @@ def U8.Insts.CoreIterRangeStep.forward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u8}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def U8.Insts.CoreIterRangeStep.forward
   (start : Std.U8) (n : Std.Usize) : Result Std.U8 := do
@@ -4783,7 +4750,7 @@ def num.I8.wrapping_add (x : Std.I8) (y : Std.I8) : Result Std.I8 := do
   rust_primitives.arithmetic.wrapping_add_i8 x y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i8}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 844:20-862:21
+    Source: 'core-models/src/core/iter.rs', lines 843:20-861:21
     Visibility: public -/
 def I8.Insts.CoreIterRangeStep.forward_checked
   (start : Std.I8) (n : Std.Usize) : Result (option.Option Std.I8) := do
@@ -4798,7 +4765,7 @@ def I8.Insts.CoreIterRangeStep.forward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i8}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def I8.Insts.CoreIterRangeStep.forward
   (start : Std.I8) (n : Std.Usize) : Result Std.I8 := do
@@ -4823,7 +4790,7 @@ def num.U16.checked_add
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u16}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 812:20-817:21
+    Source: 'core-models/src/core/iter.rs', lines 811:20-816:21
     Visibility: public -/
 def U16.Insts.CoreIterRangeStep.forward_checked
   (start : Std.U16) (n : Std.Usize) : Result (option.Option Std.U16) := do
@@ -4833,7 +4800,7 @@ def U16.Insts.CoreIterRangeStep.forward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u16}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def U16.Insts.CoreIterRangeStep.forward
   (start : Std.U16) (n : Std.Usize) : Result Std.U16 := do
@@ -4847,7 +4814,7 @@ def num.I16.wrapping_add (x : Std.I16) (y : Std.I16) : Result Std.I16 := do
   rust_primitives.arithmetic.wrapping_add_i16 x y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i16}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 844:20-862:21
+    Source: 'core-models/src/core/iter.rs', lines 843:20-861:21
     Visibility: public -/
 def I16.Insts.CoreIterRangeStep.forward_checked
   (start : Std.I16) (n : Std.Usize) : Result (option.Option Std.I16) := do
@@ -4862,7 +4829,7 @@ def I16.Insts.CoreIterRangeStep.forward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i16}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def I16.Insts.CoreIterRangeStep.forward
   (start : Std.I16) (n : Std.Usize) : Result Std.I16 := do
@@ -4887,7 +4854,7 @@ def num.U32.checked_add
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u32}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 812:20-817:21
+    Source: 'core-models/src/core/iter.rs', lines 811:20-816:21
     Visibility: public -/
 def U32.Insts.CoreIterRangeStep.forward_checked
   (start : Std.U32) (n : Std.Usize) : Result (option.Option Std.U32) := do
@@ -4897,7 +4864,7 @@ def U32.Insts.CoreIterRangeStep.forward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u32}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def U32.Insts.CoreIterRangeStep.forward
   (start : Std.U32) (n : Std.Usize) : Result Std.U32 := do
@@ -4911,7 +4878,7 @@ def num.I32.wrapping_add (x : Std.I32) (y : Std.I32) : Result Std.I32 := do
   rust_primitives.arithmetic.wrapping_add_i32 x y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i32}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 844:20-862:21
+    Source: 'core-models/src/core/iter.rs', lines 843:20-861:21
     Visibility: public -/
 def I32.Insts.CoreIterRangeStep.forward_checked
   (start : Std.I32) (n : Std.Usize) : Result (option.Option Std.I32) := do
@@ -4926,7 +4893,7 @@ def I32.Insts.CoreIterRangeStep.forward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i32}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def I32.Insts.CoreIterRangeStep.forward
   (start : Std.I32) (n : Std.Usize) : Result Std.I32 := do
@@ -4951,7 +4918,7 @@ def num.U64.checked_add
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u64}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 812:20-817:21
+    Source: 'core-models/src/core/iter.rs', lines 811:20-816:21
     Visibility: public -/
 def U64.Insts.CoreIterRangeStep.forward_checked
   (start : Std.U64) (n : Std.Usize) : Result (option.Option Std.U64) := do
@@ -4961,7 +4928,7 @@ def U64.Insts.CoreIterRangeStep.forward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u64}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def U64.Insts.CoreIterRangeStep.forward
   (start : Std.U64) (n : Std.Usize) : Result Std.U64 := do
@@ -4975,7 +4942,7 @@ def num.I64.wrapping_add (x : Std.I64) (y : Std.I64) : Result Std.I64 := do
   rust_primitives.arithmetic.wrapping_add_i64 x y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i64}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 844:20-862:21
+    Source: 'core-models/src/core/iter.rs', lines 843:20-861:21
     Visibility: public -/
 def I64.Insts.CoreIterRangeStep.forward_checked
   (start : Std.I64) (n : Std.Usize) : Result (option.Option Std.I64) := do
@@ -4990,7 +4957,7 @@ def I64.Insts.CoreIterRangeStep.forward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i64}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def I64.Insts.CoreIterRangeStep.forward
   (start : Std.I64) (n : Std.Usize) : Result Std.I64 := do
@@ -5015,7 +4982,7 @@ def num.Usize.checked_add
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for usize}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 812:20-817:21
+    Source: 'core-models/src/core/iter.rs', lines 811:20-816:21
     Visibility: public -/
 def Usize.Insts.CoreIterRangeStep.forward_checked
   (start : Std.Usize) (n : Std.Usize) : Result (option.Option Std.Usize) := do
@@ -5027,7 +4994,7 @@ def Usize.Insts.CoreIterRangeStep.forward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for usize}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def Usize.Insts.CoreIterRangeStep.forward
   (start : Std.Usize) (n : Std.Usize) : Result Std.Usize := do
@@ -5042,7 +5009,7 @@ def num.Isize.wrapping_add
   rust_primitives.arithmetic.wrapping_add_isize x y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for isize}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 844:20-862:21
+    Source: 'core-models/src/core/iter.rs', lines 843:20-861:21
     Visibility: public -/
 def Isize.Insts.CoreIterRangeStep.forward_checked
   (start : Std.Isize) (n : Std.Usize) : Result (option.Option Std.Isize) := do
@@ -5059,7 +5026,7 @@ def Isize.Insts.CoreIterRangeStep.forward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for isize}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def Isize.Insts.CoreIterRangeStep.forward
   (start : Std.Isize) (n : Std.Usize) : Result Std.Isize := do
@@ -5084,7 +5051,7 @@ def num.U128.checked_add
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u128}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 902:20-904:21
+    Source: 'core-models/src/core/iter.rs', lines 901:20-903:21
     Visibility: public -/
 def U128.Insts.CoreIterRangeStep.forward_checked
   (start : Std.U128) (n : Std.Usize) : Result (option.Option Std.U128) := do
@@ -5092,7 +5059,7 @@ def U128.Insts.CoreIterRangeStep.forward_checked
   num.U128.checked_add start i
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u128}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def U128.Insts.CoreIterRangeStep.forward
   (start : Std.U128) (n : Std.Usize) : Result Std.U128 := do
@@ -5110,7 +5077,7 @@ def num.I128.checked_add
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i128}::forward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 933:20-935:21
+    Source: 'core-models/src/core/iter.rs', lines 932:20-934:21
     Visibility: public -/
 def I128.Insts.CoreIterRangeStep.forward_checked
   (start : Std.I128) (n : Std.Usize) : Result (option.Option Std.I128) := do
@@ -5118,7 +5085,7 @@ def I128.Insts.CoreIterRangeStep.forward_checked
   num.I128.checked_add start i
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i128}::forward]:
-    Source: 'core-models/src/core/iter.rs', lines 780:12-782:13
+    Source: 'core-models/src/core/iter.rs', lines 779:12-781:13
     Visibility: public -/
 def I128.Insts.CoreIterRangeStep.forward
   (start : Std.I128) (n : Std.Usize) : Result Std.I128 := do
@@ -5143,7 +5110,7 @@ def num.U8.checked_sub
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u8}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 819:20-824:21
+    Source: 'core-models/src/core/iter.rs', lines 818:20-823:21
     Visibility: public -/
 def U8.Insts.CoreIterRangeStep.backward_checked
   (start : Std.U8) (n : Std.Usize) : Result (option.Option Std.U8) := do
@@ -5153,7 +5120,7 @@ def U8.Insts.CoreIterRangeStep.backward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u8}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def U8.Insts.CoreIterRangeStep.backward
   (start : Std.U8) (n : Std.Usize) : Result Std.U8 := do
@@ -5167,7 +5134,7 @@ def num.I8.wrapping_sub (x : Std.I8) (y : Std.I8) : Result Std.I8 := do
   rust_primitives.arithmetic.wrapping_sub_i8 x y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i8}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 864:20-882:21
+    Source: 'core-models/src/core/iter.rs', lines 863:20-881:21
     Visibility: public -/
 def I8.Insts.CoreIterRangeStep.backward_checked
   (start : Std.I8) (n : Std.Usize) : Result (option.Option Std.I8) := do
@@ -5182,7 +5149,7 @@ def I8.Insts.CoreIterRangeStep.backward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i8}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def I8.Insts.CoreIterRangeStep.backward
   (start : Std.I8) (n : Std.Usize) : Result Std.I8 := do
@@ -5207,7 +5174,7 @@ def num.U16.checked_sub
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u16}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 819:20-824:21
+    Source: 'core-models/src/core/iter.rs', lines 818:20-823:21
     Visibility: public -/
 def U16.Insts.CoreIterRangeStep.backward_checked
   (start : Std.U16) (n : Std.Usize) : Result (option.Option Std.U16) := do
@@ -5217,7 +5184,7 @@ def U16.Insts.CoreIterRangeStep.backward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u16}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def U16.Insts.CoreIterRangeStep.backward
   (start : Std.U16) (n : Std.Usize) : Result Std.U16 := do
@@ -5231,7 +5198,7 @@ def num.I16.wrapping_sub (x : Std.I16) (y : Std.I16) : Result Std.I16 := do
   rust_primitives.arithmetic.wrapping_sub_i16 x y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i16}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 864:20-882:21
+    Source: 'core-models/src/core/iter.rs', lines 863:20-881:21
     Visibility: public -/
 def I16.Insts.CoreIterRangeStep.backward_checked
   (start : Std.I16) (n : Std.Usize) : Result (option.Option Std.I16) := do
@@ -5246,7 +5213,7 @@ def I16.Insts.CoreIterRangeStep.backward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i16}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def I16.Insts.CoreIterRangeStep.backward
   (start : Std.I16) (n : Std.Usize) : Result Std.I16 := do
@@ -5271,7 +5238,7 @@ def num.U32.checked_sub
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u32}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 819:20-824:21
+    Source: 'core-models/src/core/iter.rs', lines 818:20-823:21
     Visibility: public -/
 def U32.Insts.CoreIterRangeStep.backward_checked
   (start : Std.U32) (n : Std.Usize) : Result (option.Option Std.U32) := do
@@ -5281,7 +5248,7 @@ def U32.Insts.CoreIterRangeStep.backward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u32}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def U32.Insts.CoreIterRangeStep.backward
   (start : Std.U32) (n : Std.Usize) : Result Std.U32 := do
@@ -5295,7 +5262,7 @@ def num.I32.wrapping_sub (x : Std.I32) (y : Std.I32) : Result Std.I32 := do
   rust_primitives.arithmetic.wrapping_sub_i32 x y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i32}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 864:20-882:21
+    Source: 'core-models/src/core/iter.rs', lines 863:20-881:21
     Visibility: public -/
 def I32.Insts.CoreIterRangeStep.backward_checked
   (start : Std.I32) (n : Std.Usize) : Result (option.Option Std.I32) := do
@@ -5310,7 +5277,7 @@ def I32.Insts.CoreIterRangeStep.backward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i32}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def I32.Insts.CoreIterRangeStep.backward
   (start : Std.I32) (n : Std.Usize) : Result Std.I32 := do
@@ -5335,7 +5302,7 @@ def num.U64.checked_sub
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u64}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 819:20-824:21
+    Source: 'core-models/src/core/iter.rs', lines 818:20-823:21
     Visibility: public -/
 def U64.Insts.CoreIterRangeStep.backward_checked
   (start : Std.U64) (n : Std.Usize) : Result (option.Option Std.U64) := do
@@ -5345,7 +5312,7 @@ def U64.Insts.CoreIterRangeStep.backward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u64}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def U64.Insts.CoreIterRangeStep.backward
   (start : Std.U64) (n : Std.Usize) : Result Std.U64 := do
@@ -5359,7 +5326,7 @@ def num.I64.wrapping_sub (x : Std.I64) (y : Std.I64) : Result Std.I64 := do
   rust_primitives.arithmetic.wrapping_sub_i64 x y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i64}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 864:20-882:21
+    Source: 'core-models/src/core/iter.rs', lines 863:20-881:21
     Visibility: public -/
 def I64.Insts.CoreIterRangeStep.backward_checked
   (start : Std.I64) (n : Std.Usize) : Result (option.Option Std.I64) := do
@@ -5374,7 +5341,7 @@ def I64.Insts.CoreIterRangeStep.backward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i64}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def I64.Insts.CoreIterRangeStep.backward
   (start : Std.I64) (n : Std.Usize) : Result Std.I64 := do
@@ -5399,7 +5366,7 @@ def num.Usize.checked_sub
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for usize}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 819:20-824:21
+    Source: 'core-models/src/core/iter.rs', lines 818:20-823:21
     Visibility: public -/
 def Usize.Insts.CoreIterRangeStep.backward_checked
   (start : Std.Usize) (n : Std.Usize) : Result (option.Option Std.Usize) := do
@@ -5411,7 +5378,7 @@ def Usize.Insts.CoreIterRangeStep.backward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for usize}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def Usize.Insts.CoreIterRangeStep.backward
   (start : Std.Usize) (n : Std.Usize) : Result Std.Usize := do
@@ -5426,7 +5393,7 @@ def num.Isize.wrapping_sub
   rust_primitives.arithmetic.wrapping_sub_isize x y
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for isize}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 864:20-882:21
+    Source: 'core-models/src/core/iter.rs', lines 863:20-881:21
     Visibility: public -/
 def Isize.Insts.CoreIterRangeStep.backward_checked
   (start : Std.Isize) (n : Std.Usize) : Result (option.Option Std.Isize) := do
@@ -5443,7 +5410,7 @@ def Isize.Insts.CoreIterRangeStep.backward_checked
   | core.result.Result.Err _ => ok option.Option.None
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for isize}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def Isize.Insts.CoreIterRangeStep.backward
   (start : Std.Isize) (n : Std.Usize) : Result Std.Isize := do
@@ -5468,7 +5435,7 @@ def num.U128.checked_sub
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u128}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 906:20-908:21
+    Source: 'core-models/src/core/iter.rs', lines 905:20-907:21
     Visibility: public -/
 def U128.Insts.CoreIterRangeStep.backward_checked
   (start : Std.U128) (n : Std.Usize) : Result (option.Option Std.U128) := do
@@ -5476,7 +5443,7 @@ def U128.Insts.CoreIterRangeStep.backward_checked
   num.U128.checked_sub start i
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u128}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def U128.Insts.CoreIterRangeStep.backward
   (start : Std.U128) (n : Std.Usize) : Result Std.U128 := do
@@ -5494,7 +5461,7 @@ def num.I128.checked_sub
   else ok (option.Option.Some result)
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i128}::backward_checked]:
-    Source: 'core-models/src/core/iter.rs', lines 937:20-939:21
+    Source: 'core-models/src/core/iter.rs', lines 936:20-938:21
     Visibility: public -/
 def I128.Insts.CoreIterRangeStep.backward_checked
   (start : Std.I128) (n : Std.Usize) : Result (option.Option Std.I128) := do
@@ -5502,7 +5469,7 @@ def I128.Insts.CoreIterRangeStep.backward_checked
   num.I128.checked_sub start i
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i128}::backward]:
-    Source: 'core-models/src/core/iter.rs', lines 784:12-786:13
+    Source: 'core-models/src/core/iter.rs', lines 783:12-785:13
     Visibility: public -/
 def I128.Insts.CoreIterRangeStep.backward
   (start : Std.I128) (n : Std.Usize) : Result Std.I128 := do
@@ -5510,7 +5477,7 @@ def I128.Insts.CoreIterRangeStep.backward
   option.Option.unwrap o
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u8}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 802:20-810:21
+    Source: 'core-models/src/core/iter.rs', lines 801:20-809:21
     Visibility: public -/
 def U8.Insts.CoreIterRangeStep.steps_between
   (start : Std.U8) (end1 : Std.U8) :
@@ -5524,7 +5491,7 @@ def U8.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for u8}]
-    Source: 'core-models/src/core/iter.rs', lines 798:16-825:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 797:16-824:17 -/
 @[reducible]
 def U8.Insts.CoreIterRangeStep : iter.range.Step Std.U8 := {
   cloneCloneInst := U8.Insts.CoreCloneClone
@@ -5539,7 +5506,7 @@ def U8.Insts.CoreIterRangeStep : iter.range.Step Std.U8 := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u16}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 802:20-810:21
+    Source: 'core-models/src/core/iter.rs', lines 801:20-809:21
     Visibility: public -/
 def U16.Insts.CoreIterRangeStep.steps_between
   (start : Std.U16) (end1 : Std.U16) :
@@ -5553,7 +5520,7 @@ def U16.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for u16}]
-    Source: 'core-models/src/core/iter.rs', lines 798:16-825:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 797:16-824:17 -/
 @[reducible]
 def U16.Insts.CoreIterRangeStep : iter.range.Step Std.U16 := {
   cloneCloneInst := U16.Insts.CoreCloneClone
@@ -5568,7 +5535,7 @@ def U16.Insts.CoreIterRangeStep : iter.range.Step Std.U16 := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u32}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 802:20-810:21
+    Source: 'core-models/src/core/iter.rs', lines 801:20-809:21
     Visibility: public -/
 def U32.Insts.CoreIterRangeStep.steps_between
   (start : Std.U32) (end1 : Std.U32) :
@@ -5582,7 +5549,7 @@ def U32.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for u32}]
-    Source: 'core-models/src/core/iter.rs', lines 798:16-825:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 797:16-824:17 -/
 @[reducible]
 def U32.Insts.CoreIterRangeStep : iter.range.Step Std.U32 := {
   cloneCloneInst := U32.Insts.CoreCloneClone
@@ -5597,7 +5564,7 @@ def U32.Insts.CoreIterRangeStep : iter.range.Step Std.U32 := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u64}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 802:20-810:21
+    Source: 'core-models/src/core/iter.rs', lines 801:20-809:21
     Visibility: public -/
 def U64.Insts.CoreIterRangeStep.steps_between
   (start : Std.U64) (end1 : Std.U64) :
@@ -5611,7 +5578,7 @@ def U64.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for u64}]
-    Source: 'core-models/src/core/iter.rs', lines 798:16-825:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 797:16-824:17 -/
 @[reducible]
 def U64.Insts.CoreIterRangeStep : iter.range.Step Std.U64 := {
   cloneCloneInst := U64.Insts.CoreCloneClone
@@ -5626,7 +5593,7 @@ def U64.Insts.CoreIterRangeStep : iter.range.Step Std.U64 := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for usize}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 802:20-810:21
+    Source: 'core-models/src/core/iter.rs', lines 801:20-809:21
     Visibility: public -/
 def Usize.Insts.CoreIterRangeStep.steps_between
   (start : Std.Usize) (end1 : Std.Usize) :
@@ -5638,7 +5605,7 @@ def Usize.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for usize}]
-    Source: 'core-models/src/core/iter.rs', lines 798:16-825:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 797:16-824:17 -/
 @[reducible]
 def Usize.Insts.CoreIterRangeStep : iter.range.Step Std.Usize := {
   cloneCloneInst := Usize.Insts.CoreCloneClone
@@ -5653,7 +5620,7 @@ def Usize.Insts.CoreIterRangeStep : iter.range.Step Std.Usize := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i8}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 831:20-842:21
+    Source: 'core-models/src/core/iter.rs', lines 830:20-841:21
     Visibility: public -/
 def I8.Insts.CoreIterRangeStep.steps_between
   (start : Std.I8) (end1 : Std.I8) :
@@ -5669,7 +5636,7 @@ def I8.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for i8}]
-    Source: 'core-models/src/core/iter.rs', lines 827:16-883:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 826:16-882:17 -/
 @[reducible]
 def I8.Insts.CoreIterRangeStep : iter.range.Step Std.I8 := {
   cloneCloneInst := I8.Insts.CoreCloneClone
@@ -5684,7 +5651,7 @@ def I8.Insts.CoreIterRangeStep : iter.range.Step Std.I8 := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i16}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 831:20-842:21
+    Source: 'core-models/src/core/iter.rs', lines 830:20-841:21
     Visibility: public -/
 def I16.Insts.CoreIterRangeStep.steps_between
   (start : Std.I16) (end1 : Std.I16) :
@@ -5700,7 +5667,7 @@ def I16.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for i16}]
-    Source: 'core-models/src/core/iter.rs', lines 827:16-883:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 826:16-882:17 -/
 @[reducible]
 def I16.Insts.CoreIterRangeStep : iter.range.Step Std.I16 := {
   cloneCloneInst := I16.Insts.CoreCloneClone
@@ -5715,7 +5682,7 @@ def I16.Insts.CoreIterRangeStep : iter.range.Step Std.I16 := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i32}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 831:20-842:21
+    Source: 'core-models/src/core/iter.rs', lines 830:20-841:21
     Visibility: public -/
 def I32.Insts.CoreIterRangeStep.steps_between
   (start : Std.I32) (end1 : Std.I32) :
@@ -5731,7 +5698,7 @@ def I32.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for i32}]
-    Source: 'core-models/src/core/iter.rs', lines 827:16-883:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 826:16-882:17 -/
 @[reducible]
 def I32.Insts.CoreIterRangeStep : iter.range.Step Std.I32 := {
   cloneCloneInst := I32.Insts.CoreCloneClone
@@ -5746,7 +5713,7 @@ def I32.Insts.CoreIterRangeStep : iter.range.Step Std.I32 := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i64}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 831:20-842:21
+    Source: 'core-models/src/core/iter.rs', lines 830:20-841:21
     Visibility: public -/
 def I64.Insts.CoreIterRangeStep.steps_between
   (start : Std.I64) (end1 : Std.I64) :
@@ -5762,7 +5729,7 @@ def I64.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for i64}]
-    Source: 'core-models/src/core/iter.rs', lines 827:16-883:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 826:16-882:17 -/
 @[reducible]
 def I64.Insts.CoreIterRangeStep : iter.range.Step Std.I64 := {
   cloneCloneInst := I64.Insts.CoreCloneClone
@@ -5777,7 +5744,7 @@ def I64.Insts.CoreIterRangeStep : iter.range.Step Std.I64 := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for isize}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 831:20-842:21
+    Source: 'core-models/src/core/iter.rs', lines 830:20-841:21
     Visibility: public -/
 def Isize.Insts.CoreIterRangeStep.steps_between
   (start : Std.Isize) (end1 : Std.Isize) :
@@ -5791,7 +5758,7 @@ def Isize.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for isize}]
-    Source: 'core-models/src/core/iter.rs', lines 827:16-883:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 826:16-882:17 -/
 @[reducible]
 def Isize.Insts.CoreIterRangeStep : iter.range.Step Std.Isize := {
   cloneCloneInst := Isize.Insts.CoreCloneClone
@@ -5806,7 +5773,7 @@ def Isize.Insts.CoreIterRangeStep : iter.range.Step Std.Isize := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for u128}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 891:20-900:21
+    Source: 'core-models/src/core/iter.rs', lines 890:20-899:21
     Visibility: public -/
 def U128.Insts.CoreIterRangeStep.steps_between
   (start : Std.U128) (end1 : Std.U128) :
@@ -5823,7 +5790,7 @@ def U128.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for u128}]
-    Source: 'core-models/src/core/iter.rs', lines 887:16-909:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 886:16-908:17 -/
 @[reducible]
 def U128.Insts.CoreIterRangeStep : iter.range.Step Std.U128 := {
   cloneCloneInst := U128.Insts.CoreCloneClone
@@ -5838,7 +5805,7 @@ def U128.Insts.CoreIterRangeStep : iter.range.Step Std.U128 := {
 }
 
 /-- [core_models::iter::range::{impl core_models::iter::range::Step for i128}::steps_between]:
-    Source: 'core-models/src/core/iter.rs', lines 915:20-931:21
+    Source: 'core-models/src/core/iter.rs', lines 914:20-930:21
     Visibility: public -/
 def I128.Insts.CoreIterRangeStep.steps_between
   (start : Std.I128) (end1 : Std.I128) :
@@ -5859,7 +5826,7 @@ def I128.Insts.CoreIterRangeStep.steps_between
   else ok (0#usize, option.Option.None)
 
 /-- Trait implementation: [core_models::iter::range::{impl core_models::iter::range::Step for i128}]
-    Source: 'core-models/src/core/iter.rs', lines 911:16-940:17 -/
+    Source: 'core-models/src/core/iter.rs', lines 910:16-939:17 -/
 @[reducible]
 def I128.Insts.CoreIterRangeStep : iter.range.Step Std.I128 := {
   cloneCloneInst := I128.Insts.CoreCloneClone
@@ -9468,6 +9435,54 @@ def option.Option.Insts.CoreDefaultDefault (T : Type) : default.Default
   default := option.Option.Insts.CoreDefaultDefault.default T
 }
 
+/-- [core_models::option::{impl core_models::clone::Clone for core_models::option::Option<T>}::clone]:
+    Source: 'core-models/src/core/option.rs', lines 258:4-263:5
+    Visibility: public -/
+def option.Option.Insts.CoreCloneClone.clone
+  {T : Type} (cloneCloneInst : clone.Clone T) (self : option.Option T) :
+  Result (option.Option T)
+  := do
+  match self with
+  | option.Option.Some arg0 =>
+    let t ← cloneCloneInst.clone arg0
+    ok (option.Option.Some t)
+  | option.Option.None => ok option.Option.None
+
+/-- Trait implementation: [core_models::option::{impl core_models::clone::Clone for core_models::option::Option<T>}]
+    Source: 'core-models/src/core/option.rs', lines 257:0-264:1 -/
+@[reducible]
+def option.Option.Insts.CoreCloneClone {T : Type} (cloneCloneInst :
+  clone.Clone T) : clone.Clone (option.Option T) := {
+  clone := option.Option.Insts.CoreCloneClone.clone cloneCloneInst
+}
+
+/-- [core_models::option::{impl core_models::cmp::PartialEq<core_models::option::Option<T>> for core_models::option::Option<T>}::eq]:
+    Source: 'core-models/src/core/option.rs', lines 267:4-273:5
+    Visibility: public -/
+def option.Option.Insts.CoreCmpPartialEqOption.eq
+  {T : Type} (cmpPartialEqInst : cmp.PartialEq T T) (self : option.Option T)
+  (other : option.Option T) :
+  Result Bool
+  := do
+  match self with
+  | option.Option.Some a =>
+    match other with
+    | option.Option.Some b => cmpPartialEqInst.eq a b
+    | option.Option.None => ok false
+  | option.Option.None =>
+    match other with
+    | option.Option.Some _ => ok false
+    | option.Option.None => ok true
+
+/-- Trait implementation: [core_models::option::{impl core_models::cmp::PartialEq<core_models::option::Option<T>> for core_models::option::Option<T>}]
+    Source: 'core-models/src/core/option.rs', lines 266:0-274:1 -/
+@[reducible]
+def option.Option.Insts.CoreCmpPartialEqOption {T : Type}
+  (cmpPartialEqInst : cmp.PartialEq T T) : cmp.PartialEq (option.Option T)
+  (option.Option T) := {
+  eq := option.Option.Insts.CoreCmpPartialEqOption.eq cmpPartialEqInst
+}
+
 /-- [core_models::panicking::panic_explicit]:
     Source: 'core-models/src/core/panicking.rs', lines 3:0-5:1
     Visibility: public -/
@@ -9486,6 +9501,70 @@ def panicking.panic (_msg : Str) : Result Never := do
 def panicking.panic_fmt (_fmt : fmt.Arguments) : Result Never := do
   fail Error.panic
 
+/-- [core_models::result::{impl core_models::iter::traits::collect::FromIterator<core_models::result::Result<A, E>> for core_models::result::Result<V, E>}::from_iter]:
+    Source: 'core-models/src/core/result.rs', lines 299:4-301:5
+    Visibility: public -/
+def
+  result.Result.Insts.CoreIterTraitsCollectFromIteratorResult.from_iter
+  {A : Type} (E : Type) {V : Type} {T : Type} {Clause1_Item : Type}
+  {Clause1_IntoIter : Type} (itertraitscollectFromIteratorInst :
+  iter.traits.collect.FromIterator V A) (itertraitscollectIntoIteratorInst :
+  iter.traits.collect.IntoIterator T Clause1_Item Clause1_IntoIter) (iter_ : T)
+  :
+  Aeneas.Std.Result (result.Result V E)
+  := do
+  let t ←
+    itertraitscollectFromIteratorInst.from_iter
+      itertraitscollectIntoIteratorInst iter_
+  Aeneas.Std.Result.ok (result.Result.Ok t)
+
+/-- Trait implementation: [core_models::result::{impl core_models::iter::traits::collect::FromIterator<core_models::result::Result<A, E>> for core_models::result::Result<V, E>}]
+    Source: 'core-models/src/core/result.rs', lines 296:0-302:1 -/
+@[reducible]
+def result.Result.Insts.CoreIterTraitsCollectFromIteratorResult {A :
+  Type} (E : Type) {V : Type} (itertraitscollectFromIteratorInst :
+  iter.traits.collect.FromIterator V A) : iter.traits.collect.FromIterator
+  (result.Result V E) (result.Result A E) := {
+  from_iter := fun {T : Type} {Clause0_Item : Type} {Clause0_IntoIter : Type}
+    (itertraitscollectIntoIteratorInst : iter.traits.collect.IntoIterator T
+    Clause0_Item Clause0_IntoIter) =>
+    result.Result.Insts.CoreIterTraitsCollectFromIteratorResult.from_iter
+    E itertraitscollectFromIteratorInst itertraitscollectIntoIteratorInst
+}
+
+/-- [core_models::result::{impl core_models::ops::try_trait::Try<T, core_models::result::Result<core_models::convert::Infallible, E>> for core_models::result::Result<T, E>}::branch]:
+    Source: 'core-models/src/core/result.rs', lines 314:4-319:5
+    Visibility: public -/
+def result.Result.Insts.CoreOpsTry_traitTryTResultInfallibleE.branch
+  {T : Type} {E : Type} (self : result.Result T E) :
+  Aeneas.Std.Result (ops.control_flow.ControlFlow (result.Result convert.Infallible E) T)
+  := do
+  match self with
+  | core.result.Result.Ok v => Aeneas.Std.Result.ok (ops.control_flow.ControlFlow.Continue v)
+  | core.result.Result.Err e =>
+    Aeneas.Std.Result.ok (ops.control_flow.ControlFlow.Break (result.Result.Err e))
+
+/-- [core_models::result::{impl core_models::ops::try_trait::Try<T, core_models::result::Result<core_models::convert::Infallible, E>> for core_models::result::Result<T, E>}::from_output]:
+    Source: 'core-models/src/core/result.rs', lines 309:4-311:5
+    Visibility: public -/
+def
+  result.Result.Insts.CoreOpsTry_traitTryTResultInfallibleE.from_output
+  {T : Type} (E : Type) (output : T) : Aeneas.Std.Result (result.Result T E) := do
+  Aeneas.Std.Result.ok (result.Result.Ok output)
+
+/-- Trait implementation: [core_models::result::{impl core_models::ops::try_trait::Try<T, core_models::result::Result<core_models::convert::Infallible, E>> for core_models::result::Result<T, E>}]
+    Source: 'core-models/src/core/result.rs', lines 304:0-320:1 -/
+@[reducible]
+def result.Result.Insts.CoreOpsTry_traitTryTResultInfallibleE (T : Type)
+  (E : Type) : ops.try_trait.Try (result.Result T E) T (result.Result
+  convert.Infallible E) := {
+  from_output :=
+    result.Result.Insts.CoreOpsTry_traitTryTResultInfallibleE.from_output
+    E
+  branch :=
+    result.Result.Insts.CoreOpsTry_traitTryTResultInfallibleE.branch
+}
+
 /-- [core_models::slice::iter::{core_models::slice::iter::Chunks<'a, T>}::new]:
     Source: 'core-models/src/core/slice.rs', lines 17:8-19:9
     Visibility: public -/
@@ -9513,8 +9592,422 @@ def slice.iter.Windows.new
   := do
   ok { size, elements }
 
+/-- [core_models::slice::{impl core_models::cmp::PartialEq<[U]> for [T]}::eq]: loop body 0:
+    Source: 'core-models/src/core/slice.rs', lines 261:12-265:13
+    Visibility: public -/
+@[rust_loop_body]
+def Slice.Insts.CoreCmpPartialEqSlice.eq_loop.body
+  {U : Type} {T : Type} (cmpPartialEqInst : cmp.PartialEq T U) (self : Slice T)
+  (other : Slice U) (iter_ : core.ops.range.Range Std.Usize) (res : Bool) :
+  Result (ControlFlow ((core.ops.range.Range Std.Usize) × Bool) Bool)
+  := do
+  let (o, iter1) ←
+    core.ops.range.Range.Insts.CoreIterTraitsIteratorIterator.next
+      core.Usize.Insts.CoreIterRangeStep iter_
+  match o with
+  | core.option.Option.None => ok (done res)
+  | core.option.Option.Some i =>
+    let t ← Slice.index_usize self i
+    let t1 ← Slice.index_usize other i
+    let b ← cmpPartialEqInst.eq t t1
+    if b
+    then ok (cont (iter1, res))
+    else ok (cont (iter1, false))
+
+/-- [core_models::slice::{impl core_models::cmp::PartialEq<[U]> for [T]}::eq]: loop 0:
+    Source: 'core-models/src/core/slice.rs', lines 261:12-265:13
+    Visibility: public -/
+@[rust_loop]
+def Slice.Insts.CoreCmpPartialEqSlice.eq_loop
+  {U : Type} {T : Type} (cmpPartialEqInst : cmp.PartialEq T U)
+  (iter_ : core.ops.range.Range Std.Usize) (self : Slice T) (other : Slice U)
+  (res : Bool) :
+  Result Bool
+  := do
+  loop
+    (fun (iter1, res1) => Slice.Insts.CoreCmpPartialEqSlice.eq_loop.body
+      cmpPartialEqInst self other iter1 res1)
+    (iter_, res)
+
+/-- [core_models::slice::{impl core_models::cmp::PartialEq<[U]> for [T]}::eq]:
+    Source: 'core-models/src/core/slice.rs', lines 256:4-268:5
+    Visibility: public -/
+def Slice.Insts.CoreCmpPartialEqSlice.eq
+  {U : Type} {T : Type} (cmpPartialEqInst : cmp.PartialEq T U) (self : Slice T)
+  (other : Slice U) :
+  Result Bool
+  := do
+  let i ← core.slice.Slice.len self
+  let i1 ← core.slice.Slice.len other
+  if i != i1
+  then ok false
+  else
+    Slice.Insts.CoreCmpPartialEqSlice.eq_loop cmpPartialEqInst
+      { start := 0#usize, «end» := i } self other true
+
+/-- Trait implementation: [core_models::slice::{impl core_models::cmp::PartialEq<[U]> for [T]}]
+    Source: 'core-models/src/core/slice.rs', lines 255:0-269:1 -/
+@[reducible]
+def Slice.Insts.CoreCmpPartialEqSlice {U : Type} {T : Type}
+  (cmpPartialEqInst : cmp.PartialEq T U) : cmp.PartialEq (Slice T) (Slice U)
+  := {
+  eq := Slice.Insts.CoreCmpPartialEqSlice.eq cmpPartialEqInst
+}
+
+/-- Trait implementation: [core_models::slice::{impl core_models::cmp::Eq for [T]}]
+    Source: 'core-models/src/core/slice.rs', lines 271:0-271:49 -/
+@[reducible]
+def Slice.Insts.CoreCmpEq {T : Type} (cmpEqInst : cmp.Eq T) : cmp.Eq
+  (Slice T) := {
+  PartialEqInst := Slice.Insts.CoreCmpPartialEqSlice
+    cmpEqInst.PartialEqInst
+}
+
+/-- [core_models::slice::{impl core_models::cmp::PartialOrd<[T]> for [T]}::partial_cmp]: loop body 0:
+    Source: 'core-models/src/core/slice.rs', lines 282:8-296:5
+    Visibility: public -/
+@[rust_loop_body]
+def Slice.Insts.CoreCmpPartialOrdSlice.partial_cmp_loop.body
+  {T : Type} (cmpPartialOrdInst : cmp.PartialOrd T T) (self : Slice T)
+  (other : Slice T) (iter_ : core.ops.range.Range Std.Usize) :
+  Result (ControlFlow (core.ops.range.Range Std.Usize) (option.Option
+    cmp.Ordering))
+  := do
+  let (o, iter1) ←
+    core.ops.range.Range.Insts.CoreIterTraitsIteratorIterator.next
+      core.Usize.Insts.CoreIterRangeStep iter_
+  match o with
+  | core.option.Option.None =>
+    let i ← core.slice.Slice.len self
+    let i1 ← core.slice.Slice.len other
+    if i < i1
+    then ok (done (option.Option.Some cmp.Ordering.Less))
+    else
+      if i > i1
+      then ok (done (option.Option.Some cmp.Ordering.Greater))
+      else ok (done (option.Option.Some cmp.Ordering.Equal))
+  | core.option.Option.Some i =>
+    let t ← Slice.index_usize self i
+    let t1 ← Slice.index_usize other i
+    let o1 ← cmpPartialOrdInst.partial_cmp t t1
+    match o1 with
+    | option.Option.Some o2 =>
+      match o2 with
+      | cmp.Ordering.Less => ok (done o1)
+      | cmp.Ordering.Equal => ok (cont iter1)
+      | cmp.Ordering.Greater => ok (done o1)
+    | option.Option.None => ok (done option.Option.None)
+
+/-- [core_models::slice::{impl core_models::cmp::PartialOrd<[T]> for [T]}::partial_cmp]: loop 0:
+    Source: 'core-models/src/core/slice.rs', lines 282:8-296:5
+    Visibility: public -/
+@[rust_loop]
+def Slice.Insts.CoreCmpPartialOrdSlice.partial_cmp_loop
+  {T : Type} (cmpPartialOrdInst : cmp.PartialOrd T T)
+  (iter_ : core.ops.range.Range Std.Usize) (self : Slice T) (other : Slice T) :
+  Result (option.Option cmp.Ordering)
+  := do
+  loop
+    (fun iter1 =>
+      Slice.Insts.CoreCmpPartialOrdSlice.partial_cmp_loop.body
+      cmpPartialOrdInst self other iter1)
+    iter_
+
+/-- [core_models::slice::{impl core_models::cmp::PartialOrd<[T]> for [T]}::partial_cmp]:
+    Source: 'core-models/src/core/slice.rs', lines 274:4-296:5
+    Visibility: public -/
+def Slice.Insts.CoreCmpPartialOrdSlice.partial_cmp
+  {T : Type} (cmpPartialOrdInst : cmp.PartialOrd T T) (self : Slice T)
+  (other : Slice T) :
+  Result (option.Option cmp.Ordering)
+  := do
+  let i ← core.slice.Slice.len self
+  let i1 ← core.slice.Slice.len other
+  let l ← if i < i1
+            then ok i
+            else ok i1
+  Slice.Insts.CoreCmpPartialOrdSlice.partial_cmp_loop cmpPartialOrdInst
+    { start := 0#usize, «end» := l } self other
+
+/-- Trait implementation: [core_models::slice::{impl core_models::cmp::PartialOrd<[T]> for [T]}]
+    Source: 'core-models/src/core/slice.rs', lines 273:0-297:1 -/
+@[reducible]
+def Slice.Insts.CoreCmpPartialOrdSlice {T : Type} (cmpPartialOrdInst :
+  cmp.PartialOrd T T) : cmp.PartialOrd (Slice T) (Slice T) := {
+  PartialEqInst := Slice.Insts.CoreCmpPartialEqSlice
+    cmpPartialOrdInst.PartialEqInst
+  partial_cmp := Slice.Insts.CoreCmpPartialOrdSlice.partial_cmp
+    cmpPartialOrdInst
+}
+
+/-- [core_models::slice::{impl core_models::cmp::Ord for [T]}::cmp]: loop body 0:
+    Source: 'core-models/src/core/slice.rs', lines 308:8-322:5
+    Visibility: public -/
+@[rust_loop_body]
+def Slice.Insts.CoreCmpOrd.cmp_loop.body
+  {T : Type} (cmpOrdInst : cmp.Ord T) (self : Slice T) (other : Slice T)
+  (iter_ : core.ops.range.Range Std.Usize) :
+  Result (ControlFlow (core.ops.range.Range Std.Usize) cmp.Ordering)
+  := do
+  let (o, iter1) ←
+    core.ops.range.Range.Insts.CoreIterTraitsIteratorIterator.next
+      core.Usize.Insts.CoreIterRangeStep iter_
+  match o with
+  | core.option.Option.None =>
+    let i ← core.slice.Slice.len self
+    let i1 ← core.slice.Slice.len other
+    if i < i1
+    then ok (done cmp.Ordering.Less)
+    else
+      if i > i1
+      then ok (done cmp.Ordering.Greater)
+      else ok (done cmp.Ordering.Equal)
+  | core.option.Option.Some i =>
+    let t ← Slice.index_usize self i
+    let t1 ← Slice.index_usize other i
+    let o1 ← cmpOrdInst.cmp t t1
+    match o1 with
+    | cmp.Ordering.Less => ok (done cmp.Ordering.Less)
+    | cmp.Ordering.Equal => ok (cont iter1)
+    | cmp.Ordering.Greater => ok (done cmp.Ordering.Greater)
+
+/-- [core_models::slice::{impl core_models::cmp::Ord for [T]}::cmp]: loop 0:
+    Source: 'core-models/src/core/slice.rs', lines 308:8-322:5
+    Visibility: public -/
+@[rust_loop]
+def Slice.Insts.CoreCmpOrd.cmp_loop
+  {T : Type} (cmpOrdInst : cmp.Ord T) (iter_ : core.ops.range.Range Std.Usize)
+  (self : Slice T) (other : Slice T) :
+  Result cmp.Ordering
+  := do
+  loop
+    (fun iter1 => Slice.Insts.CoreCmpOrd.cmp_loop.body cmpOrdInst self
+      other iter1)
+    iter_
+
+/-- [core_models::slice::{impl core_models::cmp::Ord for [T]}::cmp]:
+    Source: 'core-models/src/core/slice.rs', lines 300:4-322:5
+    Visibility: public -/
+def Slice.Insts.CoreCmpOrd.cmp
+  {T : Type} (cmpOrdInst : cmp.Ord T) (self : Slice T) (other : Slice T) :
+  Result cmp.Ordering
+  := do
+  let i ← core.slice.Slice.len self
+  let i1 ← core.slice.Slice.len other
+  let l ← if i < i1
+            then ok i
+            else ok i1
+  Slice.Insts.CoreCmpOrd.cmp_loop cmpOrdInst
+    { start := 0#usize, «end» := l } self other
+
+/-- Trait implementation: [core_models::slice::{impl core_models::cmp::Ord for [T]}]
+    Source: 'core-models/src/core/slice.rs', lines 299:0-323:1 -/
+@[reducible]
+def Slice.Insts.CoreCmpOrd {T : Type} (cmpOrdInst : cmp.Ord T) : cmp.Ord
+  (Slice T) := {
+  EqInst := Slice.Insts.CoreCmpEq cmpOrdInst.EqInst
+  PartialOrdInst := Slice.Insts.CoreCmpPartialOrdSlice
+    cmpOrdInst.PartialOrdInst
+  cmp := Slice.Insts.CoreCmpOrd.cmp cmpOrdInst
+}
+
+/-- [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], T> for usize}::index]:
+    Source: 'core-models/src/core/slice.rs', lines 374:8-376:9
+    Visibility: public -/
+def Usize.Insts.CoreSliceIndexSliceIndexSliceT.index
+  {T : Type} (self : Std.Usize) (slice : Slice T) : Result T := do
+  rust_primitives.slice.slice_index slice self
+
+/-- [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], T> for usize}::get]:
+    Source: 'core-models/src/core/slice.rs', lines 366:8-372:9
+    Visibility: public -/
+def Usize.Insts.CoreSliceIndexSliceIndexSliceT.get
+  {T : Type} (self : Std.Usize) (slice : Slice T) :
+  Result (option.Option T)
+  := do
+  let i ← rust_primitives.slice.slice_length slice
+  if self < i
+  then
+    let t ← rust_primitives.slice.slice_index slice self
+    ok (option.Option.Some t)
+  else ok option.Option.None
+
+/-- Trait implementation: [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], T> for usize}]
+    Source: 'core-models/src/core/slice.rs', lines 364:4-377:5 -/
+@[reducible]
+def Usize.Insts.CoreSliceIndexSliceIndexSliceT (T : Type) :
+  slice.index.SliceIndex Std.Usize (Slice T) T := {
+  get := Usize.Insts.CoreSliceIndexSliceIndexSliceT.get
+  index := Usize.Insts.CoreSliceIndexSliceIndexSliceT.index
+}
+
+/-- [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::RangeFull}::index]:
+    Source: 'core-models/src/core/slice.rs', lines 386:8-388:9
+    Visibility: public -/
+def ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index
+  {T : Type} (self : ops.range.RangeFull) (slice : Slice T) :
+  Result (Slice T)
+  := do
+  ok slice
+
+/-- [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::RangeFull}::get]:
+    Source: 'core-models/src/core/slice.rs', lines 383:8-385:9
+    Visibility: public -/
+def ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
+  {T : Type} (self : ops.range.RangeFull) (slice : Slice T) :
+  Result (option.Option (Slice T))
+  := do
+  ok (option.Option.Some slice)
+
+/-- Trait implementation: [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::RangeFull}]
+    Source: 'core-models/src/core/slice.rs', lines 381:4-389:5 -/
+@[reducible]
+def ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice (T :
+  Type) : slice.index.SliceIndex ops.range.RangeFull (Slice T) (Slice T) := {
+  get :=
+    ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
+  index :=
+    ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index
+}
+
+/-- [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::RangeFrom<usize>}::index]:
+    Source: 'core-models/src/core/slice.rs', lines 403:8-405:9
+    Visibility: public -/
+def
+  ops.range.RangeFromUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.index
+  {T : Type} (self : ops.range.RangeFrom Std.Usize) (slice : Slice T) :
+  Result (Slice T)
+  := do
+  let i ← rust_primitives.slice.slice_length slice
+  rust_primitives.slice.slice_slice slice self.start i
+
+/-- [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::RangeFrom<usize>}::get]:
+    Source: 'core-models/src/core/slice.rs', lines 395:8-401:9
+    Visibility: public -/
+def
+  ops.range.RangeFromUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.get
+  {T : Type} (self : ops.range.RangeFrom Std.Usize) (slice : Slice T) :
+  Result (option.Option (Slice T))
+  := do
+  let i ← rust_primitives.slice.slice_length slice
+  if self.start <= i
+  then
+    let s ← rust_primitives.slice.slice_slice slice self.start i
+    ok (option.Option.Some s)
+  else ok option.Option.None
+
+/-- Trait implementation: [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::RangeFrom<usize>}]
+    Source: 'core-models/src/core/slice.rs', lines 393:4-406:5 -/
+@[reducible]
+def ops.range.RangeFromUsize.Insts.CoreSliceIndexSliceIndexSliceSlice (T
+  : Type) : slice.index.SliceIndex (ops.range.RangeFrom Std.Usize) (Slice T)
+  (Slice T) := {
+  get :=
+    ops.range.RangeFromUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.get
+  index :=
+    ops.range.RangeFromUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.index
+}
+
+/-- [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::RangeTo<usize>}::index]:
+    Source: 'core-models/src/core/slice.rs', lines 419:8-421:9
+    Visibility: public -/
+def
+  ops.range.RangeToUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.index
+  {T : Type} (self : ops.range.RangeTo Std.Usize) (slice : Slice T) :
+  Result (Slice T)
+  := do
+  rust_primitives.slice.slice_slice slice 0#usize self.«end»
+
+/-- [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::RangeTo<usize>}::get]:
+    Source: 'core-models/src/core/slice.rs', lines 411:8-417:9
+    Visibility: public -/
+def ops.range.RangeToUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.get
+  {T : Type} (self : ops.range.RangeTo Std.Usize) (slice : Slice T) :
+  Result (option.Option (Slice T))
+  := do
+  let i ← rust_primitives.slice.slice_length slice
+  if self.«end» <= i
+  then
+    let s ← rust_primitives.slice.slice_slice slice 0#usize self.«end»
+    ok (option.Option.Some s)
+  else ok option.Option.None
+
+/-- Trait implementation: [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::RangeTo<usize>}]
+    Source: 'core-models/src/core/slice.rs', lines 409:4-422:5 -/
+@[reducible]
+def ops.range.RangeToUsize.Insts.CoreSliceIndexSliceIndexSliceSlice (T :
+  Type) : slice.index.SliceIndex (ops.range.RangeTo Std.Usize) (Slice T) (Slice
+  T) := {
+  get :=
+    ops.range.RangeToUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.get
+  index :=
+    ops.range.RangeToUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.index
+}
+
+/-- [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::Range<usize>}::index]:
+    Source: 'core-models/src/core/slice.rs', lines 435:8-437:9
+    Visibility: public -/
+def ops.range.RangeUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.index
+  {T : Type} (self : ops.range.Range Std.Usize) (slice : Slice T) :
+  Result (Slice T)
+  := do
+  rust_primitives.slice.slice_slice slice self.start self.«end»
+
+/-- [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::Range<usize>}::get]:
+    Source: 'core-models/src/core/slice.rs', lines 427:8-433:9
+    Visibility: public -/
+def ops.range.RangeUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.get
+  {T : Type} (self : ops.range.Range Std.Usize) (slice : Slice T) :
+  Result (option.Option (Slice T))
+  := do
+  if self.start <= self.«end»
+  then
+    let i ← rust_primitives.slice.slice_length slice
+    if self.«end» <= i
+    then
+      let s ← rust_primitives.slice.slice_slice slice self.start self.«end»
+      ok (option.Option.Some s)
+    else ok option.Option.None
+  else ok option.Option.None
+
+/-- Trait implementation: [core_models::slice::index::{impl core_models::slice::index::SliceIndex<[T], [T]> for core_models::ops::range::Range<usize>}]
+    Source: 'core-models/src/core/slice.rs', lines 425:4-438:5 -/
+@[reducible]
+def ops.range.RangeUsize.Insts.CoreSliceIndexSliceIndexSliceSlice (T :
+  Type) : slice.index.SliceIndex (ops.range.Range Std.Usize) (Slice T) (Slice
+  T) := {
+  get :=
+    ops.range.RangeUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.get
+  index :=
+    ops.range.RangeUsize.Insts.CoreSliceIndexSliceIndexSliceSlice.index
+}
+
+/-- [core_models::slice::index::{impl core_models::ops::index::Index<I, Clause0_Output> for [T]}::index]:
+    Source: 'core-models/src/core/slice.rs', lines 454:8-459:9
+    Visibility: public -/
+def Slice.Insts.CoreOpsIndexIndex.index
+  {T : Type} {I : Type} {Clause0_Output : Type}
+  (SliceIndexISliceClause0_OutputInst : slice.index.SliceIndex I (Slice T)
+  Clause0_Output) (self : Slice T) (i : I) :
+  Result Clause0_Output
+  := do
+  let o ← SliceIndexISliceClause0_OutputInst.get i self
+  match o with
+  | option.Option.Some r => ok r
+  | option.Option.None => panicking.internal.panic Clause0_Output
+
+/-- Trait implementation: [core_models::slice::index::{impl core_models::ops::index::Index<I, Clause0_Output> for [T]}]
+    Source: 'core-models/src/core/slice.rs', lines 448:4-460:5 -/
+@[reducible]
+def Slice.Insts.CoreOpsIndexIndex {T : Type} {I : Type} {Clause0_Output
+  : Type} (SliceIndexISliceClause0_OutputInst : slice.index.SliceIndex I (Slice
+  T) Clause0_Output) : ops.index.Index (Slice T) I Clause0_Output := {
+  index := Slice.Insts.CoreOpsIndexIndex.index
+    SliceIndexISliceClause0_OutputInst
+}
+
 /-- [core_models::slice::{impl core_models::ops::index::Index<core_models::ops::range::Range<usize>, [T]> for &'_0 [T]}::index]:
-    Source: 'core-models/src/core/slice.rs', lines 405:4-407:5
+    Source: 'core-models/src/core/slice.rs', lines 475:4-477:5
     Visibility: public -/
 def Shared0Slice.Insts.CoreOpsIndexIndexRangeUsizeSlice.index
   {T : Type} (self : Slice T) (i : ops.range.Range Std.Usize) :
@@ -9523,7 +10016,7 @@ def Shared0Slice.Insts.CoreOpsIndexIndexRangeUsizeSlice.index
   rust_primitives.slice.slice_slice self i.start i.«end»
 
 /-- Trait implementation: [core_models::slice::{impl core_models::ops::index::Index<core_models::ops::range::Range<usize>, [T]> for &'_0 [T]}]
-    Source: 'core-models/src/core/slice.rs', lines 402:0-408:1 -/
+    Source: 'core-models/src/core/slice.rs', lines 472:0-478:1 -/
 @[reducible]
 def Shared0Slice.Insts.CoreOpsIndexIndexRangeUsizeSlice (T : Type) :
   ops.index.Index (Slice T) (ops.range.Range Std.Usize) (Slice T) := {
@@ -9531,7 +10024,7 @@ def Shared0Slice.Insts.CoreOpsIndexIndexRangeUsizeSlice (T : Type) :
 }
 
 /-- [core_models::slice::{impl core_models::ops::index::Index<core_models::ops::range::RangeTo<usize>, [T]> for &'_0 [T]}::index]:
-    Source: 'core-models/src/core/slice.rs', lines 414:4-416:5
+    Source: 'core-models/src/core/slice.rs', lines 484:4-486:5
     Visibility: public -/
 def Shared0Slice.Insts.CoreOpsIndexIndexRangeToUsizeSlice.index
   {T : Type} (self : Slice T) (i : ops.range.RangeTo Std.Usize) :
@@ -9540,7 +10033,7 @@ def Shared0Slice.Insts.CoreOpsIndexIndexRangeToUsizeSlice.index
   rust_primitives.slice.slice_slice self 0#usize i.«end»
 
 /-- Trait implementation: [core_models::slice::{impl core_models::ops::index::Index<core_models::ops::range::RangeTo<usize>, [T]> for &'_0 [T]}]
-    Source: 'core-models/src/core/slice.rs', lines 411:0-417:1 -/
+    Source: 'core-models/src/core/slice.rs', lines 481:0-487:1 -/
 @[reducible]
 def Shared0Slice.Insts.CoreOpsIndexIndexRangeToUsizeSlice (T : Type) :
   ops.index.Index (Slice T) (ops.range.RangeTo Std.Usize) (Slice T) := {
@@ -9548,7 +10041,7 @@ def Shared0Slice.Insts.CoreOpsIndexIndexRangeToUsizeSlice (T : Type) :
 }
 
 /-- [core_models::slice::{impl core_models::ops::index::Index<core_models::ops::range::RangeFrom<usize>, [T]> for &'_0 [T]}::index]:
-    Source: 'core-models/src/core/slice.rs', lines 423:4-425:5
+    Source: 'core-models/src/core/slice.rs', lines 493:4-495:5
     Visibility: public -/
 def Shared0Slice.Insts.CoreOpsIndexIndexRangeFromUsizeSlice.index
   {T : Type} (self : Slice T) (i : ops.range.RangeFrom Std.Usize) :
@@ -9558,7 +10051,7 @@ def Shared0Slice.Insts.CoreOpsIndexIndexRangeFromUsizeSlice.index
   rust_primitives.slice.slice_slice self i.start i1
 
 /-- Trait implementation: [core_models::slice::{impl core_models::ops::index::Index<core_models::ops::range::RangeFrom<usize>, [T]> for &'_0 [T]}]
-    Source: 'core-models/src/core/slice.rs', lines 420:0-426:1 -/
+    Source: 'core-models/src/core/slice.rs', lines 490:0-496:1 -/
 @[reducible]
 def Shared0Slice.Insts.CoreOpsIndexIndexRangeFromUsizeSlice (T : Type) :
   ops.index.Index (Slice T) (ops.range.RangeFrom Std.Usize) (Slice T) := {
@@ -9566,7 +10059,7 @@ def Shared0Slice.Insts.CoreOpsIndexIndexRangeFromUsizeSlice (T : Type) :
 }
 
 /-- [core_models::slice::{impl core_models::ops::index::Index<core_models::ops::range::RangeFull, [T]> for &'_0 [T]}::index]:
-    Source: 'core-models/src/core/slice.rs', lines 431:4-433:5
+    Source: 'core-models/src/core/slice.rs', lines 501:4-503:5
     Visibility: public -/
 def Shared0Slice.Insts.CoreOpsIndexIndexRangeFullSlice.index
   {T : Type} (self : Slice T) (i : ops.range.RangeFull) :
@@ -9576,7 +10069,7 @@ def Shared0Slice.Insts.CoreOpsIndexIndexRangeFullSlice.index
   rust_primitives.slice.slice_slice self 0#usize i1
 
 /-- Trait implementation: [core_models::slice::{impl core_models::ops::index::Index<core_models::ops::range::RangeFull, [T]> for &'_0 [T]}]
-    Source: 'core-models/src/core/slice.rs', lines 429:0-434:1 -/
+    Source: 'core-models/src/core/slice.rs', lines 499:0-504:1 -/
 @[reducible]
 def Shared0Slice.Insts.CoreOpsIndexIndexRangeFullSlice (T : Type) :
   ops.index.Index (Slice T) ops.range.RangeFull (Slice T) := {
@@ -9584,14 +10077,14 @@ def Shared0Slice.Insts.CoreOpsIndexIndexRangeFullSlice (T : Type) :
 }
 
 /-- [core_models::slice::{impl core_models::ops::index::Index<usize, T> for &'_0 [T]}::index]:
-    Source: 'core-models/src/core/slice.rs', lines 441:4-443:5
+    Source: 'core-models/src/core/slice.rs', lines 511:4-513:5
     Visibility: public -/
 def Shared0Slice.Insts.CoreOpsIndexIndexUsizeT.index
   {T : Type} (self : Slice T) (i : Std.Usize) : Result T := do
   rust_primitives.slice.slice_index self i
 
 /-- Trait implementation: [core_models::slice::{impl core_models::ops::index::Index<usize, T> for &'_0 [T]}]
-    Source: 'core-models/src/core/slice.rs', lines 438:0-444:1 -/
+    Source: 'core-models/src/core/slice.rs', lines 508:0-514:1 -/
 @[reducible]
 def Shared0Slice.Insts.CoreOpsIndexIndexUsizeT (T : Type) :
   ops.index.Index (Slice T) Std.Usize T := {
@@ -9618,4 +10111,75 @@ def U64.Insts.CoreStrTraitsFromStrU64 : str.traits.FromStr Std.U64
   from_str := U64.Insts.CoreStrTraitsFromStrU64.from_str
 }
 
+
+/-- [core_models::iter::adapters::step_by::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::step_by::StepBy<I>}::next]: loop body 0:
+    Source: 'core-models/src/core/iter.rs', lines 458:16-464:13
+    Visibility: public -/
+@[rust_loop_body]
+def
+  iter.adapters.step_by.StepBy.Insts.CoreIterTraitsIteratorIterator.next_loop.body
+  {I : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
+  iter.traits.iterator.Iterator I Clause0_Item)
+  (iter_ : core.ops.range.Range Std.Usize) (t : I) :
+  Result (ControlFlow ((core.ops.range.Range Std.Usize) × I) ((option.Option
+    Clause0_Item) × I))
+  := do
+  let (o, iter1) ←
+    core.ops.range.Range.Insts.CoreIterTraitsIteratorIterator.next
+      core.Usize.Insts.CoreIterRangeStep iter_
+  match o with
+  | core.option.Option.None =>
+    let (o1, t1) ← traitsiteratorIteratorInst.next t
+    ok (done (o1, t1))
+  | core.option.Option.Some _ =>
+    let (o1, t1) ← traitsiteratorIteratorInst.next t
+    match o1 with
+    | option.Option.Some _ => ok (cont (iter1, t1))
+    | option.Option.None => ok (done (option.Option.None, t1))
+
+/-- [core_models::iter::adapters::step_by::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::step_by::StepBy<I>}::next]: loop 0:
+    Source: 'core-models/src/core/iter.rs', lines 458:16-464:13
+    Visibility: public -/
+@[rust_loop]
+def
+  iter.adapters.step_by.StepBy.Insts.CoreIterTraitsIteratorIterator.next_loop
+  {I : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
+  iter.traits.iterator.Iterator I Clause0_Item)
+  (iter_ : core.ops.range.Range Std.Usize) (t : I) :
+  Result ((option.Option Clause0_Item) × I)
+  := do
+  loop
+    (fun (iter1, t1) =>
+      iter.adapters.step_by.StepBy.Insts.CoreIterTraitsIteratorIterator.next_loop.body
+      traitsiteratorIteratorInst iter1 t1)
+    (iter_, t)
+
+/-- [core_models::iter::adapters::step_by::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::step_by::StepBy<I>}::next]:
+    Source: 'core-models/src/core/iter.rs', lines 457:12-464:13
+    Visibility: public -/
+def
+  iter.adapters.step_by.StepBy.Insts.CoreIterTraitsIteratorIterator.next
+  {I : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
+  iter.traits.iterator.Iterator I Clause0_Item)
+  (self : iter.adapters.step_by.StepBy I) :
+  Result ((option.Option Clause0_Item) × (iter.adapters.step_by.StepBy I))
+  := do
+  let (o, t) ←
+    iter.adapters.step_by.StepBy.Insts.CoreIterTraitsIteratorIterator.next_loop
+      traitsiteratorIteratorInst { start := 1#usize, «end» := self.step }
+      self.iter
+  ok (o, { self with iter := t })
+
+/-- Trait implementation: [core_models::iter::adapters::step_by::{impl core_models::iter::traits::iterator::Iterator<Clause0_Item> for core_models::iter::adapters::step_by::StepBy<I>}]
+    Source: 'core-models/src/core/iter.rs', lines 454:8-465:9 -/
+@[reducible]
+def iter.adapters.step_by.StepBy.Insts.CoreIterTraitsIteratorIterator {I
+  : Type} {Clause0_Item : Type} (traitsiteratorIteratorInst :
+  iter.traits.iterator.Iterator I Clause0_Item) : iter.traits.iterator.Iterator
+  (iter.adapters.step_by.StepBy I) Clause0_Item := {
+  next :=
+    iter.adapters.step_by.StepBy.Insts.CoreIterTraitsIteratorIterator.next
+    traitsiteratorIteratorInst
+}
+
 end CoreModels.core
diff --git a/lean/CoreModels/Core/FunsEpilogue.lean b/lean/CoreModels/Core/FunsEpilogue.lean
index 1f3754a..95fe915 100644
--- a/lean/CoreModels/Core/FunsEpilogue.lean
+++ b/lean/CoreModels/Core/FunsEpilogue.lean
@@ -40,6 +40,52 @@ end core
 
 namespace alloc
 
+/-! ## `IntoIter::map` (a provided `Iterator` method)
+
+`map` lives on the extraction-excluded `IteratorMethods` trait, so Aeneas
+never synthesises the per-impl `Iterator::map` specialisation that a
+downstream crate references when it writes `v.into_iter().map(f)`. We supply
+it by hand, mirroring Aeneas's own builtin `Aeneas/Std/VecIter.lean` (which
+this project shadows via `open Aeneas.Std hiding namespace core alloc`).
+
+The `@[rust_fun "…"]` attribute binds the Rust path of the provided method to
+this body, so the downstream name-map lands here. The body just builds the
+`Map` adapter; iteration then runs through `Map`'s own `Iterator` instance.
+`F` is the closure, `T` the item, `O` its output (the `FnMut` instance is
+irrelevant to the model, hence `_`-prefixed). -/
+@[rust_fun "alloc::vec::into_iter::{core::iter::traits::iterator::Iterator<alloc::vec::into_iter::IntoIter<@T, @A>, @T>}::map"]
+def vec.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.map
+  {T O F : Type} (_FnMutInst : core.ops.function.FnMut F T O) :
+  vec.into_iter.IntoIter T → F →
+  Aeneas.Std.Result (core.iter.adapters.map.Map (vec.into_iter.IntoIter T) F) :=
+  fun it f => .ok { iter := it, f := f }
+
+/-! ## `FromIterator<T>` for `VecDeque<T, Global>`
+
+Like `Vec`'s `FromIterator`, this impl is `--exclude`d from charon: alloc
+implements *std*'s `FromIterator`, whose `from_iter<I: IntoIterator<Item = A>>`
+pins the iterator's `Item` to the element type, which cannot match
+core-models' deliberately bound-free `FromIterator::from_iter<T: IntoIterator>`
+(its `Clause0_Item` is a free implicit). So we supply the instance by hand,
+binding `Item` free to match the trait field.
+
+NOTE: this is a *stub* — `from_iter` returns an empty deque. We cannot model
+the real collect: core-models' `IntoIterator` carries no `Iterator`
+super-instance (the `iteratorIteratorInst` field was dropped), so there is no
+`next` to drive a fold here. Refine if downstream reasoning depends on the
+contents of a `VecDeque::from_iter` result. -/
+@[rust_trait_impl "core::iter::traits::collect::FromIterator<alloc::collections::vec_deque::VecDeque<@T, alloc::alloc::Global>, @T>"]
+def collections.vec_deque.VecDequeTGlobal.Insts.CoreIterTraitsCollectFromIterator
+  (T : Type) :
+  core.iter.traits.collect.FromIterator
+    (collections.vec_deque.VecDeque T alloc.Global) T := {
+  from_iter := fun {U Item IntoIter}
+    (_IntoIteratorInst : core.iter.traits.collect.IntoIterator U Item IntoIter)
+    (_iter : U) => do
+    let s ← rust_primitives.sequence.seq_empty T
+    Aeneas.Std.Result.ok (s, core.marker.PhantomData.mk)
+}
+
 /-! ## `[T]::to_vec` and `Box<[T]>::into_vec`
 
 Aeneas's builtin name map turns `<[T]>::to_vec` into a reference to
@@ -55,18 +101,22 @@ noncomputable section
 @[rust_fun "alloc::slice::{[@T]}::to_vec"]
 def slice.Slice.to_vec
   {T : Type} (cloneInst : core.clone.Clone T) (s : Aeneas.Std.Slice T) :
-  Aeneas.Std.Result (vec.Vec T alloc.Global) :=
+  Aeneas.Std.Result (vec.Vec T) :=
   slice.Dummy.to_vec cloneInst s
 
 @[rust_fun "alloc::slice::{alloc::boxed::Box<[@T], @A>}::into_vec"]
 def slice.Slice.into_vec
-  {T : Type} (A : Type) (s : Aeneas.Std.Slice T) : Aeneas.Std.Result (vec.Vec T A) :=
-  slice.Dummy.into_vec A s
+  {T : Type} (s : Aeneas.Std.Slice T) : Aeneas.Std.Result (vec.Vec T) :=
+  slice.Dummy.into_vec s
 
 end
 
-def vec.Vec.new := @vec.VecTGlobal.new
-def vec.Vec.with_capacity := @vec.VecTGlobal.with_capacity
+-- `vec.Vec.new` / `vec.Vec.with_capacity` are now extracted directly into
+-- `CoreModels.Alloc` (and `vec.VecTGlobal` no longer exists, since `vec.Vec`
+-- dropped its allocator type parameter), so these manual re-exports are
+-- obsolete:
+-- def vec.Vec.new := @vec.VecTGlobal.new
+-- def vec.Vec.with_capacity := @vec.VecTGlobal.with_capacity
 
 end alloc
 end CoreModels
diff --git a/lean/CoreModels/Core/FunsPrologue.lean b/lean/CoreModels/Core/FunsPrologue.lean
index e67b3cd..95a60f1 100644
--- a/lean/CoreModels/Core/FunsPrologue.lean
+++ b/lean/CoreModels/Core/FunsPrologue.lean
@@ -4,6 +4,7 @@
 -/
 import CoreModels.Core.Types
 import CoreModels.Alloc.Types
+import CoreModels.RustPrimitives.Funs
 
 namespace CoreModels.core
 
@@ -75,6 +76,47 @@ instance I64.Insts.CoreCmpPartialOrdI64     : cmp.PartialOrd I64   I64   := mkIP
 instance I128.Insts.CoreCmpPartialOrdI128   : cmp.PartialOrd I128  I128  := mkIPartialOrd
 instance Isize.Insts.CoreCmpPartialOrdIsize : cmp.PartialOrd Isize Isize := mkIPartialOrd
 
+/-! ## Scalar `Ord` instances
+
+`core::cmp::Ord for <int>` is `aeneas::exclude`d in `cmp.rs` (like `PartialEq`
+/ `PartialOrd`), so — to match the excluded `PartialOrd` instances above — we
+re-provide it here. Without these, any model code requiring `T: Ord` on a
+scalar (e.g. `<[T]>::cmp`, sorting, `BinaryHeap`) references an undefined
+`<int>.Insts.CoreCmpOrd`. -/
+
+def mkUOrd {ty} : cmp.Ord (UScalar ty) := {
+  EqInst := { PartialEqInst := { eq := fun x y => ok (x == y) } }
+  PartialOrdInst := mkUPartialOrd
+  cmp := fun x y =>
+    ok (match compare x.val y.val with
+        | .lt => cmp.Ordering.Less
+        | .eq => cmp.Ordering.Equal
+        | .gt => cmp.Ordering.Greater)
+}
+
+def mkIOrd {ty} : cmp.Ord (IScalar ty) := {
+  EqInst := { PartialEqInst := { eq := fun x y => ok (x == y) } }
+  PartialOrdInst := mkIPartialOrd
+  cmp := fun x y =>
+    ok (match compare x.val y.val with
+        | .lt => cmp.Ordering.Less
+        | .eq => cmp.Ordering.Equal
+        | .gt => cmp.Ordering.Greater)
+}
+
+instance U8.Insts.CoreCmpOrd    : cmp.Ord U8    := mkUOrd
+instance U16.Insts.CoreCmpOrd   : cmp.Ord U16   := mkUOrd
+instance U32.Insts.CoreCmpOrd   : cmp.Ord U32   := mkUOrd
+instance U64.Insts.CoreCmpOrd   : cmp.Ord U64   := mkUOrd
+instance U128.Insts.CoreCmpOrd  : cmp.Ord U128  := mkUOrd
+instance Usize.Insts.CoreCmpOrd : cmp.Ord Usize := mkUOrd
+instance I8.Insts.CoreCmpOrd    : cmp.Ord I8    := mkIOrd
+instance I16.Insts.CoreCmpOrd   : cmp.Ord I16   := mkIOrd
+instance I32.Insts.CoreCmpOrd   : cmp.Ord I32   := mkIOrd
+instance I64.Insts.CoreCmpOrd   : cmp.Ord I64   := mkIOrd
+instance I128.Insts.CoreCmpOrd  : cmp.Ord I128  := mkIOrd
+instance Isize.Insts.CoreCmpOrd : cmp.Ord Isize := mkIOrd
+
 abbrev ops.range.Range.Insts.CoreIterTraitsIteratorIterator.next :=
   @IteratorRange.next
 
@@ -104,24 +146,38 @@ def Shared1A.Insts.CoreCmpPartialOrdShared0B.gt
   | some cmp.Ordering.Greater => ok true
   | _ => ok false
 
-/-- [core::slice::cmp::{core::cmp::PartialEq<[U]> for [T]}::eq]:
-    Source: '/rustc/library/core/src/slice/cmp.rs', lines 18:4-18:37
-    Name pattern: [core::slice::cmp::{core::cmp::PartialEq<[@T], [@U]>}::eq]
-    Visibility: public -/
-@[rust_fun "core::slice::cmp::{core::cmp::PartialEq<[@T], [@U]>}::eq"]
-def Slice.Insts.CoreCmpPartialEqSlice.eq
-  {T : Type} {U : Type} (cmpPartialEqInst : cmp.PartialEq T U) :
-  Slice T → Slice U → Result Bool := fun s1 s2 =>
-  if s1.length ≠ s2.length then ok false
-  else do
-    let rs ← (s1.val.zip s2.val).mapM (fun p => cmpPartialEqInst.eq p.1 p.2)
-    ok (rs.all id)
 
 /-! ## Slice -/
 
 def slice.Slice.len {T : Type u} (v : Aeneas.Std.Slice T) : Aeneas.Std.Result Usize :=
   pure (@Aeneas.Std.Slice.len T v)
 
+/-- `[T]::iter()` — constructs `core_models::slice::iter::Iter<'a, T>`.
+
+    Part of the `aeneas::exclude`d `impl Slice<T>` block (like `len` above), so
+    it's provided here. The Rust is `Iter(seq_from_slice(s))`; since the model
+    is `Iter T := Seq T` (refs erased), the `Iter(…)` wrap is the identity. -/
+def slice.Slice.iter {T : Type} (s : Aeneas.Std.Slice T) :
+    Result (slice.iter.Iter T) :=
+  rust_primitives.sequence.seq_from_slice s
+
+/-- `Iterator::next` for `core_models::slice::iter::Iter<'a, T>` (the iterator
+    returned by `[T]::iter()`, with `Item = &'a T`).
+
+    The `impl … Iterator for Iter` is `aeneas::exclude`d (aeneas#805), so Aeneas
+    emits *references* to this `next` — e.g. from `Vec::clone`'s loop in
+    `Alloc/Funs.lean` — but never a body. The model erases the `&'a`, so `Iter`
+    is just the remaining `Seq T`; `next` pops the front element. This mirrors
+    the generated `vec.into_iter.IntoIter` `next`. -/
+def slice.iter.Iter.Insts.CoreIterTraitsIteratorIteratorSharedAT.next
+    {T : Type} (self : slice.iter.Iter T) :
+    Result ((option.Option T) × slice.iter.Iter T) := do
+  let i ← rust_primitives.sequence.seq_len self
+  if i = 0#usize then ok (option.Option.None, self)
+  else
+    let (t, s) ← rust_primitives.sequence.seq_remove self 0#usize
+    ok (option.Option.Some t, s)
+
 /-! ## Option -/
 
 def option.Option.unwrap_or :=
diff --git a/lean/CoreModels/Core/Types.lean b/lean/CoreModels/Core/Types.lean
index 3740284..e6387de 100644
--- a/lean/CoreModels/Core/Types.lean
+++ b/lean/CoreModels/Core/Types.lean
@@ -25,15 +25,17 @@ namespace CoreModels.core
 @[reducible]
 def array.TryFromSliceError := Unit
 
-/-- [core_models::array::Dummy]
+/-
+/-- [core_models::array::Array]
     Source: 'core-models/src/core/array.rs', lines 8:0-8:40 -/
 @[reducible]
-def array.Dummy (T : Type) (N : Std.Usize) := Array T N
+def array.Array (T : Type) (N : Std.Usize) := Array T N
+-/
 
-/-- [core_models::array::{core_models::array::Dummy<T, N>}::each_ref::closure]
+/-- [core_models::array::{core_models::array::Array<T, N>}::each_ref::closure]
     Source: 'core-models/src/core/array.rs', lines 46:22-46:43 -/
 @[reducible]
-def array.Dummy.each_ref.closure (T : Type) (N : Std.Usize) := Array T N
+def array.Array.each_ref.closure (T : Type) (N : Std.Usize) := Array T N
 
 /-- Trait declaration: [core_models::iter::traits::collect::IntoIterator]
     Source: 'core-models/src/core/iter.rs', lines 386:8-395:9
@@ -43,7 +45,7 @@ structure iter.traits.collect.IntoIterator (Self : Type) (Self_Item : Type)
   into_iter : Self → Result Self_IntoIter
 
 /-- [core_models::array::iter::IntoIter]
-    Source: 'core-models/src/core/array.rs', lines 145:4-145:55
+    Source: 'core-models/src/core/array.rs', lines 158:4-158:55
     Visibility: public -/
 @[reducible]
 def array.iter.IntoIter (T : Type) (N : Std.Usize) :=
@@ -55,31 +57,6 @@ def array.iter.IntoIter (T : Type) (N : Std.Usize) :=
 structure ops.index.Index (Self : Type) (Idx : Type) (Self_Output : Type) where
   index : Self → Idx → Result Self_Output
 
-/-- [core_models::ops::range::Range]
-    Source: 'core-models/src/core/ops.rs', lines 293:4-296:5
-    Visibility: public -/
-structure ops.range.Range (T : Type) where
-  start : T
-  «end» : T
-
-/-- [core_models::ops::range::RangeTo]
-    Source: 'core-models/src/core/ops.rs', lines 285:4-287:5
-    Visibility: public -/
-structure ops.range.RangeTo (T : Type) where
-  «end» : T
-
-/-- [core_models::ops::range::RangeFrom]
-    Source: 'core-models/src/core/ops.rs', lines 289:4-291:5
-    Visibility: public -/
-structure ops.range.RangeFrom (T : Type) where
-  start : T
-
-/-- [core_models::ops::range::RangeFull]
-    Source: 'core-models/src/core/ops.rs', lines 298:4-298:25
-    Visibility: public -/
-@[reducible]
-def ops.range.RangeFull := Unit
-
 /-- Trait declaration: [core_models::clone::Clone]
     Source: 'core-models/src/core/clone.rs', lines 13:0-16:1
     Visibility: public -/
@@ -242,14 +219,14 @@ def fmt.Formatter := Unit
 def fmt.Error := Unit
 
 /-- Trait declaration: [core_models::fmt::Debug]
-    Source: 'core-models/src/core/fmt.rs', lines 19:0-22:1
+    Source: 'core-models/src/core/fmt.rs', lines 25:0-28:1
     Visibility: public -/
 structure fmt.Debug (Self : Type) where
-  dbg_fmt : Self → fmt.Formatter → Result ((result.Result Unit fmt.Error)
-    × fmt.Formatter)
+  fmt : Self → fmt.Formatter → Result ((result.Result Unit fmt.Error) ×
+    fmt.Formatter)
 
 /-- Trait declaration: [core_models::fmt::Display]
-    Source: 'core-models/src/core/fmt.rs', lines 13:0-16:1
+    Source: 'core-models/src/core/fmt.rs', lines 19:0-22:1
     Visibility: public -/
 structure fmt.Display (Self : Type) where
   fmt : Self → fmt.Formatter → Result ((result.Result Unit fmt.Error) ×
@@ -268,25 +245,25 @@ structure error.Error (Self : Type) where
 def f32.f32 := Unit
 
 /-- [core_models::fmt::Arguments]
-    Source: 'core-models/src/core/fmt.rs', lines 25:0-25:33
+    Source: 'core-models/src/core/fmt.rs', lines 31:0-31:33
     Visibility: public -/
 @[reducible]
 def fmt.Arguments := Unit
 
 /-- [core_models::fmt::rt::ArgumentType]
-    Source: 'core-models/src/core/fmt.rs', lines 52:4-59:5 -/
+    Source: 'core-models/src/core/fmt.rs', lines 58:4-65:5 -/
 @[discriminant isize]
 inductive fmt.rt.ArgumentType where
 | Placeholder : core.marker.PhantomData Unit → fmt.rt.ArgumentType
 
 /-- [core_models::fmt::rt::Argument]
-    Source: 'core-models/src/core/fmt.rs', lines 61:4-63:5
+    Source: 'core-models/src/core/fmt.rs', lines 67:4-69:5
     Visibility: public -/
 structure fmt.rt.Argument where
   ty : fmt.rt.ArgumentType
 
 /-- [core_models::fmt::rt::Count]
-    Source: 'core-models/src/core/fmt.rs', lines 101:4-105:5 -/
+    Source: 'core-models/src/core/fmt.rs', lines 107:4-111:5 -/
 @[discriminant isize]
 inductive fmt.rt.Count where
 | Is : Std.U16 → fmt.rt.Count
@@ -294,7 +271,7 @@ inductive fmt.rt.Count where
 | Implied : fmt.rt.Count
 
 /-- [core_models::fmt::rt::Placeholder]
-    Source: 'core-models/src/core/fmt.rs', lines 107:4-112:5 -/
+    Source: 'core-models/src/core/fmt.rs', lines 113:4-118:5 -/
 structure fmt.rt.Placeholder where
   position : Std.Usize
   flags : Std.U32
@@ -302,7 +279,7 @@ structure fmt.rt.Placeholder where
   width : fmt.rt.Count
 
 /-- [core_models::fmt::rt::UnsafeArg]
-    Source: 'core-models/src/core/fmt.rs', lines 114:4-114:21 -/
+    Source: 'core-models/src/core/fmt.rs', lines 120:4-120:21 -/
 @[reducible]
 def fmt.rt.UnsafeArg := Unit
 
@@ -319,35 +296,35 @@ structure hash.Hash (Self : Type) where
     H
 
 /-- [core_models::iter::adapters::skip::Skip]
-    Source: 'core-models/src/core/iter.rs', lines 697:8-700:9
+    Source: 'core-models/src/core/iter.rs', lines 696:8-699:9
     Visibility: public -/
 structure iter.adapters.skip.Skip (I : Type) where
   iter : I
   n : Std.Usize
 
 /-- [core_models::iter::adapters::chain::Chain]
-    Source: 'core-models/src/core/iter.rs', lines 666:8-669:9
+    Source: 'core-models/src/core/iter.rs', lines 665:8-668:9
     Visibility: public -/
 structure iter.adapters.chain.Chain (A : Type) (B : Type) where
   a : option.Option A
   b : B
 
 /-- [core_models::iter::adapters::filter::Filter]
-    Source: 'core-models/src/core/iter.rs', lines 633:8-636:9
+    Source: 'core-models/src/core/iter.rs', lines 632:8-635:9
     Visibility: public -/
 structure iter.adapters.filter.Filter (I : Type) (P : Type) where
   iter : I
   predicate : P
 
 /-- [core_models::iter::adapters::zip::Zip]
-    Source: 'core-models/src/core/iter.rs', lines 606:8-609:9
+    Source: 'core-models/src/core/iter.rs', lines 605:8-608:9
     Visibility: public -/
 structure iter.adapters.zip.Zip (I1 : Type) (I2 : Type) where
   it1 : I1
   it2 : I2
 
 /-- [core_models::iter::adapters::flatten::Flatten]
-    Source: 'core-models/src/core/iter.rs', lines 562:8-568:9
+    Source: 'core-models/src/core/iter.rs', lines 561:8-567:9
     Visibility: public -/
 structure iter.adapters.flatten.Flatten (I : Type) (Clause0_Item : Type)
   (Clause1_Item : Type) where
@@ -355,7 +332,7 @@ structure iter.adapters.flatten.Flatten (I : Type) (Clause0_Item : Type)
   current : option.Option Clause0_Item
 
 /-- [core_models::iter::adapters::flat_map::FlatMap]
-    Source: 'core-models/src/core/iter.rs', lines 524:8-528:9
+    Source: 'core-models/src/core/iter.rs', lines 523:8-527:9
     Visibility: public -/
 structure iter.adapters.flat_map.FlatMap (I : Type) (U : Type) (F : Type) where
   it : I
@@ -363,14 +340,14 @@ structure iter.adapters.flat_map.FlatMap (I : Type) (U : Type) (F : Type) where
   current : option.Option U
 
 /-- [core_models::iter::adapters::take::Take]
-    Source: 'core-models/src/core/iter.rs', lines 497:8-500:9
+    Source: 'core-models/src/core/iter.rs', lines 496:8-499:9
     Visibility: public -/
 structure iter.adapters.take.Take (I : Type) where
   iter : I
   n : Std.Usize
 
 /-- [core_models::iter::adapters::map::Map]
-    Source: 'core-models/src/core/iter.rs', lines 470:8-473:9
+    Source: 'core-models/src/core/iter.rs', lines 469:8-472:9
     Visibility: public -/
 structure iter.adapters.map.Map (I : Type) (F : Type) where
   iter : I
@@ -458,7 +435,7 @@ structure iter.traits.iterator.IteratorMethods (Self : Type) (Self_Clause0_Item
     iter.traits.collect.FromIterator B Self_Clause0_Item), Self → Result B
 
 /-- Trait declaration: [core_models::iter::range::Step]
-    Source: 'core-models/src/core/iter.rs', lines 732:4-752:5
+    Source: 'core-models/src/core/iter.rs', lines 731:4-751:5
     Visibility: public -/
 structure iter.range.Step (Self : Type) where
   cloneCloneInst : clone.Clone Self
@@ -770,7 +747,8 @@ structure ops.try_trait.FromResidual (Self : Type) (R : Type) where
   from_residual : R → Result Self
 
 /-- Trait declaration: [core_models::ops::try_trait::Try]
-    Source: 'core-models/src/core/ops.rs', lines 252:4-257:5 -/
+    Source: 'core-models/src/core/ops.rs', lines 252:4-257:5
+    Visibility: public -/
 structure ops.try_trait.Try (Self : Type) (Self_Output : Type) (Self_Residual :
   Type) where
   from_output : Self_Output → Result Self
@@ -788,6 +766,31 @@ structure ops.deref.Deref (Self : Type) (Self_Target : Type) where
 structure ops.drop.Drop (Self : Type) where
   drop : Self → Result Self
 
+/-- [core_models::ops::range::RangeTo]
+    Source: 'core-models/src/core/ops.rs', lines 285:4-287:5
+    Visibility: public -/
+structure ops.range.RangeTo (T : Type) where
+  «end» : T
+
+/-- [core_models::ops::range::RangeFrom]
+    Source: 'core-models/src/core/ops.rs', lines 289:4-291:5
+    Visibility: public -/
+structure ops.range.RangeFrom (T : Type) where
+  start : T
+
+/-- [core_models::ops::range::Range]
+    Source: 'core-models/src/core/ops.rs', lines 293:4-296:5
+    Visibility: public -/
+structure ops.range.Range (T : Type) where
+  start : T
+  «end» : T
+
+/-- [core_models::ops::range::RangeFull]
+    Source: 'core-models/src/core/ops.rs', lines 298:4-298:25
+    Visibility: public -/
+@[reducible]
+def ops.range.RangeFull := Unit
+
 /-- [core_models::ops::range::RangeInclusive]
     Source: 'core-models/src/core/ops.rs', lines 300:4-303:5
     Visibility: public -/
@@ -795,10 +798,12 @@ structure ops.range.RangeInclusive (T : Type) where
   start : T
   «end» : T
 
+/-
 /-- [core_models::slice::Slice]
-    Source: 'core-models/src/core/slice.rs', lines 5:0-5:19 -/
+    Source: 'core-models/src/core/slice.rs', lines 5:0-5:21 -/
 @[reducible]
-def slice.Slice (T : Type) := T
+def slice.Slice (T : Type) := Slice T
+-/
 
 /-- [core_models::slice::iter::Chunks]
     Source: 'core-models/src/core/slice.rs', lines 12:4-15:5
@@ -827,6 +832,14 @@ structure slice.iter.Windows (T : Type) where
   size : Std.Usize
   elements : Slice T
 
+/-- Trait declaration: [core_models::slice::index::SliceIndex]
+    Source: 'core-models/src/core/slice.rs', lines 353:4-360:5
+    Visibility: public -/
+structure slice.index.SliceIndex (Self : Type) (T : Type) (Self_Output : Type)
+  where
+  get : Self → T → Result (option.Option Self_Output)
+  index : Self → T → Result Self_Output
+
 /-- [core_models::str::error::Utf8Error]
     Source: 'core-models/src/core/str.rs', lines 10:4-10:25
     Visibility: public -/
diff --git a/lean/CoreModels/Core/TypesPrologue.lean b/lean/CoreModels/Core/TypesPrologue.lean
index 7446461..b5ca5e6 100644
--- a/lean/CoreModels/Core/TypesPrologue.lean
+++ b/lean/CoreModels/Core/TypesPrologue.lean
@@ -19,12 +19,18 @@ structure Fn (Self : Type) (Args : Type) (Self_Clause0_Output : Type) where
   call : Self → Args → Result Self_Clause0_Output
 end ops.function
 
-/-! ## Phantom — used by `Aeneas/Alloc/Types.lean` rewrite
-
-`vec.Vec T A` in core-models is `Seq T × PhantomData<A>`. We can't reuse
-the existing `core.marker.PhantomData T := T` for the alloc rewrite (the
-extracted constructor sites use `()`, which is `Unit`). We instead rewrite
-the `core.marker.PhantomData A` field type to `core.Phantom A`.
+/-! ## PhantomData — replaces Aeneas's reducible alias
+
+Aeneas extracts `core::marker::PhantomData` as the reducible alias
+`def marker.PhantomData (T) := T` and builds phantom values with `()` (Charon
+models it as a ZST). That alias is unusable here: where `PhantomData A` is the
+second component of a pair (e.g. `vec.drain.Drain T A := Seq T × PhantomData A`),
+Lean unfolds it and loses `A` during unification.
+
+So we model it as a *non-reducible* `structure` instead, which keeps `A`
+syntactically present. `patch_lean.py`'s `rewrite_phantom_data` rewires the
+Aeneas output onto this carrier: it comments out the generated alias and
+rewrites the `()` constructor sites to `core.marker.PhantomData.mk`.
 -/
 
 structure marker.PhantomData (A : Type) where mk ::
diff --git a/patch_lean.py b/patch_lean.py
index d7fe1fd..361cac6 100755
--- a/patch_lean.py
+++ b/patch_lean.py
@@ -112,6 +112,10 @@ def rename_alloc_models(text: str) -> str:
     text = text.replace("namespace alloc_models", "namespace CoreModels.alloc")
     text = text.replace("end alloc_models", "end CoreModels.alloc")
     text = text.replace("alloc_models", "alloc")
+    # Aeneas also PascalCases the staged crate name when it synthesises
+    # trait-impl identifiers (e.g. `Alloc_modelsAllocAllocator`), which the
+    # lowercase replace above misses.
+    text = text.replace("Alloc_models", "Alloc")
     return text
 
 
@@ -154,21 +158,6 @@ def rewrite_alloc_imports(text: str) -> str:
     )
     return text
 
-def fix_vec_allocator(text: str) -> str:
-    text = replace_blocks(text, [
-        ("alloc::vec::Vec",
-         "def vec.Vec (T : Type) (A : Type := alloc.Global) :=\n"
-         "  rust_primitives.sequence.Seq T × core.marker.PhantomData A"),
-        ("alloc::vec::drain::Drain",
-         "def vec.drain.Drain (T : Type) (A : Type := alloc.Global) :=\n"
-         "  rust_primitives.sequence.Seq T × core.marker.PhantomData A"),
-        ("alloc::vec::into_iter::IntoIter",
-         "def vec.into_iter.IntoIter (T : Type) (A : Type := alloc.Global) :=\n"
-         "  rust_primitives.sequence.Seq T × core.marker.PhantomData A"),
-    ])
-    
-    return text
-
 def fix_result_match(text: str) -> str:
     """ A match on `result.Result` cannot be parsed properly by Lean in
     `I128.Insts.Core_modelsIterStepStep.steps_between`.
@@ -220,6 +209,134 @@ def rewrite_phantom_data(text: str) -> str:
         trailer="replaced by rewrite_phantom_data in favor of the def in `TypesPrologue.lean`",
     )
 
+
+def rename_iter_param(text: str) -> str:
+    """Aeneas sometimes names a function parameter `iter`, which shadows the
+    `iter` *namespace* (`core_models::iter`). Inside the body, a qualified
+    reference like `iter.adapters.step_by...next_loop.body` then resolves to
+    the local parameter instead of the namespace and fails to elaborate.
+    See https://github.com/AeneasVerif/aeneas/issues/1098.
+
+    For every top-level block whose signature binds a parameter named `iter`,
+    rename that parameter (and its value-level uses) to `iter_`. We leave
+    `iter.<...>` namespace paths, `::iter::` Rust paths (in doc headers), and
+    `iter :=` struct-field names untouched.
+
+    One subtlety: an adapter constructor such as `Skip::new` builds its value
+    with Rust field-shorthand, which Aeneas extracts as `ok { iter, n }`. Here
+    `iter` is simultaneously the struct field *name* and the (binder) value.
+    Blindly renaming it to `{ iter_, n }` would reference a nonexistent field
+    `iter_`, so we first expand the shorthand to `{ iter := iter_, n }` —
+    keeping the field name `iter` while pointing it at the renamed binder.
+    """
+    # A standalone `iter` identifier (binder or value), i.e. NOT:
+    #   - part of a `::iter::` Rust path or `.iter` projection (lookbehind),
+    #   - the prefix of `iter1` or a namespace path `iter.foo` (lookahead),
+    #   - the struct-field name in `iter := ...` (negative lookahead for `:=`).
+    token = re.compile(r"(?<![\w.:])iter(?![\w.])(?!\s*:=)")
+    # `iter` as the leading field of a record literal `{ iter, ... }` / `{ iter }`
+    # (but not the already-explicit `{ iter := ... }`).
+    shorthand = re.compile(r"(\{\s*)iter\b(?!\s*:=)")
+
+    def fn(ident: str, block_lines: list[str]) -> str | None:
+        block = "\n".join(block_lines)
+        # Only act on blocks that actually bind an `iter` parameter.
+        if not re.search(r"\(\s*iter\s*:(?!=)", block):
+            return None
+        # Expand field-shorthand before the generic rename so the field name
+        # survives (the inserted `iter := iter_` is then left alone: `iter` is
+        # guarded by the `:=` lookahead, `iter_` by the trailing-`_` lookahead).
+        block = shorthand.sub(r"\1iter := iter_", block)
+        return token.sub("iter_", block)
+
+    return transform_blocks(text, fn)
+
+
+def drop_intoiterator_iterator_inst(text: str) -> str:
+    """Strip the `iteratorIteratorInst := ...` field from `IntoIterator` impl
+    records.
+
+    Aeneas extracts the alloc crate against the *real* `core`'s
+    `IntoIterator` trait, whose Lean shape carries an `iteratorIteratorInst`
+    field (the materialised `IntoIter: Iterator` super-bound). Our
+    replacement `core_models` `IntoIterator` (in `CoreModels.Core`) has no
+    such field — the core-side impls (e.g. arrays) never set it. So the
+    `iteratorIteratorInst := ...` assignment Aeneas emits in every alloc
+    `IntoIterator` impl record refers to a nonexistent field and breaks
+    elaboration; we drop it, leaving just the `into_iter := ...` field.
+
+    Only `IntoIterator` trait-implementation blocks are touched. Within such
+    a block we delete the `iteratorIteratorInst :=` line and any (more
+    deeply indented) continuation lines of its value, up to the next field
+    assignment (`<name> :=`) or the closing `}`.
+    """
+    def fn(ident: str, block_lines: list[str]) -> str | None:
+        if "iter::traits::collect::IntoIterator" not in ident:
+            return None
+        out: list[str] = []
+        i, n, dropped = 0, len(block_lines), False
+        while i < n:
+            if block_lines[i].lstrip().startswith("iteratorIteratorInst :="):
+                i += 1  # skip the field line itself
+                # Skip its value continuation lines until the next field /  `}`.
+                while i < n:
+                    nxt = block_lines[i].strip()
+                    if nxt == "}" or re.match(r"\w+ :=", nxt):
+                        break
+                    i += 1
+                dropped = True
+                continue
+            out.append(block_lines[i])
+            i += 1
+        return "\n".join(out) if dropped else None
+
+    return transform_blocks(text, fn)
+
+
+# Standalone `Result` / `ok` tokens, i.e. NOT already part of a dotted path
+# such as `result.Result`, `Aeneas.Std.Result`, or `result.Result.ok`.
+_BARE_RESULT_RE = re.compile(r"(?<![\w.])Result\b")
+_BARE_OK_RE = re.compile(r"(?<![\w.])ok\b")
+
+
+def qualify_result_monad_impls(text: str) -> str:
+    """Fully qualify the Aeneas error monad inside any trait impl whose `Self`
+    is `Result<_, _>` (e.g. the `Try` impl's `from_output` / `«branch»`, and
+    the `FromIterator<Result<_, _>>` impl's `from_iter`).
+
+    Those defs are emitted into the `result.Result.*` namespace. Inside that
+    namespace the bare names `Result` and `ok` resolve to *our* `result.Result`
+    inductive (from `TypesPrologue.lean`) and `result.Result.ok` projection,
+    not to Aeneas's `Aeneas.Std.Result` / `Aeneas.Std.Result.ok`, so the
+    generated bodies fail to elaborate with `type expected, got Result ...`.
+
+    `TypesPrologue.lean` dodges the exact same clash by hand by spelling out
+    `Aeneas.Std.Result`. We apply that convention here: in every block of an
+    impl `for ... result::Result`, rewrite each *standalone* `Result` ->
+    `Aeneas.Std.Result` and `ok` -> `Aeneas.Std.Result.ok` (dotted paths like
+    `result.Result.Ok` are left untouched). The doc-comment header is
+    preserved verbatim. The match keys on the un-renamed Rust path in the doc
+    header (`core_models` survives `rename_namespace`, which only rewrites
+    `namespace`/`end` lines and `Core_models`).
+    """
+    def fn(ident: str, block_lines: list[str]) -> str | None:
+        if "for core_models::result::Result" not in ident:
+            return None
+        # Preserve the `/-- ... -/` doc comment; only rewrite the code below it.
+        doc_end = 0
+        while doc_end < len(block_lines) and \
+                not block_lines[doc_end].rstrip().endswith("-/"):
+            doc_end += 1
+        doc_end += 1
+        head = block_lines[:doc_end]
+        body = "\n".join(block_lines[doc_end:])
+        body = _BARE_RESULT_RE.sub("Aeneas.Std.Result", body)
+        body = _BARE_OK_RE.sub("Aeneas.Std.Result.ok", body)
+        return "\n".join(head) + ("\n" + body if body else "")
+
+    return transform_blocks(text, fn)
+
+
 def desugar_pure_num_bound_binds(text: str) -> str:
     """The generated `Funs.lean` uses monadic bind syntax to fetch numeric
     bounds:
@@ -254,7 +371,9 @@ def comment_out_num_bounds(text: str) -> str:
 
 def comment_out_types(text: str) -> str:
     """
-    Some type declarations in Types.lean are commented out (provided by TypesPrologue.lean).
+    Some type declarations in Types.lean are commented out: most are provided
+    by TypesPrologue.lean, while `array::Array` / `slice::Slice` are redundant
+    aliases for the Aeneas builtins `Array T N` / `Slice T` (see below).
     """
     return comment_out_blocks(text, [
         "core_models::ops::function::FnOnce",
@@ -263,6 +382,19 @@ def comment_out_types(text: str) -> str:
         "core_models::cmp::Ordering",
         "core_models::option::Option",
         "core_models::result::Result",
+        # `array.Array` is just an alias for Aeneas's builtin `Array T N`, so
+        # the generated `def` is redundant and only shadows the builtin.
+        #
+        # `slice.Slice` is the dummy `struct Slice<T>([T])` we declare in Rust
+        # only to hang the `Slice::*` impls off of; Aeneas translates it to a
+        # `def slice.Slice`, but every actual slice *type* reference in the
+        # generated Lean uses the bare `Slice T` (the opened Aeneas builtin) —
+        # i.e. exactly what `[T]` translates to — and the `slice.Slice.*`
+        # methods only need `slice.Slice` as a name prefix, not as a type. So
+        # we drop the dummy def and let `Slice T` resolve to the builtin, just
+        # like `array.Array`.
+        "core_models::array::Array",
+        "core_models::slice::Slice",
     ])
 
 def add_funs_prologue_import(text: str) -> str:
@@ -348,8 +480,8 @@ def _find_block_end(lines: list[str], i: int, n: int) -> tuple[int, int]:
 
 
 def _ident_matches(ident: str, sub: str) -> bool:
-    """Substring match modes used by both `comment_out_blocks` and
-    `replace_blocks`:
+    """Substring match modes used by `comment_out_blocks` and
+    `relocate_blocks_to_end`:
 
       * `"foo::"`  — prefix match (entry ends with `::`)
       * exact equality
@@ -430,31 +562,45 @@ def fn(ident: str, block_lines: list[str]) -> str | None:
     return transform_blocks(text, fn)
 
 
-def replace_blocks(text: str, replacements: list[tuple[str, str]]) -> str:
-    """Replace the def body of each top-level doc-headed block whose
-    identifier contains a matching substring.
-
-    `replacements` is a list of `(substring, replacement_text)` pairs;
-    matching uses the same modes as `comment_out_blocks`. First match wins,
-    so order entries from most-specific to least-specific if any could
-    overlap. The original `/-- ... -/` doc-comment header is preserved;
-    only the attributes / def / body that follow it are swapped for
-    `replacement_text`.
+def relocate_blocks_to_end(
+    text: str,
+    name_substrings: list[str],
+    *,
+    end_marker: str,
+) -> str:
+    """Move every top-level doc-headed block whose identifier matches one of
+    `name_substrings` to the end of the namespace — just before the line
+    `end_marker` — preserving their relative order.
+
+    Aeneas orders definitions from its *generic* call graph, which does not
+    see the *monomorphised* dependency a `StepBy<Range<usize>>` iterator has
+    on the concrete `Usize` `Step` instance. That instance is a computable
+    `def` emitted late in `Funs.lean` (interleaved with the `num.*` defs it
+    relies on), so the adapter lands *before* it and elaboration fails with
+    `unknown identifier core.Usize.Insts.CoreIterRangeStep`. Hoisting the
+    adapter past the instance fixes the order; nothing else in the file
+    references the adapter's `Iterator` impl, so no new forward reference is
+    introduced. The later (already-correct) users — e.g. the slice compare
+    loops — are untouched because they sit after the instance already.
     """
+    captured: list[str] = []
+
     def fn(ident: str, block_lines: list[str]) -> str | None:
-        for sub, repl in replacements:
-            if _ident_matches(ident, sub):
-                # Preserve the doc-comment lines (up to and including the
-                # one ending in `-/`); replace everything after.
-                doc_end = 0
-                while doc_end < len(block_lines) and \
-                        not block_lines[doc_end].rstrip().endswith("-/"):
-                    doc_end += 1
-                doc_end += 1
-                return "\n".join(block_lines[:doc_end]) + "\n" + repl
+        if any(_ident_matches(ident, s) for s in name_substrings):
+            captured.append("\n".join(block_lines))
+            return ""
         return None
 
-    return transform_blocks(text, fn)
+    body = transform_blocks(text, fn)
+    if not captured:
+        return body
+
+    needle = "\n" + end_marker
+    idx = body.rfind(needle)
+    block_text = "\n\n".join(captured)
+    if idx == -1:
+        return body.rstrip() + "\n\n" + block_text + "\n"
+    return body[:idx] + "\n\n" + block_text + "\n" + body[idx:]
 
 
 # ---------------------------------------------------------------------------
@@ -486,6 +632,16 @@ def main() -> int:
             text = comment_out_num_bounds(text)
             text = desugar_pure_num_bound_binds(text)
             text = fix_result_match(text)
+            text = rename_iter_param(text)
+            text = qualify_result_monad_impls(text)
+            # The `StepBy` iterator monomorphises onto the concrete `Usize`
+            # `Step` instance, which Aeneas emits *later* in the file. Hoist
+            # the adapter past it so the reference resolves.
+            text = relocate_blocks_to_end(
+                text,
+                ["iter::adapters::step_by::{impl core_models::iter::traits::iterator::Iterator"],
+                end_marker="end CoreModels.core",
+            )
         if path == types_path:
             text = comment_out_types(text)
         write(path, text)
@@ -532,7 +688,9 @@ def patch_alloc() -> None:
         text = rewrite_alloc_imports(text)
         text = fix_fail_panic(text)
         text = rewrite_phantom_data(text)
-        text = fix_vec_allocator(text)
+        if path == funs:
+            text = rename_iter_param(text)
+            text = drop_intoiterator_iterator_inst(text)
         write(path, text)
     print(f"patched {ALLOC_DIR}.")
 
diff --git a/tests/rust_lean_equiv_test/source/src/alloc/vec.rs b/tests/rust_lean_equiv_test/source/src/alloc/vec.rs
index 615190d..8a9843e 100644
--- a/tests/rust_lean_equiv_test/source/src/alloc/vec.rs
+++ b/tests/rust_lean_equiv_test/source/src/alloc/vec.rs
@@ -314,3 +314,70 @@ pub fn test_vec_swap_remove_back() -> bool {
 // once Vec tests can compile in the first place.
 // TODO(vec-iter-extraction): Vec::iter / Vec::into_iter use iterator traits
 // whose Lean models we don't have yet.
+
+#[rust_lean_test]
+pub fn test_vec_new_len_zero() -> bool {
+    let v: Vec<u8> = Vec::new();
+    v.len() == 0
+}
+
+#[rust_lean_test]
+pub fn test_vec_push_len() -> bool {
+    let mut v: Vec<u8> = Vec::new();
+    v.push(7u8);
+    v.len() == 1
+}
+
+#[rust_lean_test]
+pub fn test_vec_push_pop() -> bool {
+    let mut v: Vec<u8> = Vec::new();
+    v.push(9u8);
+    match v.pop() {
+        Some(x) => x == 9u8,
+        None => false,
+    }
+}
+
+// ----- PartialEq / Clone / IntoIterator on Vec (branch additions) ------------
+// These exercise the extracted `eq_loop` / `clone_loop` / `IntoIter::next`.
+
+#[rust_lean_test]
+pub fn test_vec_eq_same() -> bool {
+    let mut a: Vec<u8> = Vec::new();
+    a.push(1u8);
+    a.push(2u8);
+    let mut b: Vec<u8> = Vec::new();
+    b.push(1u8);
+    b.push(2u8);
+    (a == b) == true
+}
+
+#[rust_lean_test]
+pub fn test_vec_eq_diff() -> bool {
+    let mut a: Vec<u8> = Vec::new();
+    a.push(1u8);
+    let mut b: Vec<u8> = Vec::new();
+    b.push(2u8);
+    (a == b) == false
+}
+
+#[rust_lean_test]
+pub fn test_vec_clone_preserves() -> bool {
+    let mut a: Vec<u8> = Vec::new();
+    a.push(3u8);
+    a.push(4u8);
+    let b = a.clone();
+    (a == b) == true
+}
+
+#[rust_lean_test]
+pub fn test_vec_into_iter_first() -> bool {
+    let mut v: Vec<u8> = Vec::new();
+    v.push(7u8);
+    v.push(8u8);
+    let mut it = v.into_iter();
+    match it.next() {
+        Some(x) => x == 7u8,
+        None => false,
+    }
+}
diff --git a/tests/rust_lean_equiv_test/source/src/core/cmp.rs b/tests/rust_lean_equiv_test/source/src/core/cmp.rs
index fcdf5c8..e1ff596 100644
--- a/tests/rust_lean_equiv_test/source/src/core/cmp.rs
+++ b/tests/rust_lean_equiv_test/source/src/core/cmp.rs
@@ -106,3 +106,31 @@ pub fn test_int_ge_false() -> bool {
 // option type (fine, helpers exist) AND the Ordering variant. We test the
 // downstream `is_lt` / `is_eq` / `is_gt` predicates above instead; matching
 // on `Option<Ordering>` directly needs more care to keep types pinned.
+
+// ----- u8: Ord::cmp ----------------------------------------------------------
+// Directly exercises the scalar `Ord` instance (`U8.Insts.CoreCmpOrd`)
+// re-provided in `FunsPrologue`.
+
+#[rust_lean_test]
+pub fn test_u8_cmp_less() -> bool {
+    match 3u8.cmp(&7u8) {
+        std::cmp::Ordering::Less => true,
+        _ => false,
+    }
+}
+
+#[rust_lean_test]
+pub fn test_u8_cmp_greater() -> bool {
+    match 9u8.cmp(&2u8) {
+        std::cmp::Ordering::Greater => true,
+        _ => false,
+    }
+}
+
+#[rust_lean_test]
+pub fn test_u8_cmp_equal() -> bool {
+    match 5u8.cmp(&5u8) {
+        std::cmp::Ordering::Equal => true,
+        _ => false,
+    }
+}
diff --git a/tests/rust_lean_equiv_test/source/src/core/option.rs b/tests/rust_lean_equiv_test/source/src/core/option.rs
index 2bfa7b7..850805c 100644
--- a/tests/rust_lean_equiv_test/source/src/core/option.rs
+++ b/tests/rust_lean_equiv_test/source/src/core/option.rs
@@ -691,3 +691,30 @@ pub fn test_manual_take_some_bool() -> bool {
     old == Some(true) && x.is_none()
 }
 */
+
+// ----- PartialEq: `Option<T> == Option<T>` -----------------------------------
+
+#[rust_lean_test]
+pub fn test_option_eq_some_same() -> bool {
+    (Some(5u8) == Some(5u8)) == true
+}
+
+#[rust_lean_test]
+pub fn test_option_eq_some_diff() -> bool {
+    (Some(5u8) == Some(6u8)) == false
+}
+
+#[rust_lean_test]
+pub fn test_option_eq_none_none() -> bool {
+    (none_u8() == none_u8()) == true
+}
+
+#[rust_lean_test]
+pub fn test_option_eq_some_none() -> bool {
+    (Some(5u8) == none_u8()) == false
+}
+
+#[rust_lean_test]
+pub fn test_option_eq_none_some() -> bool {
+    (none_u8() == Some(5u8)) == false
+}
diff --git a/tests/rust_lean_equiv_test/source/src/core/slice.rs b/tests/rust_lean_equiv_test/source/src/core/slice.rs
index d45122f..b2d822f 100644
--- a/tests/rust_lean_equiv_test/source/src/core/slice.rs
+++ b/tests/rust_lean_equiv_test/source/src/core/slice.rs
@@ -681,3 +681,80 @@ pub fn test_slice_index_range_full_len() -> bool {
     t.len() == 8
 }
 */
+
+// ----- PartialEq / Ord on slices (branch additions) --------------------------
+
+#[rust_lean_test]
+pub fn test_slice_eq_same() -> bool {
+    let a: &[u8] = &[1u8, 2, 3];
+    let b: &[u8] = &[1u8, 2, 3];
+    (a == b) == true
+}
+
+#[rust_lean_test]
+pub fn test_slice_eq_diff() -> bool {
+    let a: &[u8] = &[1u8, 2, 3];
+    let b: &[u8] = &[1u8, 2, 4];
+    (a == b) == false
+}
+
+// ----- Ord / PartialOrd on slices (lexicographic) ----------------------------
+// These exercise the extracted `partial_cmp_loop` / `cmp_loop`.
+
+#[rust_lean_test]
+pub fn test_slice_cmp_less_by_elem() -> bool {
+    let a: &[u8] = &[1, 2, 3];
+    let b: &[u8] = &[1, 5, 0];
+    match a.cmp(b) {
+        std::cmp::Ordering::Less => true,
+        _ => false,
+    }
+}
+
+#[rust_lean_test]
+pub fn test_slice_cmp_less_by_len() -> bool {
+    // `[1,2]` is a prefix of `[1,2,3]`, so it is `Less`.
+    let a: &[u8] = &[1, 2];
+    let b: &[u8] = &[1, 2, 3];
+    match a.cmp(b) {
+        std::cmp::Ordering::Less => true,
+        _ => false,
+    }
+}
+
+#[rust_lean_test]
+pub fn test_slice_cmp_greater_by_elem() -> bool {
+    let a: &[u8] = &[2];
+    let b: &[u8] = &[1, 9, 9];
+    match a.cmp(b) {
+        std::cmp::Ordering::Greater => true,
+        _ => false,
+    }
+}
+
+#[rust_lean_test]
+pub fn test_slice_cmp_equal() -> bool {
+    let a: &[u8] = &[4, 5, 6];
+    let b: &[u8] = &[4, 5, 6];
+    match a.cmp(b) {
+        std::cmp::Ordering::Equal => true,
+        _ => false,
+    }
+}
+
+#[rust_lean_test]
+pub fn test_slice_partial_cmp_less() -> bool {
+    let a: &[u8] = &[1, 2];
+    let b: &[u8] = &[1, 3];
+    match a.partial_cmp(b) {
+        Some(std::cmp::Ordering::Less) => true,
+        _ => false,
+    }
+}
+
+#[rust_lean_test]
+pub fn test_slice_eq_diff_len() -> bool {
+    let a: &[u8] = &[1, 2];
+    let b: &[u8] = &[1, 2, 3];
+    (a == b) == false
+}