diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs
index 8316025c..bc6d0cf7 100644
--- a/charon/src/bin/charon-driver/translate/translate_traits.rs
+++ b/charon/src/bin/charon-driver/translate/translate_traits.rs
@@ -265,7 +265,6 @@ impl BodyTransCtx<'_, '_> {
                 hax::FullDefKind::AssocFn { .. } => {
                     match &impl_item.value {
                         Provided { is_override, .. } => {
-                            let fun_id = self.register_fun_decl_id(item_span, item_def_id);
                             let fun_def = self.t_ctx.hax_def(item_def_id)?;
                             let binder_kind = BinderKind::TraitMethod(trait_id, name.clone());
                             let fn_ref = self.translate_binder_for_def(
@@ -273,6 +272,21 @@ impl BodyTransCtx<'_, '_> {
                                 binder_kind,
                                 &fun_def,
                                 |bt_ctx| {
+                                    // If the impl is opaque, we only translate the signature of a
+                                    // method with a default body if it's directly used somewhere
+                                    // else.
+                                    // We insert the `Binder<FunDeclRef>` unconditionally here, and
+                                    // remove the ones that correspond to untranslated functions in
+                                    // the `remove_unused_methods` pass.
+                                    let fun_id = if *is_override
+                                        && !item_meta.opacity.is_transparent()
+                                    {
+                                        bt_ctx
+                                            .register_fun_decl_id_no_enqueue(item_span, item_def_id)
+                                    } else {
+                                        bt_ctx.register_fun_decl_id(item_span, item_def_id)
+                                    };
+
                                     // TODO: there's probably a cleaner way to write this
                                     assert_eq!(bt_ctx.binding_levels.len(), 2);
                                     let fun_generics = bt_ctx
diff --git a/charon/src/transform/remove_unused_methods.rs b/charon/src/transform/remove_unused_methods.rs
index aed95e15..e55c82ba 100644
--- a/charon/src/transform/remove_unused_methods.rs
+++ b/charon/src/transform/remove_unused_methods.rs
@@ -1,4 +1,4 @@
-//! Remove the trait methods that were not translated.
+//! Remove the trait/impl methods that were not translated.
 use crate::ast::*;
 
 use super::{ctx::TransformPass, TransformCtx};
@@ -13,9 +13,12 @@ impl TransformPass for Transform {
                 .is_some()
         };
         // Keep only the methods for which we translated the corresponding `FunDecl`. We ensured
-        // that this would be translated if the method is used or implemented.
+        // that this would be translated if the method is used or transparently implemented.
         for tdecl in ctx.translated.trait_decls.iter_mut() {
             tdecl.provided_methods.retain(method_is_translated);
         }
+        for timpl in ctx.translated.trait_impls.iter_mut() {
+            timpl.provided_methods.retain(method_is_translated);
+        }
     }
 }
diff --git a/charon/tests/ui/associated-types.out b/charon/tests/ui/associated-types.out
index 1da92ce8..48bb1530 100644
--- a/charon/tests/ui/associated-types.out
+++ b/charon/tests/ui/associated-types.out
@@ -6,7 +6,6 @@ trait core::clone::Clone<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
     fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
-    fn clone_from<'_0, '_1> = core::clone::Clone::clone_from<'_0_0, '_0_1, Self>
 }
 
 trait core::marker::Copy<Self>
@@ -51,11 +50,6 @@ where
     [@TraitClause0]: core::marker::Sized<T>,
     [@TraitClause1]: core::clone::Clone<T>,
 
-fn core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5::clone_from<'_0, '_1, T>(@1: &'_0 mut (core::option::Option<T>[@TraitClause0]), @2: &'_1 (core::option::Option<T>[@TraitClause0]))
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::clone::Clone<T>,
-
 impl<T> core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5<T> : core::clone::Clone<core::option::Option<T>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<T>,
@@ -63,7 +57,6 @@ where
 {
     parent_clause0 = core::marker::Sized<core::option::Option<T>[@TraitClause0]>
     fn clone<'_0> = core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5::clone<'_0_0, T>[@TraitClause0, @TraitClause1]
-    fn clone_from<'_0, '_1> = core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5::clone_from<'_0_0, '_0_1, T>[@TraitClause0, @TraitClause1]
 }
 
 fn test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}::use_item_required<'a, T>(@1: core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>]) -> core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>]
@@ -310,8 +303,6 @@ where
 
 fn test_crate::Foo::use_item_required<'a, Self, Self_Item>(@1: Self_Item) -> Self_Item
 
-fn core::clone::Clone::clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self))
-
 fn alloc::borrow::ToOwned::to_owned<'_0, Self, Self_Owned>(@1: &'_0 (Self)) -> Self_Owned
 
 fn core::borrow::Borrow::borrow<'_0, Self, Borrowed>(@1: &'_0 (Self)) -> &'_0 (Borrowed)
diff --git a/charon/tests/ui/call-to-known-trait-method.out b/charon/tests/ui/call-to-known-trait-method.out
index 27cd1695..4c8dc082 100644
--- a/charon/tests/ui/call-to-known-trait-method.out
+++ b/charon/tests/ui/call-to-known-trait-method.out
@@ -58,7 +58,6 @@ trait core::clone::Clone<Self>
 trait core::cmp::PartialEq<Self, Rhs>
 {
     fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>
-    fn ne<'_0, '_1> = core::cmp::PartialEq::ne<'_0_0, '_0_1, Self, Rhs>
 }
 
 fn test_crate::{impl test_crate::Trait<B, (A, B)> for test_crate::Struct<A>[@TraitClause0]}::method<A, B, C>()
@@ -110,12 +109,9 @@ impl core::clone::impls::{impl core::clone::Clone for u8}#6 : core::clone::Clone
 
 fn core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19::eq<'_0, '_1>(@1: &'_0 (bool), @2: &'_1 (bool)) -> bool
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19::ne<'_0, '_1>(@1: &'_0 (bool), @2: &'_1 (bool)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19 : core::cmp::PartialEq<bool, bool>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<bool> for bool}#19::ne<'_0_0, '_0_1>
 }
 
 fn test_crate::main()
@@ -148,7 +144,5 @@ fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
 
 fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
 
-fn core::cmp::PartialEq::ne<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
 
 
diff --git a/charon/tests/ui/issue-297-cfg.out b/charon/tests/ui/issue-297-cfg.out
index 1a438de5..3940a89a 100644
--- a/charon/tests/ui/issue-297-cfg.out
+++ b/charon/tests/ui/issue-297-cfg.out
@@ -93,22 +93,11 @@ fn core::slice::{Slice<T>}::chunks<'_0, T>(@1: &'_0 (Slice<T>), @2: usize) -> co
 where
     [@TraitClause0]: core::marker::Sized<T>,
 
-trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    const MAY_HAVE_SIDE_EFFECT : bool
-}
-
 trait core::iter::traits::iterator::Iterator<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
     type Item
     fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
-    fn size_hint<'_0> = core::iter::traits::iterator::Iterator::size_hint<'_0_0, Self>
-    fn count<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::count<Self>[@TraitClause0_0]
-    fn last<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::last<Self>[@TraitClause0_0]
-    fn nth<'_0> = core::iter::traits::iterator::Iterator::nth<'_0_0, Self>
-    fn __iterator_get_unchecked<'_0, [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>> = core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0_0, Self>[@TraitClause0_0]
 }
 
 fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<I>(@1: I) -> I
@@ -120,26 +109,6 @@ fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::sli
 where
     [@TraitClause0]: core::marker::Sized<T>,
 
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::Chunks<'a, T>[@TraitClause0])) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::count<'a, T>(@1: core::slice::iter::Chunks<'a, T>[@TraitClause0]) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::last<'a, T>(@1: core::slice::iter::Chunks<'a, T>[@TraitClause0]) -> core::option::Option<&'_ (Slice<T>)>[core::marker::Sized<&'_ (Slice<T>)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option<&'_ (Slice<T>)>[core::marker::Sized<&'_ (Slice<T>)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> &'_ (Slice<T>)
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
 impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71<'a, T> : core::iter::traits::iterator::Iterator<core::slice::iter::Chunks<'a, T>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<T>,
@@ -147,11 +116,6 @@ where
     parent_clause0 = core::marker::Sized<&'_ (Slice<T>)>
     type Item = &'a (Slice<T>)
     fn next<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::next<'a, '_0_0, T>[@TraitClause0]
-    fn size_hint<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::size_hint<'a, '_0_0, T>[@TraitClause0]
-    fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::count<'a, T>[@TraitClause0]
-    fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::last<'a, T>[@TraitClause0]
-    fn nth<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::nth<'a, '_0_0, T>[@TraitClause0]
-    fn __iterator_get_unchecked<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0]
 }
 
 fn test_crate::f2<'_0, '_1>(@1: &'_0 (Slice<u8>), @2: &'_1 mut (Slice<i16>)) -> usize
@@ -411,18 +375,6 @@ where
 
 fn core::iter::traits::iterator::Iterator::next<'_0, Self>(@1: &'_0 mut (Self)) -> core::option::Option<Self::Item>[Self::parent_clause0]
 
-fn core::iter::traits::iterator::Iterator::size_hint<'_0, Self>(@1: &'_0 (Self)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-
-fn core::iter::traits::iterator::Iterator::count<Self>(@1: Self) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::last<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::nth<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::option::Option<Self::Item>[Self::parent_clause0]
-
 trait core::clone::Clone<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
@@ -563,9 +515,11 @@ trait core::iter::traits::accum::Product<Self, A>
     fn product<I, [@TraitClause0]: core::marker::Sized<I>, [@TraitClause1]: core::iter::traits::iterator::Iterator<I>, @TraitClause1_1::Item = A> = core::iter::traits::accum::Product::product<Self, A, I>[@TraitClause0_0, @TraitClause0_1]
 }
 
-unsafe fn core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> Self::Item
-where
-    [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>,
+trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    const MAY_HAVE_SIDE_EFFECT : bool
+}
 
 fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
 
diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out
index ed90702c..1cac871f 100644
--- a/charon/tests/ui/issue-45-misc.out
+++ b/charon/tests/ui/issue-45-misc.out
@@ -79,92 +79,27 @@ enum core::option::Option<T>
 |  Some(T)
 
 
-enum core::result::Result<T, E>
-  where
-      [@TraitClause0]: core::marker::Sized<T>,
-      [@TraitClause1]: core::marker::Sized<E>,
- =
-|  Ok(T)
-|  Err(E)
-
-
-trait core::clone::Clone<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
-}
-
-trait core::marker::Copy<Self>
+trait core::iter::traits::iterator::Iterator<Self>
 {
-    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
+    type Item
+    fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
 }
 
-trait core::num::nonzero::private::Sealed<Self>
+fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<I>(@1: I) -> I
+where
+    [@TraitClause0]: core::marker::Sized<I>,
+    [@TraitClause1]: core::iter::traits::iterator::Iterator<I>,
 
-trait core::num::nonzero::ZeroablePrimitive<Self>
+trait core::clone::Clone<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    parent_clause1 : [@TraitClause1]: core::marker::Copy<Self>
-    parent_clause2 : [@TraitClause2]: core::num::nonzero::private::Sealed<Self>
-    parent_clause3 : [@TraitClause3]: core::marker::Sized<Self::NonZeroInner>
-    parent_clause4 : [@TraitClause4]: core::marker::Copy<Self::NonZeroInner>
-    type NonZeroInner
-}
-
-opaque type core::num::nonzero::NonZero<T>
-  where
-      [@TraitClause0]: core::marker::Sized<T>,
-      [@TraitClause1]: core::num::nonzero::ZeroablePrimitive<T>,
-
-fn core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0>(@1: &'_0 (usize)) -> usize
-
-impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Clone<usize>
-{
-    parent_clause0 = core::marker::Sized<usize>
-    fn clone<'_0> = core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0_0>
-}
-
-impl core::marker::{impl core::marker::Copy for usize}#37 : core::marker::Copy<usize>
-{
-    parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize}#5
-}
-
-impl core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25 : core::num::nonzero::private::Sealed<usize>
-
-opaque type core::num::nonzero::private::NonZeroUsizeInner
-
-fn core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26::clone<'_0>(@1: &'_0 (core::num::nonzero::private::NonZeroUsizeInner)) -> core::num::nonzero::private::NonZeroUsizeInner
-
-impl core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26 : core::clone::Clone<core::num::nonzero::private::NonZeroUsizeInner>
-{
-    parent_clause0 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
-    fn clone<'_0> = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26::clone<'_0_0>
-}
-
-impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27 : core::marker::Copy<core::num::nonzero::private::NonZeroUsizeInner>
-{
-    parent_clause0 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26
-}
-
-impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26 : core::num::nonzero::ZeroablePrimitive<usize>
-{
-    parent_clause0 = core::marker::Sized<usize>
-    parent_clause1 = core::marker::{impl core::marker::Copy for usize}#37
-    parent_clause2 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25
-    parent_clause3 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
-    parent_clause4 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
-    type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner
+    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
 }
 
 trait core::cmp::PartialEq<Self, Rhs>
 {
     fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>
-    fn ne<'_0, '_1> = core::cmp::PartialEq::ne<'_0_0, '_0_1, Self, Rhs>
-}
-
-trait core::cmp::Eq<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Self>
 }
 
 enum core::cmp::Ordering =
@@ -177,46 +112,8 @@ trait core::cmp::PartialOrd<Self, Rhs>
 {
     parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Rhs>
     fn partial_cmp<'_0, '_1> = core::cmp::PartialOrd::partial_cmp<'_0_0, '_0_1, Self, Rhs>
-    fn lt<'_0, '_1> = core::cmp::PartialOrd::lt<'_0_0, '_0_1, Self, Rhs>
-    fn le<'_0, '_1> = core::cmp::PartialOrd::le<'_0_0, '_0_1, Self, Rhs>
-    fn gt<'_0, '_1> = core::cmp::PartialOrd::gt<'_0_0, '_0_1, Self, Rhs>
-    fn ge<'_0, '_1> = core::cmp::PartialOrd::ge<'_0_0, '_0_1, Self, Rhs>
 }
 
-trait core::cmp::Ord<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::cmp::Eq<Self>
-    parent_clause1 : [@TraitClause1]: core::cmp::PartialOrd<Self, Self>
-    fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>
-}
-
-trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    const MAY_HAVE_SIDE_EFFECT : bool
-}
-
-trait core::iter::traits::iterator::Iterator<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
-    type Item
-    fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
-    fn size_hint<'_0> = core::iter::traits::iterator::Iterator::size_hint<'_0_0, Self>
-    fn count<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::count<Self>[@TraitClause0_0]
-    fn last<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::last<Self>[@TraitClause0_0]
-    fn advance_by<'_0> = core::iter::traits::iterator::Iterator::advance_by<'_0_0, Self>
-    fn nth<'_0> = core::iter::traits::iterator::Iterator::nth<'_0_0, Self>
-    fn max<[@TraitClause0]: core::marker::Sized<Self>, [@TraitClause1]: core::cmp::Ord<Self::Item>> = core::iter::traits::iterator::Iterator::max<Self>[@TraitClause0_0, @TraitClause0_1]
-    fn min<[@TraitClause0]: core::marker::Sized<Self>, [@TraitClause1]: core::cmp::Ord<Self::Item>> = core::iter::traits::iterator::Iterator::min<Self>[@TraitClause0_0, @TraitClause0_1]
-    fn is_sorted<[@TraitClause0]: core::marker::Sized<Self>, [@TraitClause1]: core::cmp::PartialOrd<Self::Item, Self::Item>> = core::iter::traits::iterator::Iterator::is_sorted<Self>[@TraitClause0_0, @TraitClause0_1]
-    fn __iterator_get_unchecked<'_0, [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>> = core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0_0, Self>[@TraitClause0_0]
-}
-
-fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<I>(@1: I) -> I
-where
-    [@TraitClause0]: core::marker::Sized<I>,
-    [@TraitClause1]: core::iter::traits::iterator::Iterator<I>,
-
 trait core::iter::range::Step<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
@@ -225,10 +122,6 @@ trait core::iter::range::Step<Self>
     fn steps_between<'_0, '_1> = core::iter::range::Step::steps_between<'_0_0, '_0_1, Self>
     fn forward_checked = core::iter::range::Step::forward_checked<Self>
     fn backward_checked = core::iter::range::Step::backward_checked<Self>
-    fn forward = core::iter::range::Step::forward<Self>
-    fn forward_unchecked = core::iter::range::Step::forward_unchecked<Self>
-    fn backward = core::iter::range::Step::backward<Self>
-    fn backward_unchecked = core::iter::range::Step::backward_unchecked<Self>
 }
 
 fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0])) -> core::option::Option<A>[@TraitClause0]
@@ -236,54 +129,6 @@ where
     [@TraitClause0]: core::marker::Sized<A>,
     [@TraitClause1]: core::iter::range::Step<A>,
 
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::size_hint<'_0, A>(@1: &'_0 (core::ops::range::Range<A>[@TraitClause0])) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::count<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::last<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0]), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::nth<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0]), @2: usize) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::max<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-    [@TraitClause2]: core::cmp::Ord<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::min<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-    [@TraitClause2]: core::cmp::Ord<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::is_sorted<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-unsafe fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::__iterator_get_unchecked<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0]), @2: usize) -> A
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-    [@TraitClause2]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<core::ops::range::Range<A>[@TraitClause0]>,
-
 impl<A> core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<A> : core::iter::traits::iterator::Iterator<core::ops::range::Range<A>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<A>,
@@ -292,15 +137,6 @@ where
     parent_clause0 = @TraitClause0
     type Item = A
     fn next<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn size_hint<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::size_hint<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn count = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::count<A>[@TraitClause0, @TraitClause1]
-    fn last = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::last<A>[@TraitClause0, @TraitClause1]
-    fn advance_by<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::advance_by<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn nth<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::nth<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn max<[@TraitClause0]: core::cmp::Ord<A>> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::max<A>[@TraitClause0, @TraitClause1, @TraitClause0_0]
-    fn min<[@TraitClause0]: core::cmp::Ord<A>> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::min<A>[@TraitClause0, @TraitClause1, @TraitClause0_0]
-    fn is_sorted = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::is_sorted<A>[@TraitClause0, @TraitClause1]
-    fn __iterator_get_unchecked<'_0, [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<core::ops::range::Range<A>[@TraitClause0]>> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::__iterator_get_unchecked<'_0_0, A>[@TraitClause0, @TraitClause1, @TraitClause0_0]
 }
 
 fn core::clone::impls::{impl core::clone::Clone for u8}#6::clone<'_0>(@1: &'_0 (u8)) -> u8
@@ -313,32 +149,17 @@ impl core::clone::impls::{impl core::clone::Clone for u8}#6 : core::clone::Clone
 
 fn core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22::eq<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22::ne<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22 : core::cmp::PartialEq<u8, u8>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22::ne<'_0_0, '_0_1>
 }
 
 fn core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::partial_cmp<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> core::option::Option<core::cmp::Ordering>[core::marker::Sized<core::cmp::Ordering>]
 
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::lt<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::le<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::gt<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::ge<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60 : core::cmp::PartialOrd<u8, u8>
 {
     parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq<u8> for u8}#22
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::partial_cmp<'_0_0, '_0_1>
-    fn lt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::lt<'_0_0, '_0_1>
-    fn le<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::le<'_0_0, '_0_1>
-    fn gt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::gt<'_0_0, '_0_1>
-    fn ge<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u8> for u8}#60::ge<'_0_0, '_0_1>
 }
 
 fn core::iter::range::{impl core::iter::range::Step for u8}#35::steps_between<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> core::option::Option<usize>[core::marker::Sized<usize>]
@@ -347,14 +168,6 @@ fn core::iter::range::{impl core::iter::range::Step for u8}#35::forward_checked(
 
 fn core::iter::range::{impl core::iter::range::Step for u8}#35::backward_checked(@1: u8, @2: usize) -> core::option::Option<u8>[core::marker::Sized<u8>]
 
-fn core::iter::range::{impl core::iter::range::Step for u8}#35::forward(@1: u8, @2: usize) -> u8
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for u8}#35::forward_unchecked(@1: u8, @2: usize) -> u8
-
-fn core::iter::range::{impl core::iter::range::Step for u8}#35::backward(@1: u8, @2: usize) -> u8
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for u8}#35::backward_unchecked(@1: u8, @2: usize) -> u8
-
 impl core::iter::range::{impl core::iter::range::Step for u8}#35 : core::iter::range::Step<u8>
 {
     parent_clause0 = core::marker::Sized<u8>
@@ -363,10 +176,6 @@ impl core::iter::range::{impl core::iter::range::Step for u8}#35 : core::iter::r
     fn steps_between<'_0, '_1> = core::iter::range::{impl core::iter::range::Step for u8}#35::steps_between<'_0_0, '_0_1>
     fn forward_checked = core::iter::range::{impl core::iter::range::Step for u8}#35::forward_checked
     fn backward_checked = core::iter::range::{impl core::iter::range::Step for u8}#35::backward_checked
-    fn forward = core::iter::range::{impl core::iter::range::Step for u8}#35::forward
-    fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for u8}#35::forward_unchecked
-    fn backward = core::iter::range::{impl core::iter::range::Step for u8}#35::backward
-    fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for u8}#35::backward_unchecked
 }
 
 fn test_crate::cbd(@1: Array<u8, 33 : usize>)
@@ -580,66 +389,33 @@ fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &
 
 fn core::iter::range::Step::forward_checked<Self>(@1: Self, @2: usize) -> core::option::Option<Self>[Self::parent_clause0]
 
-fn core::iter::range::Step::forward<Self>(@1: Self, @2: usize) -> Self
-
-unsafe fn core::iter::range::Step::forward_unchecked<Self>(@1: Self, @2: usize) -> Self
-
 fn core::iter::range::Step::backward_checked<Self>(@1: Self, @2: usize) -> core::option::Option<Self>[Self::parent_clause0]
 
-fn core::iter::range::Step::backward<Self>(@1: Self, @2: usize) -> Self
-
-unsafe fn core::iter::range::Step::backward_unchecked<Self>(@1: Self, @2: usize) -> Self
-
 fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
 
 fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> core::option::Option<core::cmp::Ordering>[core::marker::Sized<core::cmp::Ordering>]
 
-fn core::cmp::PartialOrd::lt<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::le<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::gt<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::ge<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
 fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
 
-fn core::cmp::PartialEq::ne<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::cmp::Ordering
-
-fn core::iter::traits::iterator::Iterator::size_hint<'_0, Self>(@1: &'_0 (Self)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-
-fn core::iter::traits::iterator::Iterator::count<Self>(@1: Self) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::nth<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::option::Option<Self::Item>[Self::parent_clause0]
-
-fn core::iter::traits::iterator::Iterator::last<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::min<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-    [@TraitClause1]: core::cmp::Ord<Self::Item>,
-
-fn core::iter::traits::iterator::Iterator::max<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-    [@TraitClause1]: core::cmp::Ord<Self::Item>,
+trait core::cmp::Eq<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Self>
+}
 
-fn core::iter::traits::iterator::Iterator::is_sorted<Self>(@1: Self) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-    [@TraitClause1]: core::cmp::PartialOrd<Self::Item, Self::Item>,
+trait core::cmp::Ord<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::cmp::Eq<Self>
+    parent_clause1 : [@TraitClause1]: core::cmp::PartialOrd<Self, Self>
+    fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>
+}
 
-fn core::iter::traits::iterator::Iterator::advance_by<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
+trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    const MAY_HAVE_SIDE_EFFECT : bool
+}
 
-unsafe fn core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> Self::Item
-where
-    [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>,
+fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::cmp::Ordering
 
 trait core::iter::traits::collect::FromIterator<Self, A>
 {
@@ -708,6 +484,11 @@ trait core::iter::traits::exact_size::ExactSizeIterator<Self>
     parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
 }
 
+trait core::marker::Copy<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
+}
+
 trait core::iter::traits::accum::Sum<Self, A>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
diff --git a/charon/tests/ui/issue-70-override-provided-method.3.out b/charon/tests/ui/issue-70-override-provided-method.3.out
index 3ac5f5f9..45748173 100644
--- a/charon/tests/ui/issue-70-override-provided-method.3.out
+++ b/charon/tests/ui/issue-70-override-provided-method.3.out
@@ -6,7 +6,6 @@ trait core::clone::Clone<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
     fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
-    fn clone_from<'_0, '_1> = core::clone::Clone::clone_from<'_0_0, '_0_1, Self>
 }
 
 trait core::cmp::PartialEq<Self, Rhs>
@@ -48,11 +47,6 @@ where
     [@TraitClause0]: core::marker::Sized<T>,
     [@TraitClause1]: core::clone::Clone<T>,
 
-fn core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5::clone_from<'_0, '_1, T>(@1: &'_0 mut (core::option::Option<T>[@TraitClause0]), @2: &'_1 (core::option::Option<T>[@TraitClause0]))
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::clone::Clone<T>,
-
 impl<T> core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5<T> : core::clone::Clone<core::option::Option<T>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<T>,
@@ -60,7 +54,6 @@ where
 {
     parent_clause0 = core::marker::Sized<core::option::Option<T>[@TraitClause0]>
     fn clone<'_0> = core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5::clone<'_0_0, T>[@TraitClause0, @TraitClause1]
-    fn clone_from<'_0, '_1> = core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5::clone_from<'_0_0, '_0_1, T>[@TraitClause0, @TraitClause1]
 }
 
 fn test_crate::{impl test_crate::GenericTrait<core::option::Option<T>[@TraitClause0]> for test_crate::Override<T>[@TraitClause0]}::other_method<T>()
@@ -195,7 +188,5 @@ where
 
 fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
 
-fn core::clone::Clone::clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self))
-
 
 
diff --git a/charon/tests/ui/issue-70-override-provided-method.out b/charon/tests/ui/issue-70-override-provided-method.out
index a42479a7..cd17f329 100644
--- a/charon/tests/ui/issue-70-override-provided-method.out
+++ b/charon/tests/ui/issue-70-override-provided-method.out
@@ -13,7 +13,6 @@ enum core::option::Option<T>
 trait core::cmp::PartialEq<Self, Rhs>
 {
     fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>
-    fn ne<'_0, '_1> = core::cmp::PartialEq::ne<'_0_0, '_0_1, Self, Rhs>
 }
 
 fn core::option::{impl core::cmp::PartialEq<core::option::Option<T>[@TraitClause0]> for core::option::Option<T>[@TraitClause0]}#14::eq<'_0, '_1, T>(@1: &'_0 (core::option::Option<T>[@TraitClause0]), @2: &'_1 (core::option::Option<T>[@TraitClause0])) -> bool
@@ -23,12 +22,9 @@ where
 
 fn core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::eq<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::ne<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30 : core::cmp::PartialEq<i32, i32>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::ne<'_0_0, '_0_1>
 }
 
 fn test_crate::main()
@@ -98,10 +94,6 @@ trait core::cmp::PartialOrd<Self, Rhs>
 {
     parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Rhs>
     fn partial_cmp<'_0, '_1> = core::cmp::PartialOrd::partial_cmp<'_0_0, '_0_1, Self, Rhs>
-    fn lt<'_0, '_1> = core::cmp::PartialOrd::lt<'_0_0, '_0_1, Self, Rhs>
-    fn le<'_0, '_1> = core::cmp::PartialOrd::le<'_0_0, '_0_1, Self, Rhs>
-    fn gt<'_0, '_1> = core::cmp::PartialOrd::gt<'_0_0, '_0_1, Self, Rhs>
-    fn ge<'_0, '_1> = core::cmp::PartialOrd::ge<'_0_0, '_0_1, Self, Rhs>
 }
 
 fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::partial_cmp<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> core::option::Option<core::cmp::Ordering>[core::marker::Sized<core::cmp::Ordering>]
@@ -148,41 +140,16 @@ fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2:
 
 fn core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::eq<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::ne<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24 : core::cmp::PartialEq<u32, u32>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::ne<'_0_0, '_0_1>
 }
 
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::lt<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::le<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::gt<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::ge<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64 : core::cmp::PartialOrd<u32, u32>
 {
     parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::partial_cmp<'_0_0, '_0_1>
-    fn lt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::lt<'_0_0, '_0_1>
-    fn le<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::le<'_0_0, '_0_1>
-    fn gt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::gt<'_0_0, '_0_1>
-    fn ge<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::ge<'_0_0, '_0_1>
 }
 
-fn core::cmp::PartialEq::ne<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::lt<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::le<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::gt<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::ge<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
 
 
diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out
index ea85a092..206ce451 100644
--- a/charon/tests/ui/loops.out
+++ b/charon/tests/ui/loops.out
@@ -787,92 +787,27 @@ enum core::option::Option<T>
 |  Some(T)
 
 
-enum core::result::Result<T, E>
-  where
-      [@TraitClause0]: core::marker::Sized<T>,
-      [@TraitClause1]: core::marker::Sized<E>,
- =
-|  Ok(T)
-|  Err(E)
-
-
-trait core::clone::Clone<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
-}
-
-trait core::marker::Copy<Self>
+trait core::iter::traits::iterator::Iterator<Self>
 {
-    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
+    type Item
+    fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
 }
 
-trait core::num::nonzero::private::Sealed<Self>
+fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<I>(@1: I) -> I
+where
+    [@TraitClause0]: core::marker::Sized<I>,
+    [@TraitClause1]: core::iter::traits::iterator::Iterator<I>,
 
-trait core::num::nonzero::ZeroablePrimitive<Self>
+trait core::clone::Clone<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    parent_clause1 : [@TraitClause1]: core::marker::Copy<Self>
-    parent_clause2 : [@TraitClause2]: core::num::nonzero::private::Sealed<Self>
-    parent_clause3 : [@TraitClause3]: core::marker::Sized<Self::NonZeroInner>
-    parent_clause4 : [@TraitClause4]: core::marker::Copy<Self::NonZeroInner>
-    type NonZeroInner
-}
-
-opaque type core::num::nonzero::NonZero<T>
-  where
-      [@TraitClause0]: core::marker::Sized<T>,
-      [@TraitClause1]: core::num::nonzero::ZeroablePrimitive<T>,
-
-fn core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0>(@1: &'_0 (usize)) -> usize
-
-impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Clone<usize>
-{
-    parent_clause0 = core::marker::Sized<usize>
-    fn clone<'_0> = core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0_0>
-}
-
-impl core::marker::{impl core::marker::Copy for usize}#37 : core::marker::Copy<usize>
-{
-    parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize}#5
-}
-
-impl core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25 : core::num::nonzero::private::Sealed<usize>
-
-opaque type core::num::nonzero::private::NonZeroUsizeInner
-
-fn core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26::clone<'_0>(@1: &'_0 (core::num::nonzero::private::NonZeroUsizeInner)) -> core::num::nonzero::private::NonZeroUsizeInner
-
-impl core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26 : core::clone::Clone<core::num::nonzero::private::NonZeroUsizeInner>
-{
-    parent_clause0 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
-    fn clone<'_0> = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26::clone<'_0_0>
-}
-
-impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27 : core::marker::Copy<core::num::nonzero::private::NonZeroUsizeInner>
-{
-    parent_clause0 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26
-}
-
-impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26 : core::num::nonzero::ZeroablePrimitive<usize>
-{
-    parent_clause0 = core::marker::Sized<usize>
-    parent_clause1 = core::marker::{impl core::marker::Copy for usize}#37
-    parent_clause2 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25
-    parent_clause3 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
-    parent_clause4 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
-    type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner
+    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
 }
 
 trait core::cmp::PartialEq<Self, Rhs>
 {
     fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>
-    fn ne<'_0, '_1> = core::cmp::PartialEq::ne<'_0_0, '_0_1, Self, Rhs>
-}
-
-trait core::cmp::Eq<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Self>
 }
 
 enum core::cmp::Ordering =
@@ -885,46 +820,8 @@ trait core::cmp::PartialOrd<Self, Rhs>
 {
     parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Rhs>
     fn partial_cmp<'_0, '_1> = core::cmp::PartialOrd::partial_cmp<'_0_0, '_0_1, Self, Rhs>
-    fn lt<'_0, '_1> = core::cmp::PartialOrd::lt<'_0_0, '_0_1, Self, Rhs>
-    fn le<'_0, '_1> = core::cmp::PartialOrd::le<'_0_0, '_0_1, Self, Rhs>
-    fn gt<'_0, '_1> = core::cmp::PartialOrd::gt<'_0_0, '_0_1, Self, Rhs>
-    fn ge<'_0, '_1> = core::cmp::PartialOrd::ge<'_0_0, '_0_1, Self, Rhs>
-}
-
-trait core::cmp::Ord<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::cmp::Eq<Self>
-    parent_clause1 : [@TraitClause1]: core::cmp::PartialOrd<Self, Self>
-    fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>
-}
-
-trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    const MAY_HAVE_SIDE_EFFECT : bool
-}
-
-trait core::iter::traits::iterator::Iterator<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
-    type Item
-    fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
-    fn size_hint<'_0> = core::iter::traits::iterator::Iterator::size_hint<'_0_0, Self>
-    fn count<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::count<Self>[@TraitClause0_0]
-    fn last<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::last<Self>[@TraitClause0_0]
-    fn advance_by<'_0> = core::iter::traits::iterator::Iterator::advance_by<'_0_0, Self>
-    fn nth<'_0> = core::iter::traits::iterator::Iterator::nth<'_0_0, Self>
-    fn max<[@TraitClause0]: core::marker::Sized<Self>, [@TraitClause1]: core::cmp::Ord<Self::Item>> = core::iter::traits::iterator::Iterator::max<Self>[@TraitClause0_0, @TraitClause0_1]
-    fn min<[@TraitClause0]: core::marker::Sized<Self>, [@TraitClause1]: core::cmp::Ord<Self::Item>> = core::iter::traits::iterator::Iterator::min<Self>[@TraitClause0_0, @TraitClause0_1]
-    fn is_sorted<[@TraitClause0]: core::marker::Sized<Self>, [@TraitClause1]: core::cmp::PartialOrd<Self::Item, Self::Item>> = core::iter::traits::iterator::Iterator::is_sorted<Self>[@TraitClause0_0, @TraitClause0_1]
-    fn __iterator_get_unchecked<'_0, [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>> = core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0_0, Self>[@TraitClause0_0]
 }
 
-fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<I>(@1: I) -> I
-where
-    [@TraitClause0]: core::marker::Sized<I>,
-    [@TraitClause1]: core::iter::traits::iterator::Iterator<I>,
-
 trait core::iter::range::Step<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
@@ -933,10 +830,6 @@ trait core::iter::range::Step<Self>
     fn steps_between<'_0, '_1> = core::iter::range::Step::steps_between<'_0_0, '_0_1, Self>
     fn forward_checked = core::iter::range::Step::forward_checked<Self>
     fn backward_checked = core::iter::range::Step::backward_checked<Self>
-    fn forward = core::iter::range::Step::forward<Self>
-    fn forward_unchecked = core::iter::range::Step::forward_unchecked<Self>
-    fn backward = core::iter::range::Step::backward<Self>
-    fn backward_unchecked = core::iter::range::Step::backward_unchecked<Self>
 }
 
 fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0])) -> core::option::Option<A>[@TraitClause0]
@@ -944,54 +837,6 @@ where
     [@TraitClause0]: core::marker::Sized<A>,
     [@TraitClause1]: core::iter::range::Step<A>,
 
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::size_hint<'_0, A>(@1: &'_0 (core::ops::range::Range<A>[@TraitClause0])) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::count<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::last<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0]), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::nth<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0]), @2: usize) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::max<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-    [@TraitClause2]: core::cmp::Ord<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::min<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-    [@TraitClause2]: core::cmp::Ord<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::is_sorted<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-unsafe fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::__iterator_get_unchecked<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0]), @2: usize) -> A
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-    [@TraitClause2]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<core::ops::range::Range<A>[@TraitClause0]>,
-
 impl<A> core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<A> : core::iter::traits::iterator::Iterator<core::ops::range::Range<A>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<A>,
@@ -1000,15 +845,6 @@ where
     parent_clause0 = @TraitClause0
     type Item = A
     fn next<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn size_hint<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::size_hint<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn count = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::count<A>[@TraitClause0, @TraitClause1]
-    fn last = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::last<A>[@TraitClause0, @TraitClause1]
-    fn advance_by<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::advance_by<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn nth<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::nth<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn max<[@TraitClause0]: core::cmp::Ord<A>> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::max<A>[@TraitClause0, @TraitClause1, @TraitClause0_0]
-    fn min<[@TraitClause0]: core::cmp::Ord<A>> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::min<A>[@TraitClause0, @TraitClause1, @TraitClause0_0]
-    fn is_sorted = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::is_sorted<A>[@TraitClause0, @TraitClause1]
-    fn __iterator_get_unchecked<'_0, [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<core::ops::range::Range<A>[@TraitClause0]>> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::__iterator_get_unchecked<'_0_0, A>[@TraitClause0, @TraitClause1, @TraitClause0_0]
 }
 
 fn core::clone::impls::{impl core::clone::Clone for i32}#14::clone<'_0>(@1: &'_0 (i32)) -> i32
@@ -1021,32 +857,17 @@ impl core::clone::impls::{impl core::clone::Clone for i32}#14 : core::clone::Clo
 
 fn core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::eq<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::ne<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30 : core::cmp::PartialEq<i32, i32>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::ne<'_0_0, '_0_1>
 }
 
 fn core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::partial_cmp<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option<core::cmp::Ordering>[core::marker::Sized<core::cmp::Ordering>]
 
-fn core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::lt<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::le<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::gt<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::ge<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76 : core::cmp::PartialOrd<i32, i32>
 {
     parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::partial_cmp<'_0_0, '_0_1>
-    fn lt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::lt<'_0_0, '_0_1>
-    fn le<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::le<'_0_0, '_0_1>
-    fn gt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::gt<'_0_0, '_0_1>
-    fn ge<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::ge<'_0_0, '_0_1>
 }
 
 fn core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option<usize>[core::marker::Sized<usize>]
@@ -1055,14 +876,6 @@ fn core::iter::range::{impl core::iter::range::Step for i32}#40::forward_checked
 
 fn core::iter::range::{impl core::iter::range::Step for i32}#40::backward_checked(@1: i32, @2: usize) -> core::option::Option<i32>[core::marker::Sized<i32>]
 
-fn core::iter::range::{impl core::iter::range::Step for i32}#40::forward(@1: i32, @2: usize) -> i32
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for i32}#40::forward_unchecked(@1: i32, @2: usize) -> i32
-
-fn core::iter::range::{impl core::iter::range::Step for i32}#40::backward(@1: i32, @2: usize) -> i32
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for i32}#40::backward_unchecked(@1: i32, @2: usize) -> i32
-
 impl core::iter::range::{impl core::iter::range::Step for i32}#40 : core::iter::range::Step<i32>
 {
     parent_clause0 = core::marker::Sized<i32>
@@ -1071,40 +884,29 @@ impl core::iter::range::{impl core::iter::range::Step for i32}#40 : core::iter::
     fn steps_between<'_0, '_1> = core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0_0, '_0_1>
     fn forward_checked = core::iter::range::{impl core::iter::range::Step for i32}#40::forward_checked
     fn backward_checked = core::iter::range::{impl core::iter::range::Step for i32}#40::backward_checked
-    fn forward = core::iter::range::{impl core::iter::range::Step for i32}#40::forward
-    fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for i32}#40::forward_unchecked
-    fn backward = core::iter::range::{impl core::iter::range::Step for i32}#40::backward
-    fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for i32}#40::backward_unchecked
 }
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21::eq<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
+fn core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0>(@1: &'_0 (usize)) -> usize
+
+impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Clone<usize>
+{
+    parent_clause0 = core::marker::Sized<usize>
+    fn clone<'_0> = core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0_0>
+}
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21::ne<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
+fn core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21::eq<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
 
 impl core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21 : core::cmp::PartialEq<usize, usize>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21::ne<'_0_0, '_0_1>
 }
 
 fn core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::partial_cmp<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option<core::cmp::Ordering>[core::marker::Sized<core::cmp::Ordering>]
 
-fn core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::lt<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::le<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::gt<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::ge<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58 : core::cmp::PartialOrd<usize, usize>
 {
     parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::partial_cmp<'_0_0, '_0_1>
-    fn lt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::lt<'_0_0, '_0_1>
-    fn le<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::le<'_0_0, '_0_1>
-    fn gt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::gt<'_0_0, '_0_1>
-    fn ge<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::ge<'_0_0, '_0_1>
 }
 
 fn core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option<usize>[core::marker::Sized<usize>]
@@ -1113,14 +915,6 @@ fn core::iter::range::{impl core::iter::range::Step for usize}#43::forward_check
 
 fn core::iter::range::{impl core::iter::range::Step for usize}#43::backward_checked(@1: usize, @2: usize) -> core::option::Option<usize>[core::marker::Sized<usize>]
 
-fn core::iter::range::{impl core::iter::range::Step for usize}#43::forward(@1: usize, @2: usize) -> usize
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for usize}#43::forward_unchecked(@1: usize, @2: usize) -> usize
-
-fn core::iter::range::{impl core::iter::range::Step for usize}#43::backward(@1: usize, @2: usize) -> usize
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for usize}#43::backward_unchecked(@1: usize, @2: usize) -> usize
-
 impl core::iter::range::{impl core::iter::range::Step for usize}#43 : core::iter::range::Step<usize>
 {
     parent_clause0 = core::marker::Sized<usize>
@@ -1129,10 +923,6 @@ impl core::iter::range::{impl core::iter::range::Step for usize}#43 : core::iter
     fn steps_between<'_0, '_1> = core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0_0, '_0_1>
     fn forward_checked = core::iter::range::{impl core::iter::range::Step for usize}#43::forward_checked
     fn backward_checked = core::iter::range::{impl core::iter::range::Step for usize}#43::backward_checked
-    fn forward = core::iter::range::{impl core::iter::range::Step for usize}#43::forward
-    fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for usize}#43::forward_unchecked
-    fn backward = core::iter::range::{impl core::iter::range::Step for usize}#43::backward
-    fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for usize}#43::backward_unchecked
 }
 
 fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize
@@ -1301,32 +1091,17 @@ impl core::clone::impls::{impl core::clone::Clone for u32}#8 : core::clone::Clon
 
 fn core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::eq<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::ne<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24 : core::cmp::PartialEq<u32, u32>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::ne<'_0_0, '_0_1>
 }
 
 fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::partial_cmp<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> core::option::Option<core::cmp::Ordering>[core::marker::Sized<core::cmp::Ordering>]
 
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::lt<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::le<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::gt<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::ge<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64 : core::cmp::PartialOrd<u32, u32>
 {
     parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::partial_cmp<'_0_0, '_0_1>
-    fn lt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::lt<'_0_0, '_0_1>
-    fn le<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::le<'_0_0, '_0_1>
-    fn gt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::gt<'_0_0, '_0_1>
-    fn ge<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<u32> for u32}#64::ge<'_0_0, '_0_1>
 }
 
 fn core::iter::range::{impl core::iter::range::Step for u32}#39::steps_between<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> core::option::Option<usize>[core::marker::Sized<usize>]
@@ -1335,14 +1110,6 @@ fn core::iter::range::{impl core::iter::range::Step for u32}#39::forward_checked
 
 fn core::iter::range::{impl core::iter::range::Step for u32}#39::backward_checked(@1: u32, @2: usize) -> core::option::Option<u32>[core::marker::Sized<u32>]
 
-fn core::iter::range::{impl core::iter::range::Step for u32}#39::forward(@1: u32, @2: usize) -> u32
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for u32}#39::forward_unchecked(@1: u32, @2: usize) -> u32
-
-fn core::iter::range::{impl core::iter::range::Step for u32}#39::backward(@1: u32, @2: usize) -> u32
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for u32}#39::backward_unchecked(@1: u32, @2: usize) -> u32
-
 impl core::iter::range::{impl core::iter::range::Step for u32}#39 : core::iter::range::Step<u32>
 {
     parent_clause0 = core::marker::Sized<u32>
@@ -1351,10 +1118,6 @@ impl core::iter::range::{impl core::iter::range::Step for u32}#39 : core::iter::
     fn steps_between<'_0, '_1> = core::iter::range::{impl core::iter::range::Step for u32}#39::steps_between<'_0_0, '_0_1>
     fn forward_checked = core::iter::range::{impl core::iter::range::Step for u32}#39::forward_checked
     fn backward_checked = core::iter::range::{impl core::iter::range::Step for u32}#39::backward_checked
-    fn forward = core::iter::range::{impl core::iter::range::Step for u32}#39::forward
-    fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for u32}#39::forward_unchecked
-    fn backward = core::iter::range::{impl core::iter::range::Step for u32}#39::backward
-    fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for u32}#39::backward_unchecked
 }
 
 fn test_crate::loop_inside_if(@1: bool, @2: u32) -> u32
@@ -1872,66 +1635,33 @@ fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &
 
 fn core::iter::range::Step::forward_checked<Self>(@1: Self, @2: usize) -> core::option::Option<Self>[Self::parent_clause0]
 
-fn core::iter::range::Step::forward<Self>(@1: Self, @2: usize) -> Self
-
-unsafe fn core::iter::range::Step::forward_unchecked<Self>(@1: Self, @2: usize) -> Self
-
 fn core::iter::range::Step::backward_checked<Self>(@1: Self, @2: usize) -> core::option::Option<Self>[Self::parent_clause0]
 
-fn core::iter::range::Step::backward<Self>(@1: Self, @2: usize) -> Self
-
-unsafe fn core::iter::range::Step::backward_unchecked<Self>(@1: Self, @2: usize) -> Self
-
 fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
 
 fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> core::option::Option<core::cmp::Ordering>[core::marker::Sized<core::cmp::Ordering>]
 
-fn core::cmp::PartialOrd::lt<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::le<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::gt<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::ge<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
 fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
 
-fn core::cmp::PartialEq::ne<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::cmp::Ordering
-
-fn core::iter::traits::iterator::Iterator::size_hint<'_0, Self>(@1: &'_0 (Self)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-
-fn core::iter::traits::iterator::Iterator::count<Self>(@1: Self) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::nth<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::option::Option<Self::Item>[Self::parent_clause0]
-
-fn core::iter::traits::iterator::Iterator::last<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::min<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-    [@TraitClause1]: core::cmp::Ord<Self::Item>,
-
-fn core::iter::traits::iterator::Iterator::max<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-    [@TraitClause1]: core::cmp::Ord<Self::Item>,
+trait core::cmp::Eq<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Self>
+}
 
-fn core::iter::traits::iterator::Iterator::is_sorted<Self>(@1: Self) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-    [@TraitClause1]: core::cmp::PartialOrd<Self::Item, Self::Item>,
+trait core::cmp::Ord<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::cmp::Eq<Self>
+    parent_clause1 : [@TraitClause1]: core::cmp::PartialOrd<Self, Self>
+    fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>
+}
 
-fn core::iter::traits::iterator::Iterator::advance_by<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
+trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    const MAY_HAVE_SIDE_EFFECT : bool
+}
 
-unsafe fn core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> Self::Item
-where
-    [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>,
+fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::cmp::Ordering
 
 trait core::marker::Tuple<Self>
 
@@ -2019,6 +1749,11 @@ trait core::iter::traits::exact_size::ExactSizeIterator<Self>
     parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
 }
 
+trait core::marker::Copy<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
+}
+
 trait core::iter::traits::accum::Sum<Self, A>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
diff --git a/charon/tests/ui/opaque-trait.out b/charon/tests/ui/opaque-trait.out
index 2b0376db..ffcfe131 100644
--- a/charon/tests/ui/opaque-trait.out
+++ b/charon/tests/ui/opaque-trait.out
@@ -37,7 +37,6 @@ trait test_crate::Trait<Self>
     const CONST3 : usize
     fn method1 = test_crate::Trait::method1<Self>
     fn method2 = test_crate::Trait::method2<Self>
-    fn method3 = test_crate::Trait::method3<Self>
 }
 
 fn test_crate::{impl test_crate::Trait for ()}#1::CONST1() -> usize
@@ -70,47 +69,11 @@ fn test_crate::{impl test_crate::Trait for ()}#1::CONST3() -> usize
 
 global test_crate::{impl test_crate::Trait for ()}#1::CONST3: usize = test_crate::{impl test_crate::Trait for ()}#1::CONST3()
 
-fn test_crate::{impl test_crate::Trait for ()}#1::method1()
-{
-    let @0: (); // return
-    let @1: (); // anonymous local
-
-    @1 := ()
-    @0 := move (@1)
-    @0 := ()
-    return
-}
-
-fn test_crate::{impl test_crate::Trait for ()}#1::method2()
-{
-    let @0: (); // return
-    let @1: (); // anonymous local
-
-    @1 := ()
-    @0 := move (@1)
-    @0 := ()
-    return
-}
-
-fn test_crate::{impl test_crate::Trait for ()}#1::method3()
-{
-    let @0: (); // return
-    let @1: (); // anonymous local
-
-    @1 := ()
-    @0 := move (@1)
-    @0 := ()
-    return
-}
-
 impl test_crate::{impl test_crate::Trait for ()}#1 : test_crate::Trait<()>
 {
     const CONST1 = test_crate::{impl test_crate::Trait for ()}#1::CONST1
     const CONST2 = test_crate::{impl test_crate::Trait for ()}#1::CONST2
     const CONST3 = test_crate::{impl test_crate::Trait for ()}#1::CONST3
-    fn method1 = test_crate::{impl test_crate::Trait for ()}#1::method1
-    fn method2 = test_crate::{impl test_crate::Trait for ()}#1::method2
-    fn method3 = test_crate::{impl test_crate::Trait for ()}#1::method3
 }
 
 fn test_crate::{impl test_crate::Trait for u8}::CONST2() -> usize
@@ -186,16 +149,5 @@ fn test_crate::Trait::method2<Self>()
     return
 }
 
-fn test_crate::Trait::method3<Self>()
-{
-    let @0: (); // return
-    let @1: (); // anonymous local
-
-    @1 := ()
-    @0 := move (@1)
-    @0 := ()
-    return
-}
-
 
 
diff --git a/charon/tests/ui/polonius_map.out b/charon/tests/ui/polonius_map.out
index f9f67991..66b1a370 100644
--- a/charon/tests/ui/polonius_map.out
+++ b/charon/tests/ui/polonius_map.out
@@ -21,7 +21,6 @@ enum core::option::Option<T>
 trait core::cmp::PartialEq<Self, Rhs>
 {
     fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>
-    fn ne<'_0, '_1> = core::cmp::PartialEq::ne<'_0_0, '_0_1, Self, Rhs>
 }
 
 trait core::cmp::Eq<Self>
@@ -33,13 +32,11 @@ trait core::hash::Hasher<Self>
 {
     fn finish<'_0> = core::hash::Hasher::finish<'_0_0, Self>
     fn write<'_0, '_1> = core::hash::Hasher::write<'_0_0, '_0_1, Self>
-    fn write_str<'_0, '_1> = core::hash::Hasher::write_str<'_0_0, '_0_1, Self>
 }
 
 trait core::hash::Hash<Self>
 {
     fn hash<'_0, '_1, H, [@TraitClause0]: core::marker::Sized<H>, [@TraitClause1]: core::hash::Hasher<H>> = core::hash::Hash::hash<'_0_0, '_0_1, Self, H>[@TraitClause0_0, @TraitClause0_1]
-    fn hash_slice<'_0, '_1, H, [@TraitClause0]: core::marker::Sized<H>, [@TraitClause1]: core::hash::Hasher<H>, [@TraitClause2]: core::marker::Sized<Self>> = core::hash::Hash::hash_slice<'_0_0, '_0_1, Self, H>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
 }
 
 trait core::hash::BuildHasher<Self>
@@ -69,12 +66,9 @@ where
 
 fn core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::eq<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::ne<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24 : core::cmp::PartialEq<u32, u32>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<u32> for u32}#24::ne<'_0_0, '_0_1>
 }
 
 impl core::cmp::impls::{impl core::cmp::Eq for u32}#43 : core::cmp::Eq<u32>
@@ -87,15 +81,9 @@ where
     [@TraitClause0]: core::marker::Sized<H>,
     [@TraitClause1]: core::hash::Hasher<H>,
 
-fn core::hash::impls::{impl core::hash::Hash for u32}#11::hash_slice<'_0, '_1, H>(@1: &'_0 (Slice<u32>), @2: &'_1 mut (H))
-where
-    [@TraitClause0]: core::marker::Sized<H>,
-    [@TraitClause1]: core::hash::Hasher<H>,
-
 impl core::hash::impls::{impl core::hash::Hash for u32}#11 : core::hash::Hash<u32>
 {
     fn hash<'_0, '_1, H, [@TraitClause0]: core::marker::Sized<H>, [@TraitClause1]: core::hash::Hasher<H>> = core::hash::impls::{impl core::hash::Hash for u32}#11::hash<'_0_0, '_0_1, H>[@TraitClause0_0, @TraitClause0_1]
-    fn hash_slice<'_0, '_1, H, [@TraitClause0]: core::marker::Sized<H>, [@TraitClause1]: core::hash::Hasher<H>> = core::hash::impls::{impl core::hash::Hash for u32}#11::hash_slice<'_0_0, '_0_1, H>[@TraitClause0_0, @TraitClause0_1]
 }
 
 opaque type std::hash::random::DefaultHasher
@@ -104,13 +92,10 @@ fn std::hash::random::{impl core::hash::Hasher for std::hash::random::DefaultHas
 
 fn std::hash::random::{impl core::hash::Hasher for std::hash::random::DefaultHasher}#4::write<'_0, '_1>(@1: &'_0 mut (std::hash::random::DefaultHasher), @2: &'_1 (Slice<u8>))
 
-fn std::hash::random::{impl core::hash::Hasher for std::hash::random::DefaultHasher}#4::write_str<'_0, '_1>(@1: &'_0 mut (std::hash::random::DefaultHasher), @2: &'_1 (Str))
-
 impl std::hash::random::{impl core::hash::Hasher for std::hash::random::DefaultHasher}#4 : core::hash::Hasher<std::hash::random::DefaultHasher>
 {
     fn finish<'_0> = std::hash::random::{impl core::hash::Hasher for std::hash::random::DefaultHasher}#4::finish<'_0_0>
     fn write<'_0, '_1> = std::hash::random::{impl core::hash::Hasher for std::hash::random::DefaultHasher}#4::write<'_0_0, '_0_1>
-    fn write_str<'_0, '_1> = std::hash::random::{impl core::hash::Hasher for std::hash::random::DefaultHasher}#4::write_str<'_0_0, '_0_1>
 }
 
 fn std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState}#1::build_hasher<'_0>(@1: &'_0 (std::hash::random::RandomState)) -> std::hash::random::DefaultHasher
@@ -238,26 +223,16 @@ fn core::hash::BuildHasher::build_hasher<'_0, Self>(@1: &'_0 (Self)) -> Self::Ha
 
 fn core::hash::Hasher::write<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Slice<u8>))
 
-fn core::hash::Hasher::write_str<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Str))
-
 fn core::hash::Hasher::finish<'_0, Self>(@1: &'_0 (Self)) -> u64
 
 fn core::borrow::Borrow::borrow<'_0, Self, Borrowed>(@1: &'_0 (Self)) -> &'_0 (Borrowed)
 
 fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
 
-fn core::cmp::PartialEq::ne<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
 fn core::hash::Hash::hash<'_0, '_1, Self, H>(@1: &'_0 (Self), @2: &'_1 mut (H))
 where
     [@TraitClause0]: core::marker::Sized<H>,
     [@TraitClause1]: core::hash::Hasher<H>,
 
-fn core::hash::Hash::hash_slice<'_0, '_1, Self, H>(@1: &'_0 (Slice<Self>), @2: &'_1 mut (H))
-where
-    [@TraitClause0]: core::marker::Sized<H>,
-    [@TraitClause1]: core::hash::Hasher<H>,
-    [@TraitClause2]: core::marker::Sized<Self>,
-
 
 
diff --git a/charon/tests/ui/trait-instance-id.out b/charon/tests/ui/trait-instance-id.out
index e8c5e3dc..42920eb2 100644
--- a/charon/tests/ui/trait-instance-id.out
+++ b/charon/tests/ui/trait-instance-id.out
@@ -46,139 +46,11 @@ fn core::array::iter::{impl core::iter::traits::collect::IntoIterator for Array<
 where
     [@TraitClause0]: core::marker::Sized<T>,
 
-enum core::result::Result<T, E>
-  where
-      [@TraitClause0]: core::marker::Sized<T>,
-      [@TraitClause1]: core::marker::Sized<E>,
- =
-|  Ok(T)
-|  Err(E)
-
-
-trait core::clone::Clone<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
-}
-
-trait core::marker::Copy<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
-}
-
-trait core::num::nonzero::private::Sealed<Self>
-
-trait core::num::nonzero::ZeroablePrimitive<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    parent_clause1 : [@TraitClause1]: core::marker::Copy<Self>
-    parent_clause2 : [@TraitClause2]: core::num::nonzero::private::Sealed<Self>
-    parent_clause3 : [@TraitClause3]: core::marker::Sized<Self::NonZeroInner>
-    parent_clause4 : [@TraitClause4]: core::marker::Copy<Self::NonZeroInner>
-    type NonZeroInner
-}
-
-opaque type core::num::nonzero::NonZero<T>
-  where
-      [@TraitClause0]: core::marker::Sized<T>,
-      [@TraitClause1]: core::num::nonzero::ZeroablePrimitive<T>,
-
-fn core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0>(@1: &'_0 (usize)) -> usize
-
-impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Clone<usize>
-{
-    parent_clause0 = core::marker::Sized<usize>
-    fn clone<'_0> = core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0_0>
-}
-
-impl core::marker::{impl core::marker::Copy for usize}#37 : core::marker::Copy<usize>
-{
-    parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize}#5
-}
-
-impl core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25 : core::num::nonzero::private::Sealed<usize>
-
-opaque type core::num::nonzero::private::NonZeroUsizeInner
-
-fn core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26::clone<'_0>(@1: &'_0 (core::num::nonzero::private::NonZeroUsizeInner)) -> core::num::nonzero::private::NonZeroUsizeInner
-
-impl core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26 : core::clone::Clone<core::num::nonzero::private::NonZeroUsizeInner>
-{
-    parent_clause0 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
-    fn clone<'_0> = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26::clone<'_0_0>
-}
-
-impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27 : core::marker::Copy<core::num::nonzero::private::NonZeroUsizeInner>
-{
-    parent_clause0 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26
-}
-
-impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26 : core::num::nonzero::ZeroablePrimitive<usize>
-{
-    parent_clause0 = core::marker::Sized<usize>
-    parent_clause1 = core::marker::{impl core::marker::Copy for usize}#37
-    parent_clause2 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25
-    parent_clause3 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
-    parent_clause4 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
-    type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner
-}
-
-trait core::marker::Tuple<Self>
-
-trait core::ops::function::FnOnce<Self, Args>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Args>
-    parent_clause1 : [@TraitClause1]: core::marker::Tuple<Args>
-    parent_clause2 : [@TraitClause2]: core::marker::Sized<Self::Output>
-    type Output
-    fn call_once = core::ops::function::FnOnce::call_once<Self, Args>
-}
-
-trait core::ops::function::FnMut<Self, Args>
-{
-    parent_clause0 : [@TraitClause0]: core::ops::function::FnOnce<Self, Args>
-    parent_clause1 : [@TraitClause1]: core::marker::Sized<Args>
-    parent_clause2 : [@TraitClause2]: core::marker::Tuple<Args>
-    fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>
-}
-
-trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    const MAY_HAVE_SIDE_EFFECT : bool
-}
-
 trait core::iter::traits::iterator::Iterator<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
     type Item
     fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
-    fn size_hint<'_0> = core::iter::traits::iterator::Iterator::size_hint<'_0_0, Self>
-    fn count<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::count<Self>[@TraitClause0_0]
-    fn last<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::last<Self>[@TraitClause0_0]
-    fn advance_by<'_0> = core::iter::traits::iterator::Iterator::advance_by<'_0_0, Self>
-    fn nth<'_0> = core::iter::traits::iterator::Iterator::nth<'_0_0, Self>
-    fn for_each<F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>, @TraitClause1_2::parent_clause0::Output = ()> = core::iter::traits::iterator::Iterator::for_each<Self, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn fold<B, F, [@TraitClause0]: core::marker::Sized<B>, [@TraitClause1]: core::marker::Sized<F>, [@TraitClause2]: core::marker::Sized<Self>, [@TraitClause3]: core::ops::function::FnMut<F, (B, Self::Item)>, @TraitClause1_3::parent_clause0::Output = B> = core::iter::traits::iterator::Iterator::fold<Self, B, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3]
-    fn all<'_0, F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>, @TraitClause1_2::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::all<'_0_0, Self, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn any<'_0, F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>, @TraitClause1_2::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::any<'_0_0, Self, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn find<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: for<'_0> core::ops::function::FnMut<P, (&'_0_0 (Self::Item))>, for<'_0> @TraitClause1_2::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::find<'_0_0, Self, P>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn find_map<'_0, B, F, [@TraitClause0]: core::marker::Sized<B>, [@TraitClause1]: core::marker::Sized<F>, [@TraitClause2]: core::marker::Sized<Self>, [@TraitClause3]: core::ops::function::FnMut<F, (Self::Item)>, @TraitClause1_3::parent_clause0::Output = core::option::Option<B>[@TraitClause1_0]> = core::iter::traits::iterator::Iterator::find_map<'_0_0, Self, B, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3]
-    fn position<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: core::ops::function::FnMut<P, (Self::Item)>, @TraitClause1_2::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::position<'_0_0, Self, P>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn rposition<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::ops::function::FnMut<P, (Self::Item)>, [@TraitClause2]: core::marker::Sized<Self>, [@TraitClause3]: core::iter::traits::exact_size::ExactSizeIterator<Self>, [@TraitClause4]: core::iter::traits::double_ended::DoubleEndedIterator<Self>, @TraitClause1_1::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::rposition<'_0_0, Self, P>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4]
-    fn is_sorted_by<F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: for<'_0, '_1> core::ops::function::FnMut<F, (&'_0_0 (Self::Item), &'_0_1 (Self::Item))>, for<'_0, '_1> @TraitClause1_2::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::is_sorted_by<Self, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn __iterator_get_unchecked<'_0, [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>> = core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0_0, Self>[@TraitClause0_0]
-}
-
-trait core::iter::traits::exact_size::ExactSizeIterator<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
-}
-
-trait core::iter::traits::double_ended::DoubleEndedIterator<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
-    fn next_back<'_0> = core::iter::traits::double_ended::DoubleEndedIterator::next_back<'_0_0, Self>
 }
 
 fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<I>(@1: I) -> I
@@ -190,34 +62,6 @@ fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::arr
 where
     [@TraitClause0]: core::marker::Sized<T>,
 
-fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::size_hint<'_0, T, const N : usize>(@1: &'_0 (core::array::iter::IntoIter<T, const N : usize>[@TraitClause0])) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::count<T, const N : usize>(@1: core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::last<T, const N : usize>(@1: core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]) -> core::option::Option<T>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::advance_by<'_0, T, const N : usize>(@1: &'_0 mut (core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::fold<T, Acc, Fold, const N : usize>(@1: core::array::iter::IntoIter<T, const N : usize>[@TraitClause0], @2: Acc, @3: Fold) -> Acc
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<Acc>,
-    [@TraitClause2]: core::marker::Sized<Fold>,
-    [@TraitClause3]: core::ops::function::FnMut<Fold, (Acc, T)>,
-    @TraitClause3::parent_clause0::Output = Acc,
-
-unsafe fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::__iterator_get_unchecked<'_0, T, const N : usize>(@1: &'_0 mut (core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]), @2: usize) -> T
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
 impl<T, const N : usize> core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2<T, const N : usize> : core::iter::traits::iterator::Iterator<core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<T>,
@@ -225,12 +69,6 @@ where
     parent_clause0 = @TraitClause0
     type Item = T
     fn next<'_0> = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::next<'_0_0, T, const N : usize>[@TraitClause0]
-    fn size_hint<'_0> = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::size_hint<'_0_0, T, const N : usize>[@TraitClause0]
-    fn count = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::count<T, const N : usize>[@TraitClause0]
-    fn last = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::last<T, const N : usize>[@TraitClause0]
-    fn advance_by<'_0> = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::advance_by<'_0_0, T, const N : usize>[@TraitClause0]
-    fn fold<Acc, Fold, [@TraitClause0]: core::marker::Sized<Acc>, [@TraitClause1]: core::marker::Sized<Fold>, [@TraitClause2]: core::ops::function::FnMut<Fold, (Acc, T)>, @TraitClause1_2::parent_clause0::Output = Acc> = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::fold<T, Acc, Fold, const N : usize>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn __iterator_get_unchecked<'_0> = core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter<T, const N : usize>[@TraitClause0]}#2::__iterator_get_unchecked<'_0_0, T, const N : usize>[@TraitClause0]
 }
 
 fn core::slice::{Slice<T>}::iter<'_0, T>(@1: &'_0 (Slice<T>)) -> core::slice::iter::Iter<'_0, T>[@TraitClause0]
@@ -241,105 +79,6 @@ fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::sli
 where
     [@TraitClause0]: core::marker::Sized<T>,
 
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::Iter<'a, T>[@TraitClause0])) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::count<'a, T>(@1: core::slice::iter::Iter<'a, T>[@TraitClause0]) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::last<'a, T>(@1: core::slice::iter::Iter<'a, T>[@TraitClause0]) -> core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::advance_by<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::for_each<'a, T, F>(@1: core::slice::iter::Iter<'a, T>[@TraitClause0], @2: F)
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (&'_ (T))>,
-    @TraitClause3::parent_clause0::Output = (),
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::fold<'a, T, B, F>(@1: core::slice::iter::Iter<'a, T>[@TraitClause0], @2: B, @3: F) -> B
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<B>,
-    [@TraitClause2]: core::marker::Sized<F>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (B, &'_ (T))>,
-    @TraitClause3::parent_clause0::Output = B,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::all<'a, '_1, T, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (&'_ (T))>,
-    @TraitClause3::parent_clause0::Output = bool,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::any<'a, '_1, T, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (&'_ (T))>,
-    @TraitClause3::parent_clause0::Output = bool,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: P) -> core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<P>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: for<'_0> core::ops::function::FnMut<P, (&'_0_0 (&'_ (T)))>,
-    for<'_0> @TraitClause3::parent_clause0::Output = bool,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find_map<'a, '_1, T, B, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: F) -> core::option::Option<B>[@TraitClause1]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<B>,
-    [@TraitClause2]: core::marker::Sized<F>,
-    [@TraitClause3]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause4]: core::ops::function::FnMut<F, (&'_ (T))>,
-    @TraitClause4::parent_clause0::Output = core::option::Option<B>[@TraitClause1],
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::position<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: P) -> core::option::Option<usize>[core::marker::Sized<usize>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<P>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: core::ops::function::FnMut<P, (&'_ (T))>,
-    @TraitClause3::parent_clause0::Output = bool,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::rposition<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: P) -> core::option::Option<usize>[core::marker::Sized<usize>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<P>,
-    [@TraitClause2]: core::ops::function::FnMut<P, (@TraitClause4::parent_clause0::Item)>,
-    [@TraitClause3]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause4]: core::iter::traits::exact_size::ExactSizeIterator<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause5]: core::iter::traits::double_ended::DoubleEndedIterator<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    @TraitClause2::parent_clause0::Output = bool,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::is_sorted_by<'a, T, F>(@1: core::slice::iter::Iter<'a, T>[@TraitClause0], @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: for<'_0, '_1> core::ops::function::FnMut<F, (&'_0_0 (&'_ (T)), &'_0_1 (&'_ (T)))>,
-    for<'_0, '_1> @TraitClause3::parent_clause0::Output = bool,
-
-unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: usize) -> &'_ (T)
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
 impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182<'a, T> : core::iter::traits::iterator::Iterator<core::slice::iter::Iter<'a, T>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<T>,
@@ -347,21 +86,6 @@ where
     parent_clause0 = core::marker::Sized<&'_ (T)>
     type Item = &'a (T)
     fn next<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::next<'a, '_0_0, T>[@TraitClause0]
-    fn size_hint<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::size_hint<'a, '_0_0, T>[@TraitClause0]
-    fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::count<'a, T>[@TraitClause0]
-    fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::last<'a, T>[@TraitClause0]
-    fn advance_by<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::advance_by<'a, '_0_0, T>[@TraitClause0]
-    fn nth<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::nth<'a, '_0_0, T>[@TraitClause0]
-    fn for_each<F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: core::ops::function::FnMut<F, (&'_ (T))>, @TraitClause1_2::parent_clause0::Output = ()> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::for_each<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn fold<B, F, [@TraitClause0]: core::marker::Sized<B>, [@TraitClause1]: core::marker::Sized<F>, [@TraitClause2]: core::ops::function::FnMut<F, (B, &'_ (T))>, @TraitClause1_2::parent_clause0::Output = B> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::fold<'a, T, B, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn all<'_0, F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: core::ops::function::FnMut<F, (&'_ (T))>, @TraitClause1_2::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::all<'a, '_0_0, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn any<'_0, F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: core::ops::function::FnMut<F, (&'_ (T))>, @TraitClause1_2::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::any<'a, '_0_0, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn find<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: for<'_0> core::ops::function::FnMut<P, (&'_0_0 (&'_ (T)))>, for<'_0> @TraitClause1_2::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn find_map<'_0, B, F, [@TraitClause0]: core::marker::Sized<B>, [@TraitClause1]: core::marker::Sized<F>, [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause3]: core::ops::function::FnMut<F, (&'_ (T))>, @TraitClause1_3::parent_clause0::Output = core::option::Option<B>[@TraitClause1_0]> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find_map<'a, '_0_0, T, B, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3]
-    fn position<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: core::ops::function::FnMut<P, (&'_ (T))>, @TraitClause1_2::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::position<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn rposition<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::ops::function::FnMut<P, (@TraitClause1_3::parent_clause0::Item)>, [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause3]: core::iter::traits::exact_size::ExactSizeIterator<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause4]: core::iter::traits::double_ended::DoubleEndedIterator<core::slice::iter::Iter<'_, T>[@TraitClause0]>, @TraitClause1_1::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::rposition<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4]
-    fn is_sorted_by<F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: for<'_0, '_1> core::ops::function::FnMut<F, (&'_0_0 (&'_ (T)), &'_0_1 (&'_ (T)))>, for<'_0, '_1> @TraitClause1_2::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::is_sorted_by<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn __iterator_get_unchecked<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0]
 }
 
 fn core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32}#365::add_assign<'_0, '_1>(@1: &'_1 mut (i32), @2: &'_0 (i32))
@@ -374,26 +98,6 @@ fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::sli
 where
     [@TraitClause0]: core::marker::Sized<T>,
 
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::Chunks<'a, T>[@TraitClause0])) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::count<'a, T>(@1: core::slice::iter::Chunks<'a, T>[@TraitClause0]) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::last<'a, T>(@1: core::slice::iter::Chunks<'a, T>[@TraitClause0]) -> core::option::Option<&'_ (Slice<T>)>[core::marker::Sized<&'_ (Slice<T>)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option<&'_ (Slice<T>)>[core::marker::Sized<&'_ (Slice<T>)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>[@TraitClause0]), @2: usize) -> &'_ (Slice<T>)
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
 impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71<'a, T> : core::iter::traits::iterator::Iterator<core::slice::iter::Chunks<'a, T>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<T>,
@@ -401,11 +105,6 @@ where
     parent_clause0 = core::marker::Sized<&'_ (Slice<T>)>
     type Item = &'a (Slice<T>)
     fn next<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::next<'a, '_0_0, T>[@TraitClause0]
-    fn size_hint<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::size_hint<'a, '_0_0, T>[@TraitClause0]
-    fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::count<'a, T>[@TraitClause0]
-    fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::last<'a, T>[@TraitClause0]
-    fn nth<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::nth<'a, '_0_0, T>[@TraitClause0]
-    fn __iterator_get_unchecked<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>[@TraitClause0]}#71::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0]
 }
 
 fn core::slice::{Slice<T>}::chunks_exact<'_0, T>(@1: &'_0 (Slice<T>), @2: usize) -> core::slice::iter::ChunksExact<'_0, T>[@TraitClause0]
@@ -416,26 +115,6 @@ fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::sli
 where
     [@TraitClause0]: core::marker::Sized<T>,
 
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::ChunksExact<'a, T>[@TraitClause0])) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::count<'a, T>(@1: core::slice::iter::ChunksExact<'a, T>[@TraitClause0]) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::last<'a, T>(@1: core::slice::iter::ChunksExact<'a, T>[@TraitClause0]) -> core::option::Option<&'_ (Slice<T>)>[core::marker::Sized<&'_ (Slice<T>)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option<&'_ (Slice<T>)>[core::marker::Sized<&'_ (Slice<T>)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>[@TraitClause0]), @2: usize) -> &'_ (Slice<T>)
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
 impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90<'a, T> : core::iter::traits::iterator::Iterator<core::slice::iter::ChunksExact<'a, T>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<T>,
@@ -443,11 +122,6 @@ where
     parent_clause0 = core::marker::Sized<&'_ (Slice<T>)>
     type Item = &'a (Slice<T>)
     fn next<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::next<'a, '_0_0, T>[@TraitClause0]
-    fn size_hint<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::size_hint<'a, '_0_0, T>[@TraitClause0]
-    fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::count<'a, T>[@TraitClause0]
-    fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::last<'a, T>[@TraitClause0]
-    fn nth<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::nth<'a, '_0_0, T>[@TraitClause0]
-    fn __iterator_get_unchecked<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>[@TraitClause0]}#90::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0]
 }
 
 fn test_crate::main()
@@ -809,44 +483,34 @@ impl<'_0> core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i3
     fn add_assign<'_0> = core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32}#365::add_assign<'_0, '_0_0>
 }
 
-fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> Self::parent_clause0::Output
-
-fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> Self::Output
-
-fn core::iter::traits::iterator::Iterator::size_hint<'_0, Self>(@1: &'_0 (Self)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-
-fn core::iter::traits::iterator::Iterator::fold<Self, B, F>(@1: Self, @2: B, @3: F) -> B
-where
-    [@TraitClause0]: core::marker::Sized<B>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<Self>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (B, Self::Item)>,
-    @TraitClause3::parent_clause0::Output = B,
-
-fn core::iter::traits::iterator::Iterator::count<Self>(@1: Self) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::last<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
+trait core::marker::Tuple<Self>
 
-fn core::iter::traits::iterator::Iterator::advance_by<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
+trait core::ops::function::FnOnce<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Args>
+    parent_clause1 : [@TraitClause1]: core::marker::Tuple<Args>
+    parent_clause2 : [@TraitClause2]: core::marker::Sized<Self::Output>
+    type Output
+    fn call_once = core::ops::function::FnOnce::call_once<Self, Args>
+}
 
-fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
+trait core::ops::function::FnMut<Self, Args>
+{
+    parent_clause0 : [@TraitClause0]: core::ops::function::FnOnce<Self, Args>
+    parent_clause1 : [@TraitClause1]: core::marker::Sized<Args>
+    parent_clause2 : [@TraitClause2]: core::marker::Tuple<Args>
+    fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>
+}
 
-unsafe fn core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> Self::Item
-where
-    [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>,
+fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> Self::parent_clause0::Output
 
-fn core::iter::traits::iterator::Iterator::nth<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::option::Option<Self::Item>[Self::parent_clause0]
+fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> Self::Output
 
-fn core::iter::traits::iterator::Iterator::for_each<Self, F>(@1: Self, @2: F)
-where
-    [@TraitClause0]: core::marker::Sized<F>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>,
-    @TraitClause2::parent_clause0::Output = (),
+trait core::clone::Clone<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
+}
 
 trait core::iter::traits::collect::FromIterator<Self, A>
 {
@@ -904,50 +568,16 @@ trait core::default::Default<Self>
     fn default = core::default::Default::default<Self>
 }
 
-fn core::iter::traits::iterator::Iterator::all<'_0, Self, F>(@1: &'_0 mut (Self), @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<F>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>,
-    @TraitClause2::parent_clause0::Output = bool,
-
-fn core::iter::traits::iterator::Iterator::any<'_0, Self, F>(@1: &'_0 mut (Self), @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<F>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>,
-    @TraitClause2::parent_clause0::Output = bool,
-
-fn core::iter::traits::iterator::Iterator::find<'_0, Self, P>(@1: &'_0 mut (Self), @2: P) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<P>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: for<'_0> core::ops::function::FnMut<P, (&'_0_0 (Self::Item))>,
-    for<'_0> @TraitClause2::parent_clause0::Output = bool,
-
-fn core::iter::traits::iterator::Iterator::find_map<'_0, Self, B, F>(@1: &'_0 mut (Self), @2: F) -> core::option::Option<B>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<B>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<Self>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (Self::Item)>,
-    @TraitClause3::parent_clause0::Output = core::option::Option<B>[@TraitClause0],
-
-fn core::iter::traits::iterator::Iterator::position<'_0, Self, P>(@1: &'_0 mut (Self), @2: P) -> core::option::Option<usize>[core::marker::Sized<usize>]
-where
-    [@TraitClause0]: core::marker::Sized<P>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: core::ops::function::FnMut<P, (Self::Item)>,
-    @TraitClause2::parent_clause0::Output = bool,
+trait core::iter::traits::double_ended::DoubleEndedIterator<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
+    fn next_back<'_0> = core::iter::traits::double_ended::DoubleEndedIterator::next_back<'_0_0, Self>
+}
 
-fn core::iter::traits::iterator::Iterator::rposition<'_0, Self, P>(@1: &'_0 mut (Self), @2: P) -> core::option::Option<usize>[core::marker::Sized<usize>]
-where
-    [@TraitClause0]: core::marker::Sized<P>,
-    [@TraitClause1]: core::ops::function::FnMut<P, (Self::Item)>,
-    [@TraitClause2]: core::marker::Sized<Self>,
-    [@TraitClause3]: core::iter::traits::exact_size::ExactSizeIterator<Self>,
-    [@TraitClause4]: core::iter::traits::double_ended::DoubleEndedIterator<Self>,
-    @TraitClause1::parent_clause0::Output = bool,
+trait core::iter::traits::exact_size::ExactSizeIterator<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
+}
 
 trait core::cmp::PartialEq<Self, Rhs>
 {
@@ -978,6 +608,11 @@ trait core::cmp::Ord<Self>
     fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>
 }
 
+trait core::marker::Copy<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
+}
+
 trait core::iter::traits::accum::Sum<Self, A>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
@@ -992,12 +627,13 @@ trait core::iter::traits::accum::Product<Self, A>
     fn product<I, [@TraitClause0]: core::marker::Sized<I>, [@TraitClause1]: core::iter::traits::iterator::Iterator<I>, @TraitClause1_1::Item = A> = core::iter::traits::accum::Product::product<Self, A, I>[@TraitClause0_0, @TraitClause0_1]
 }
 
-fn core::iter::traits::iterator::Iterator::is_sorted_by<Self, F>(@1: Self, @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<F>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: for<'_0, '_1> core::ops::function::FnMut<F, (&'_0_0 (Self::Item), &'_0_1 (Self::Item))>,
-    for<'_0, '_1> @TraitClause2::parent_clause0::Output = bool,
+trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    const MAY_HAVE_SIDE_EFFECT : bool
+}
+
+fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
 
 fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
 
diff --git a/charon/tests/ui/type_alias.out b/charon/tests/ui/type_alias.out
index 53a56ddf..b509a71b 100644
--- a/charon/tests/ui/type_alias.out
+++ b/charon/tests/ui/type_alias.out
@@ -19,7 +19,6 @@ trait alloc::borrow::ToOwned<Self>
     parent_clause1 : [@TraitClause1]: core::borrow::Borrow<Self::Owned, Self>
     type Owned
     fn to_owned<'_0> = alloc::borrow::ToOwned::to_owned<'_0_0, Self>
-    fn clone_into<'_0, '_1> = alloc::borrow::ToOwned::clone_into<'_0_0, '_0_1, Self>
 }
 
 enum alloc::borrow::Cow<'a, B>
@@ -57,11 +56,6 @@ where
     [@TraitClause0]: core::marker::Sized<T>,
     [@TraitClause1]: core::clone::Clone<T>,
 
-fn alloc::slice::{impl alloc::borrow::ToOwned for Slice<T>}#9::clone_into<'_0, '_1, T>(@1: &'_0 (Slice<T>), @2: &'_1 mut (alloc::vec::Vec<T, alloc::alloc::Global>[@TraitClause0, core::marker::Sized<alloc::alloc::Global>]))
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::clone::Clone<T>,
-
 impl<T> alloc::slice::{impl alloc::borrow::ToOwned for Slice<T>}#9<T> : alloc::borrow::ToOwned<Slice<T>>
 where
     [@TraitClause0]: core::marker::Sized<T>,
@@ -71,7 +65,6 @@ where
     parent_clause1 = alloc::slice::{impl core::borrow::Borrow<Slice<T>> for alloc::vec::Vec<T, A>[@TraitClause0, @TraitClause1]}#5<T, alloc::alloc::Global>[@TraitClause0, core::marker::Sized<alloc::alloc::Global>]
     type Owned = alloc::vec::Vec<T, alloc::alloc::Global>[@TraitClause0, core::marker::Sized<alloc::alloc::Global>]
     fn to_owned<'_0> = alloc::slice::{impl alloc::borrow::ToOwned for Slice<T>}#9::to_owned<'_0_0, T>[@TraitClause0, @TraitClause1]
-    fn clone_into<'_0, '_1> = alloc::slice::{impl alloc::borrow::ToOwned for Slice<T>}#9::clone_into<'_0_0, '_0_1, T>[@TraitClause0, @TraitClause1]
 }
 
 struct test_crate::Generic2<'a, T>
@@ -88,8 +81,6 @@ fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
 
 fn alloc::borrow::ToOwned::to_owned<'_0, Self>(@1: &'_0 (Self)) -> Self::Owned
 
-fn alloc::borrow::ToOwned::clone_into<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 mut (Self::Owned))
-
 fn core::borrow::Borrow::borrow<'_0, Self, Borrowed>(@1: &'_0 (Self)) -> &'_0 (Borrowed)
 
 
diff --git a/charon/tests/ui/ullbc-control-flow.out b/charon/tests/ui/ullbc-control-flow.out
index c3eb37c4..324dc081 100644
--- a/charon/tests/ui/ullbc-control-flow.out
+++ b/charon/tests/ui/ullbc-control-flow.out
@@ -19,92 +19,27 @@ enum core::option::Option<T>
 |  Some(T)
 
 
-enum core::result::Result<T, E>
-  where
-      [@TraitClause0]: core::marker::Sized<T>,
-      [@TraitClause1]: core::marker::Sized<E>,
- =
-|  Ok(T)
-|  Err(E)
-
-
-trait core::clone::Clone<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
-}
-
-trait core::marker::Copy<Self>
+trait core::iter::traits::iterator::Iterator<Self>
 {
-    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
+    type Item
+    fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
 }
 
-trait core::num::nonzero::private::Sealed<Self>
+fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<I>(@1: I) -> I
+where
+    [@TraitClause0]: core::marker::Sized<I>,
+    [@TraitClause1]: core::iter::traits::iterator::Iterator<I>,
 
-trait core::num::nonzero::ZeroablePrimitive<Self>
+trait core::clone::Clone<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    parent_clause1 : [@TraitClause1]: core::marker::Copy<Self>
-    parent_clause2 : [@TraitClause2]: core::num::nonzero::private::Sealed<Self>
-    parent_clause3 : [@TraitClause3]: core::marker::Sized<Self::NonZeroInner>
-    parent_clause4 : [@TraitClause4]: core::marker::Copy<Self::NonZeroInner>
-    type NonZeroInner
-}
-
-opaque type core::num::nonzero::NonZero<T>
-  where
-      [@TraitClause0]: core::marker::Sized<T>,
-      [@TraitClause1]: core::num::nonzero::ZeroablePrimitive<T>,
-
-fn core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0>(@1: &'_0 (usize)) -> usize
-
-impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Clone<usize>
-{
-    parent_clause0 = core::marker::Sized<usize>
-    fn clone<'_0> = core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0_0>
-}
-
-impl core::marker::{impl core::marker::Copy for usize}#37 : core::marker::Copy<usize>
-{
-    parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize}#5
-}
-
-impl core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25 : core::num::nonzero::private::Sealed<usize>
-
-opaque type core::num::nonzero::private::NonZeroUsizeInner
-
-fn core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26::clone<'_0>(@1: &'_0 (core::num::nonzero::private::NonZeroUsizeInner)) -> core::num::nonzero::private::NonZeroUsizeInner
-
-impl core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26 : core::clone::Clone<core::num::nonzero::private::NonZeroUsizeInner>
-{
-    parent_clause0 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
-    fn clone<'_0> = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26::clone<'_0_0>
-}
-
-impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27 : core::marker::Copy<core::num::nonzero::private::NonZeroUsizeInner>
-{
-    parent_clause0 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26
-}
-
-impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26 : core::num::nonzero::ZeroablePrimitive<usize>
-{
-    parent_clause0 = core::marker::Sized<usize>
-    parent_clause1 = core::marker::{impl core::marker::Copy for usize}#37
-    parent_clause2 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25
-    parent_clause3 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
-    parent_clause4 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
-    type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner
+    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
 }
 
 trait core::cmp::PartialEq<Self, Rhs>
 {
     fn eq<'_0, '_1> = core::cmp::PartialEq::eq<'_0_0, '_0_1, Self, Rhs>
-    fn ne<'_0, '_1> = core::cmp::PartialEq::ne<'_0_0, '_0_1, Self, Rhs>
-}
-
-trait core::cmp::Eq<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Self>
 }
 
 enum core::cmp::Ordering =
@@ -117,46 +52,8 @@ trait core::cmp::PartialOrd<Self, Rhs>
 {
     parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Rhs>
     fn partial_cmp<'_0, '_1> = core::cmp::PartialOrd::partial_cmp<'_0_0, '_0_1, Self, Rhs>
-    fn lt<'_0, '_1> = core::cmp::PartialOrd::lt<'_0_0, '_0_1, Self, Rhs>
-    fn le<'_0, '_1> = core::cmp::PartialOrd::le<'_0_0, '_0_1, Self, Rhs>
-    fn gt<'_0, '_1> = core::cmp::PartialOrd::gt<'_0_0, '_0_1, Self, Rhs>
-    fn ge<'_0, '_1> = core::cmp::PartialOrd::ge<'_0_0, '_0_1, Self, Rhs>
-}
-
-trait core::cmp::Ord<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::cmp::Eq<Self>
-    parent_clause1 : [@TraitClause1]: core::cmp::PartialOrd<Self, Self>
-    fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>
-}
-
-trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    const MAY_HAVE_SIDE_EFFECT : bool
-}
-
-trait core::iter::traits::iterator::Iterator<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
-    type Item
-    fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
-    fn size_hint<'_0> = core::iter::traits::iterator::Iterator::size_hint<'_0_0, Self>
-    fn count<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::count<Self>[@TraitClause0_0]
-    fn last<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::last<Self>[@TraitClause0_0]
-    fn advance_by<'_0> = core::iter::traits::iterator::Iterator::advance_by<'_0_0, Self>
-    fn nth<'_0> = core::iter::traits::iterator::Iterator::nth<'_0_0, Self>
-    fn max<[@TraitClause0]: core::marker::Sized<Self>, [@TraitClause1]: core::cmp::Ord<Self::Item>> = core::iter::traits::iterator::Iterator::max<Self>[@TraitClause0_0, @TraitClause0_1]
-    fn min<[@TraitClause0]: core::marker::Sized<Self>, [@TraitClause1]: core::cmp::Ord<Self::Item>> = core::iter::traits::iterator::Iterator::min<Self>[@TraitClause0_0, @TraitClause0_1]
-    fn is_sorted<[@TraitClause0]: core::marker::Sized<Self>, [@TraitClause1]: core::cmp::PartialOrd<Self::Item, Self::Item>> = core::iter::traits::iterator::Iterator::is_sorted<Self>[@TraitClause0_0, @TraitClause0_1]
-    fn __iterator_get_unchecked<'_0, [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>> = core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0_0, Self>[@TraitClause0_0]
 }
 
-fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}#1::into_iter<I>(@1: I) -> I
-where
-    [@TraitClause0]: core::marker::Sized<I>,
-    [@TraitClause1]: core::iter::traits::iterator::Iterator<I>,
-
 trait core::iter::range::Step<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
@@ -165,10 +62,6 @@ trait core::iter::range::Step<Self>
     fn steps_between<'_0, '_1> = core::iter::range::Step::steps_between<'_0_0, '_0_1, Self>
     fn forward_checked = core::iter::range::Step::forward_checked<Self>
     fn backward_checked = core::iter::range::Step::backward_checked<Self>
-    fn forward = core::iter::range::Step::forward<Self>
-    fn forward_unchecked = core::iter::range::Step::forward_unchecked<Self>
-    fn backward = core::iter::range::Step::backward<Self>
-    fn backward_unchecked = core::iter::range::Step::backward_unchecked<Self>
 }
 
 fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0])) -> core::option::Option<A>[@TraitClause0]
@@ -176,54 +69,6 @@ where
     [@TraitClause0]: core::marker::Sized<A>,
     [@TraitClause1]: core::iter::range::Step<A>,
 
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::size_hint<'_0, A>(@1: &'_0 (core::ops::range::Range<A>[@TraitClause0])) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::count<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::last<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0]), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::nth<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0]), @2: usize) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::max<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-    [@TraitClause2]: core::cmp::Ord<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::min<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> core::option::Option<A>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-    [@TraitClause2]: core::cmp::Ord<A>,
-
-fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::is_sorted<A>(@1: core::ops::range::Range<A>[@TraitClause0]) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-
-unsafe fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::__iterator_get_unchecked<'_0, A>(@1: &'_0 mut (core::ops::range::Range<A>[@TraitClause0]), @2: usize) -> A
-where
-    [@TraitClause0]: core::marker::Sized<A>,
-    [@TraitClause1]: core::iter::range::Step<A>,
-    [@TraitClause2]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<core::ops::range::Range<A>[@TraitClause0]>,
-
 impl<A> core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6<A> : core::iter::traits::iterator::Iterator<core::ops::range::Range<A>[@TraitClause0]>
 where
     [@TraitClause0]: core::marker::Sized<A>,
@@ -232,15 +77,6 @@ where
     parent_clause0 = @TraitClause0
     type Item = A
     fn next<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::next<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn size_hint<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::size_hint<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn count = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::count<A>[@TraitClause0, @TraitClause1]
-    fn last = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::last<A>[@TraitClause0, @TraitClause1]
-    fn advance_by<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::advance_by<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn nth<'_0> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::nth<'_0_0, A>[@TraitClause0, @TraitClause1]
-    fn max<[@TraitClause0]: core::cmp::Ord<A>> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::max<A>[@TraitClause0, @TraitClause1, @TraitClause0_0]
-    fn min<[@TraitClause0]: core::cmp::Ord<A>> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::min<A>[@TraitClause0, @TraitClause1, @TraitClause0_0]
-    fn is_sorted = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::is_sorted<A>[@TraitClause0, @TraitClause1]
-    fn __iterator_get_unchecked<'_0, [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<core::ops::range::Range<A>[@TraitClause0]>> = core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range<A>[@TraitClause0]}#6::__iterator_get_unchecked<'_0_0, A>[@TraitClause0, @TraitClause1, @TraitClause0_0]
 }
 
 fn core::clone::impls::{impl core::clone::Clone for i32}#14::clone<'_0>(@1: &'_0 (i32)) -> i32
@@ -253,32 +89,17 @@ impl core::clone::impls::{impl core::clone::Clone for i32}#14 : core::clone::Clo
 
 fn core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::eq<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::ne<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30 : core::cmp::PartialEq<i32, i32>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30::ne<'_0_0, '_0_1>
 }
 
 fn core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::partial_cmp<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option<core::cmp::Ordering>[core::marker::Sized<core::cmp::Ordering>]
 
-fn core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::lt<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::le<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::gt<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::ge<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76 : core::cmp::PartialOrd<i32, i32>
 {
     parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq<i32> for i32}#30
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::partial_cmp<'_0_0, '_0_1>
-    fn lt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::lt<'_0_0, '_0_1>
-    fn le<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::le<'_0_0, '_0_1>
-    fn gt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::gt<'_0_0, '_0_1>
-    fn ge<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<i32> for i32}#76::ge<'_0_0, '_0_1>
 }
 
 fn core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option<usize>[core::marker::Sized<usize>]
@@ -287,14 +108,6 @@ fn core::iter::range::{impl core::iter::range::Step for i32}#40::forward_checked
 
 fn core::iter::range::{impl core::iter::range::Step for i32}#40::backward_checked(@1: i32, @2: usize) -> core::option::Option<i32>[core::marker::Sized<i32>]
 
-fn core::iter::range::{impl core::iter::range::Step for i32}#40::forward(@1: i32, @2: usize) -> i32
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for i32}#40::forward_unchecked(@1: i32, @2: usize) -> i32
-
-fn core::iter::range::{impl core::iter::range::Step for i32}#40::backward(@1: i32, @2: usize) -> i32
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for i32}#40::backward_unchecked(@1: i32, @2: usize) -> i32
-
 impl core::iter::range::{impl core::iter::range::Step for i32}#40 : core::iter::range::Step<i32>
 {
     parent_clause0 = core::marker::Sized<i32>
@@ -303,40 +116,29 @@ impl core::iter::range::{impl core::iter::range::Step for i32}#40 : core::iter::
     fn steps_between<'_0, '_1> = core::iter::range::{impl core::iter::range::Step for i32}#40::steps_between<'_0_0, '_0_1>
     fn forward_checked = core::iter::range::{impl core::iter::range::Step for i32}#40::forward_checked
     fn backward_checked = core::iter::range::{impl core::iter::range::Step for i32}#40::backward_checked
-    fn forward = core::iter::range::{impl core::iter::range::Step for i32}#40::forward
-    fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for i32}#40::forward_unchecked
-    fn backward = core::iter::range::{impl core::iter::range::Step for i32}#40::backward
-    fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for i32}#40::backward_unchecked
 }
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21::eq<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
+fn core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0>(@1: &'_0 (usize)) -> usize
 
-fn core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21::ne<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
+impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Clone<usize>
+{
+    parent_clause0 = core::marker::Sized<usize>
+    fn clone<'_0> = core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0_0>
+}
+
+fn core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21::eq<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
 
 impl core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21 : core::cmp::PartialEq<usize, usize>
 {
     fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21::eq<'_0_0, '_0_1>
-    fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21::ne<'_0_0, '_0_1>
 }
 
 fn core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::partial_cmp<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option<core::cmp::Ordering>[core::marker::Sized<core::cmp::Ordering>]
 
-fn core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::lt<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::le<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::gt<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
-
-fn core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::ge<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool
-
 impl core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58 : core::cmp::PartialOrd<usize, usize>
 {
     parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq<usize> for usize}#21
     fn partial_cmp<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::partial_cmp<'_0_0, '_0_1>
-    fn lt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::lt<'_0_0, '_0_1>
-    fn le<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::le<'_0_0, '_0_1>
-    fn gt<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::gt<'_0_0, '_0_1>
-    fn ge<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialOrd<usize> for usize}#58::ge<'_0_0, '_0_1>
 }
 
 fn core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option<usize>[core::marker::Sized<usize>]
@@ -345,14 +147,6 @@ fn core::iter::range::{impl core::iter::range::Step for usize}#43::forward_check
 
 fn core::iter::range::{impl core::iter::range::Step for usize}#43::backward_checked(@1: usize, @2: usize) -> core::option::Option<usize>[core::marker::Sized<usize>]
 
-fn core::iter::range::{impl core::iter::range::Step for usize}#43::forward(@1: usize, @2: usize) -> usize
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for usize}#43::forward_unchecked(@1: usize, @2: usize) -> usize
-
-fn core::iter::range::{impl core::iter::range::Step for usize}#43::backward(@1: usize, @2: usize) -> usize
-
-unsafe fn core::iter::range::{impl core::iter::range::Step for usize}#43::backward_unchecked(@1: usize, @2: usize) -> usize
-
 impl core::iter::range::{impl core::iter::range::Step for usize}#43 : core::iter::range::Step<usize>
 {
     parent_clause0 = core::marker::Sized<usize>
@@ -361,10 +155,6 @@ impl core::iter::range::{impl core::iter::range::Step for usize}#43 : core::iter
     fn steps_between<'_0, '_1> = core::iter::range::{impl core::iter::range::Step for usize}#43::steps_between<'_0_0, '_0_1>
     fn forward_checked = core::iter::range::{impl core::iter::range::Step for usize}#43::forward_checked
     fn backward_checked = core::iter::range::{impl core::iter::range::Step for usize}#43::backward_checked
-    fn forward = core::iter::range::{impl core::iter::range::Step for usize}#43::forward
-    fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for usize}#43::forward_unchecked
-    fn backward = core::iter::range::{impl core::iter::range::Step for usize}#43::backward
-    fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for usize}#43::backward_unchecked
 }
 
 fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize
@@ -606,66 +396,33 @@ fn core::iter::range::Step::steps_between<'_0, '_1, Self>(@1: &'_0 (Self), @2: &
 
 fn core::iter::range::Step::forward_checked<Self>(@1: Self, @2: usize) -> core::option::Option<Self>[Self::parent_clause0]
 
-fn core::iter::range::Step::forward<Self>(@1: Self, @2: usize) -> Self
-
-unsafe fn core::iter::range::Step::forward_unchecked<Self>(@1: Self, @2: usize) -> Self
-
 fn core::iter::range::Step::backward_checked<Self>(@1: Self, @2: usize) -> core::option::Option<Self>[Self::parent_clause0]
 
-fn core::iter::range::Step::backward<Self>(@1: Self, @2: usize) -> Self
-
-unsafe fn core::iter::range::Step::backward_unchecked<Self>(@1: Self, @2: usize) -> Self
-
 fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
 
 fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> core::option::Option<core::cmp::Ordering>[core::marker::Sized<core::cmp::Ordering>]
 
-fn core::cmp::PartialOrd::lt<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::le<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::gt<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::PartialOrd::ge<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
 fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
 
-fn core::cmp::PartialEq::ne<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool
-
-fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::cmp::Ordering
-
-fn core::iter::traits::iterator::Iterator::size_hint<'_0, Self>(@1: &'_0 (Self)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-
-fn core::iter::traits::iterator::Iterator::count<Self>(@1: Self) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::nth<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::option::Option<Self::Item>[Self::parent_clause0]
-
-fn core::iter::traits::iterator::Iterator::last<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::min<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-    [@TraitClause1]: core::cmp::Ord<Self::Item>,
-
-fn core::iter::traits::iterator::Iterator::max<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-    [@TraitClause1]: core::cmp::Ord<Self::Item>,
+trait core::cmp::Eq<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::cmp::PartialEq<Self, Self>
+}
 
-fn core::iter::traits::iterator::Iterator::is_sorted<Self>(@1: Self) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-    [@TraitClause1]: core::cmp::PartialOrd<Self::Item, Self::Item>,
+trait core::cmp::Ord<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::cmp::Eq<Self>
+    parent_clause1 : [@TraitClause1]: core::cmp::PartialOrd<Self, Self>
+    fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>
+}
 
-fn core::iter::traits::iterator::Iterator::advance_by<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
+trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    const MAY_HAVE_SIDE_EFFECT : bool
+}
 
-unsafe fn core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> Self::Item
-where
-    [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>,
+fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::cmp::Ordering
 
 trait core::marker::Tuple<Self>
 
@@ -753,6 +510,11 @@ trait core::iter::traits::exact_size::ExactSizeIterator<Self>
     parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
 }
 
+trait core::marker::Copy<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
+}
+
 trait core::iter::traits::accum::Sum<Self, A>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out
index e05f1ff0..d5878631 100644
--- a/charon/tests/ui/unsize.out
+++ b/charon/tests/ui/unsize.out
@@ -118,19 +118,13 @@ trait core::clone::Clone<Self>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
     fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
-    fn clone_from<'_0, '_1> = core::clone::Clone::clone_from<'_0_0, '_0_1, Self>
 }
 
-fn alloc::string::{impl core::clone::Clone for alloc::string::String}#6::clone_from<'_0, '_1>(@1: &'_0 mut (alloc::string::String), @2: &'_1 (alloc::string::String))
-
 impl alloc::string::{impl core::clone::Clone for alloc::string::String}#6 : core::clone::Clone<alloc::string::String>
 {
     parent_clause0 = core::marker::Sized<alloc::string::String>
     fn clone<'_0> = alloc::string::{impl core::clone::Clone for alloc::string::String}#6::clone<'_0_0>
-    fn clone_from<'_0, '_1> = alloc::string::{impl core::clone::Clone for alloc::string::String}#6::clone_from<'_0_0, '_0_1>
 }
 
-fn core::clone::Clone::clone_from<'_0, '_1, Self>(@1: &'_0 mut (Self), @2: &'_1 (Self))
-
 
 
diff --git a/charon/tests/ui/unsupported/issue-79-bound-regions.out b/charon/tests/ui/unsupported/issue-79-bound-regions.out
index 0555b94f..1331a3ec 100644
--- a/charon/tests/ui/unsupported/issue-79-bound-regions.out
+++ b/charon/tests/ui/unsupported/issue-79-bound-regions.out
@@ -63,81 +63,38 @@ fn test_crate::main()
 
 fn core::iter::traits::iterator::Iterator::next<'_0, Self>(@1: &'_0 mut (Self)) -> core::option::Option<Self::Item>[Self::parent_clause0]
 
-enum core::result::Result<T, E>
-  where
-      [@TraitClause0]: core::marker::Sized<T>,
-      [@TraitClause1]: core::marker::Sized<E>,
- =
-|  Ok(T)
-|  Err(E)
-
-
-trait core::clone::Clone<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
-}
-
-trait core::marker::Copy<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
-}
-
-trait core::num::nonzero::private::Sealed<Self>
-
-trait core::num::nonzero::ZeroablePrimitive<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    parent_clause1 : [@TraitClause1]: core::marker::Copy<Self>
-    parent_clause2 : [@TraitClause2]: core::num::nonzero::private::Sealed<Self>
-    parent_clause3 : [@TraitClause3]: core::marker::Sized<Self::NonZeroInner>
-    parent_clause4 : [@TraitClause4]: core::marker::Copy<Self::NonZeroInner>
-    type NonZeroInner
-}
-
-opaque type core::num::nonzero::NonZero<T>
-  where
-      [@TraitClause0]: core::marker::Sized<T>,
-      [@TraitClause1]: core::num::nonzero::ZeroablePrimitive<T>,
-
-fn core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0>(@1: &'_0 (usize)) -> usize
-
-impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Clone<usize>
-{
-    parent_clause0 = core::marker::Sized<usize>
-    fn clone<'_0> = core::clone::impls::{impl core::clone::Clone for usize}#5::clone<'_0_0>
-}
-
-impl core::marker::{impl core::marker::Copy for usize}#37 : core::marker::Copy<usize>
+trait core::iter::traits::iterator::Iterator<Self>
 {
-    parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize}#5
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
+    type Item
+    fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
 }
 
-impl core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25 : core::num::nonzero::private::Sealed<usize>
-
-opaque type core::num::nonzero::private::NonZeroUsizeInner
-
-fn core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26::clone<'_0>(@1: &'_0 (core::num::nonzero::private::NonZeroUsizeInner)) -> core::num::nonzero::private::NonZeroUsizeInner
-
-impl core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26 : core::clone::Clone<core::num::nonzero::private::NonZeroUsizeInner>
+impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182<'a, T> : core::iter::traits::iterator::Iterator<core::slice::iter::Iter<'a, T>[@TraitClause0]>
+where
+    [@TraitClause0]: core::marker::Sized<T>,
 {
-    parent_clause0 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
-    fn clone<'_0> = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26::clone<'_0_0>
+    parent_clause0 = core::marker::Sized<&'_ (T)>
+    type Item = &'a (T)
+    fn next<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::next<'a, '_0_0, T>[@TraitClause0]
 }
 
-impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27 : core::marker::Copy<core::num::nonzero::private::NonZeroUsizeInner>
+trait core::iter::traits::collect::IntoIterator<Self>
+where
+    Self::parent_clause2::Item = Self::Item,
 {
-    parent_clause0 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
+    parent_clause1 : [@TraitClause1]: core::marker::Sized<Self::IntoIter>
+    parent_clause2 : [@TraitClause2]: core::iter::traits::iterator::Iterator<Self::IntoIter>
+    type Item
+    type IntoIter
+    fn into_iter = core::iter::traits::collect::IntoIterator::into_iter<Self>
 }
 
-impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26 : core::num::nonzero::ZeroablePrimitive<usize>
+trait core::clone::Clone<Self>
 {
-    parent_clause0 = core::marker::Sized<usize>
-    parent_clause1 = core::marker::{impl core::marker::Copy for usize}#37
-    parent_clause2 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25
-    parent_clause3 = core::marker::Sized<core::num::nonzero::private::NonZeroUsizeInner>
-    parent_clause4 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
-    type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>
 }
 
 trait core::marker::Tuple<Self>
@@ -159,201 +116,6 @@ trait core::ops::function::FnMut<Self, Args>
     fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args>
 }
 
-trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
-    const MAY_HAVE_SIDE_EFFECT : bool
-}
-
-trait core::iter::traits::iterator::Iterator<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
-    type Item
-    fn next<'_0> = core::iter::traits::iterator::Iterator::next<'_0_0, Self>
-    fn size_hint<'_0> = core::iter::traits::iterator::Iterator::size_hint<'_0_0, Self>
-    fn count<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::count<Self>[@TraitClause0_0]
-    fn last<[@TraitClause0]: core::marker::Sized<Self>> = core::iter::traits::iterator::Iterator::last<Self>[@TraitClause0_0]
-    fn advance_by<'_0> = core::iter::traits::iterator::Iterator::advance_by<'_0_0, Self>
-    fn nth<'_0> = core::iter::traits::iterator::Iterator::nth<'_0_0, Self>
-    fn for_each<F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>, @TraitClause1_2::parent_clause0::Output = ()> = core::iter::traits::iterator::Iterator::for_each<Self, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn fold<B, F, [@TraitClause0]: core::marker::Sized<B>, [@TraitClause1]: core::marker::Sized<F>, [@TraitClause2]: core::marker::Sized<Self>, [@TraitClause3]: core::ops::function::FnMut<F, (B, Self::Item)>, @TraitClause1_3::parent_clause0::Output = B> = core::iter::traits::iterator::Iterator::fold<Self, B, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3]
-    fn all<'_0, F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>, @TraitClause1_2::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::all<'_0_0, Self, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn any<'_0, F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>, @TraitClause1_2::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::any<'_0_0, Self, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn find<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: for<'_0> core::ops::function::FnMut<P, (&'_0_0 (Self::Item))>, for<'_0> @TraitClause1_2::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::find<'_0_0, Self, P>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn find_map<'_0, B, F, [@TraitClause0]: core::marker::Sized<B>, [@TraitClause1]: core::marker::Sized<F>, [@TraitClause2]: core::marker::Sized<Self>, [@TraitClause3]: core::ops::function::FnMut<F, (Self::Item)>, @TraitClause1_3::parent_clause0::Output = core::option::Option<B>[@TraitClause1_0]> = core::iter::traits::iterator::Iterator::find_map<'_0_0, Self, B, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3]
-    fn position<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: core::ops::function::FnMut<P, (Self::Item)>, @TraitClause1_2::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::position<'_0_0, Self, P>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn rposition<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::ops::function::FnMut<P, (Self::Item)>, [@TraitClause2]: core::marker::Sized<Self>, [@TraitClause3]: core::iter::traits::exact_size::ExactSizeIterator<Self>, [@TraitClause4]: core::iter::traits::double_ended::DoubleEndedIterator<Self>, @TraitClause1_1::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::rposition<'_0_0, Self, P>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4]
-    fn is_sorted_by<F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<Self>, [@TraitClause2]: for<'_0, '_1> core::ops::function::FnMut<F, (&'_0_0 (Self::Item), &'_0_1 (Self::Item))>, for<'_0, '_1> @TraitClause1_2::parent_clause0::Output = bool> = core::iter::traits::iterator::Iterator::is_sorted_by<Self, F>[@TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn __iterator_get_unchecked<'_0, [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>> = core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0_0, Self>[@TraitClause0_0]
-}
-
-trait core::iter::traits::exact_size::ExactSizeIterator<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
-}
-
-trait core::iter::traits::double_ended::DoubleEndedIterator<Self>
-{
-    parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
-    fn next_back<'_0> = core::iter::traits::double_ended::DoubleEndedIterator::next_back<'_0_0, Self>
-}
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::Iter<'a, T>[@TraitClause0])) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::count<'a, T>(@1: core::slice::iter::Iter<'a, T>[@TraitClause0]) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::last<'a, T>(@1: core::slice::iter::Iter<'a, T>[@TraitClause0]) -> core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::advance_by<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: usize) -> core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::for_each<'a, T, F>(@1: core::slice::iter::Iter<'a, T>[@TraitClause0], @2: F)
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (&'_ (T))>,
-    @TraitClause3::parent_clause0::Output = (),
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::fold<'a, T, B, F>(@1: core::slice::iter::Iter<'a, T>[@TraitClause0], @2: B, @3: F) -> B
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<B>,
-    [@TraitClause2]: core::marker::Sized<F>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (B, &'_ (T))>,
-    @TraitClause3::parent_clause0::Output = B,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::all<'a, '_1, T, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (&'_ (T))>,
-    @TraitClause3::parent_clause0::Output = bool,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::any<'a, '_1, T, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (&'_ (T))>,
-    @TraitClause3::parent_clause0::Output = bool,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: P) -> core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<P>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: for<'_0> core::ops::function::FnMut<P, (&'_0_0 (&'_ (T)))>,
-    for<'_0> @TraitClause3::parent_clause0::Output = bool,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find_map<'a, '_1, T, B, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: F) -> core::option::Option<B>[@TraitClause1]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<B>,
-    [@TraitClause2]: core::marker::Sized<F>,
-    [@TraitClause3]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause4]: core::ops::function::FnMut<F, (&'_ (T))>,
-    @TraitClause4::parent_clause0::Output = core::option::Option<B>[@TraitClause1],
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::position<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: P) -> core::option::Option<usize>[core::marker::Sized<usize>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<P>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: core::ops::function::FnMut<P, (&'_ (T))>,
-    @TraitClause3::parent_clause0::Output = bool,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::rposition<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: P) -> core::option::Option<usize>[core::marker::Sized<usize>]
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<P>,
-    [@TraitClause2]: core::ops::function::FnMut<P, (@TraitClause4::parent_clause0::Item)>,
-    [@TraitClause3]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause4]: core::iter::traits::exact_size::ExactSizeIterator<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause5]: core::iter::traits::double_ended::DoubleEndedIterator<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    @TraitClause2::parent_clause0::Output = bool,
-
-fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::is_sorted_by<'a, T, F>(@1: core::slice::iter::Iter<'a, T>[@TraitClause0], @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>,
-    [@TraitClause3]: for<'_0, '_1> core::ops::function::FnMut<F, (&'_0_0 (&'_ (T)), &'_0_1 (&'_ (T)))>,
-    for<'_0, '_1> @TraitClause3::parent_clause0::Output = bool,
-
-unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>[@TraitClause0]), @2: usize) -> &'_ (T)
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-
-impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182<'a, T> : core::iter::traits::iterator::Iterator<core::slice::iter::Iter<'a, T>[@TraitClause0]>
-where
-    [@TraitClause0]: core::marker::Sized<T>,
-{
-    parent_clause0 = core::marker::Sized<&'_ (T)>
-    type Item = &'a (T)
-    fn next<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::next<'a, '_0_0, T>[@TraitClause0]
-    fn size_hint<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::size_hint<'a, '_0_0, T>[@TraitClause0]
-    fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::count<'a, T>[@TraitClause0]
-    fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::last<'a, T>[@TraitClause0]
-    fn advance_by<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::advance_by<'a, '_0_0, T>[@TraitClause0]
-    fn nth<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::nth<'a, '_0_0, T>[@TraitClause0]
-    fn for_each<F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: core::ops::function::FnMut<F, (&'_ (T))>, @TraitClause1_2::parent_clause0::Output = ()> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::for_each<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn fold<B, F, [@TraitClause0]: core::marker::Sized<B>, [@TraitClause1]: core::marker::Sized<F>, [@TraitClause2]: core::ops::function::FnMut<F, (B, &'_ (T))>, @TraitClause1_2::parent_clause0::Output = B> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::fold<'a, T, B, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn all<'_0, F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: core::ops::function::FnMut<F, (&'_ (T))>, @TraitClause1_2::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::all<'a, '_0_0, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn any<'_0, F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: core::ops::function::FnMut<F, (&'_ (T))>, @TraitClause1_2::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::any<'a, '_0_0, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn find<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: for<'_0> core::ops::function::FnMut<P, (&'_0_0 (&'_ (T)))>, for<'_0> @TraitClause1_2::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn find_map<'_0, B, F, [@TraitClause0]: core::marker::Sized<B>, [@TraitClause1]: core::marker::Sized<F>, [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause3]: core::ops::function::FnMut<F, (&'_ (T))>, @TraitClause1_3::parent_clause0::Output = core::option::Option<B>[@TraitClause1_0]> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::find_map<'a, '_0_0, T, B, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3]
-    fn position<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: core::ops::function::FnMut<P, (&'_ (T))>, @TraitClause1_2::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::position<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn rposition<'_0, P, [@TraitClause0]: core::marker::Sized<P>, [@TraitClause1]: core::ops::function::FnMut<P, (@TraitClause1_3::parent_clause0::Item)>, [@TraitClause2]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause3]: core::iter::traits::exact_size::ExactSizeIterator<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause4]: core::iter::traits::double_ended::DoubleEndedIterator<core::slice::iter::Iter<'_, T>[@TraitClause0]>, @TraitClause1_1::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::rposition<'a, '_0_0, T, P>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2, @TraitClause0_3, @TraitClause0_4]
-    fn is_sorted_by<F, [@TraitClause0]: core::marker::Sized<F>, [@TraitClause1]: core::marker::Sized<core::slice::iter::Iter<'_, T>[@TraitClause0]>, [@TraitClause2]: for<'_0, '_1> core::ops::function::FnMut<F, (&'_0_0 (&'_ (T)), &'_0_1 (&'_ (T)))>, for<'_0, '_1> @TraitClause1_2::parent_clause0::Output = bool> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::is_sorted_by<'a, T, F>[@TraitClause0, @TraitClause0_0, @TraitClause0_1, @TraitClause0_2]
-    fn __iterator_get_unchecked<'_0> = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>[@TraitClause0]}#182::__iterator_get_unchecked<'a, '_0_0, T>[@TraitClause0]
-}
-
-fn core::iter::traits::iterator::Iterator::size_hint<'_0, Self>(@1: &'_0 (Self)) -> (usize, core::option::Option<usize>[core::marker::Sized<usize>])
-
-fn core::iter::traits::iterator::Iterator::count<Self>(@1: Self) -> usize
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::last<Self>(@1: Self) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<Self>,
-
-fn core::iter::traits::iterator::Iterator::advance_by<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>[core::marker::Sized<()>, core::marker::Sized<core::num::nonzero::NonZero<usize>[core::marker::Sized<usize>, core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26]>]
-
-fn core::iter::traits::iterator::Iterator::nth<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> core::option::Option<Self::Item>[Self::parent_clause0]
-
-trait core::iter::traits::collect::IntoIterator<Self>
-where
-    Self::parent_clause2::Item = Self::Item,
-{
-    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Item>
-    parent_clause1 : [@TraitClause1]: core::marker::Sized<Self::IntoIter>
-    parent_clause2 : [@TraitClause2]: core::iter::traits::iterator::Iterator<Self::IntoIter>
-    type Item
-    type IntoIter
-    fn into_iter = core::iter::traits::collect::IntoIterator::into_iter<Self>
-}
-
-fn core::iter::traits::iterator::Iterator::for_each<Self, F>(@1: Self, @2: F)
-where
-    [@TraitClause0]: core::marker::Sized<F>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>,
-    @TraitClause2::parent_clause0::Output = (),
-
 trait core::iter::traits::collect::FromIterator<Self, A>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
@@ -410,58 +172,16 @@ trait core::default::Default<Self>
     fn default = core::default::Default::default<Self>
 }
 
-fn core::iter::traits::iterator::Iterator::fold<Self, B, F>(@1: Self, @2: B, @3: F) -> B
-where
-    [@TraitClause0]: core::marker::Sized<B>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<Self>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (B, Self::Item)>,
-    @TraitClause3::parent_clause0::Output = B,
-
-fn core::iter::traits::iterator::Iterator::all<'_0, Self, F>(@1: &'_0 mut (Self), @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<F>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>,
-    @TraitClause2::parent_clause0::Output = bool,
-
-fn core::iter::traits::iterator::Iterator::any<'_0, Self, F>(@1: &'_0 mut (Self), @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<F>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: core::ops::function::FnMut<F, (Self::Item)>,
-    @TraitClause2::parent_clause0::Output = bool,
-
-fn core::iter::traits::iterator::Iterator::find<'_0, Self, P>(@1: &'_0 mut (Self), @2: P) -> core::option::Option<Self::Item>[Self::parent_clause0]
-where
-    [@TraitClause0]: core::marker::Sized<P>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: for<'_0> core::ops::function::FnMut<P, (&'_0_0 (Self::Item))>,
-    for<'_0> @TraitClause2::parent_clause0::Output = bool,
-
-fn core::iter::traits::iterator::Iterator::find_map<'_0, Self, B, F>(@1: &'_0 mut (Self), @2: F) -> core::option::Option<B>[@TraitClause0]
-where
-    [@TraitClause0]: core::marker::Sized<B>,
-    [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: core::marker::Sized<Self>,
-    [@TraitClause3]: core::ops::function::FnMut<F, (Self::Item)>,
-    @TraitClause3::parent_clause0::Output = core::option::Option<B>[@TraitClause0],
-
-fn core::iter::traits::iterator::Iterator::position<'_0, Self, P>(@1: &'_0 mut (Self), @2: P) -> core::option::Option<usize>[core::marker::Sized<usize>]
-where
-    [@TraitClause0]: core::marker::Sized<P>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: core::ops::function::FnMut<P, (Self::Item)>,
-    @TraitClause2::parent_clause0::Output = bool,
+trait core::iter::traits::double_ended::DoubleEndedIterator<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
+    fn next_back<'_0> = core::iter::traits::double_ended::DoubleEndedIterator::next_back<'_0_0, Self>
+}
 
-fn core::iter::traits::iterator::Iterator::rposition<'_0, Self, P>(@1: &'_0 mut (Self), @2: P) -> core::option::Option<usize>[core::marker::Sized<usize>]
-where
-    [@TraitClause0]: core::marker::Sized<P>,
-    [@TraitClause1]: core::ops::function::FnMut<P, (Self::Item)>,
-    [@TraitClause2]: core::marker::Sized<Self>,
-    [@TraitClause3]: core::iter::traits::exact_size::ExactSizeIterator<Self>,
-    [@TraitClause4]: core::iter::traits::double_ended::DoubleEndedIterator<Self>,
-    @TraitClause1::parent_clause0::Output = bool,
+trait core::iter::traits::exact_size::ExactSizeIterator<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::iter::traits::iterator::Iterator<Self>
+}
 
 trait core::cmp::PartialEq<Self, Rhs>
 {
@@ -492,6 +212,11 @@ trait core::cmp::Ord<Self>
     fn cmp<'_0, '_1> = core::cmp::Ord::cmp<'_0_0, '_0_1, Self>
 }
 
+trait core::marker::Copy<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::clone::Clone<Self>
+}
+
 trait core::iter::traits::accum::Sum<Self, A>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
@@ -506,16 +231,11 @@ trait core::iter::traits::accum::Product<Self, A>
     fn product<I, [@TraitClause0]: core::marker::Sized<I>, [@TraitClause1]: core::iter::traits::iterator::Iterator<I>, @TraitClause1_1::Item = A> = core::iter::traits::accum::Product::product<Self, A, I>[@TraitClause0_0, @TraitClause0_1]
 }
 
-fn core::iter::traits::iterator::Iterator::is_sorted_by<Self, F>(@1: Self, @2: F) -> bool
-where
-    [@TraitClause0]: core::marker::Sized<F>,
-    [@TraitClause1]: core::marker::Sized<Self>,
-    [@TraitClause2]: for<'_0, '_1> core::ops::function::FnMut<F, (&'_0_0 (Self::Item), &'_0_1 (Self::Item))>,
-    for<'_0, '_1> @TraitClause2::parent_clause0::Output = bool,
-
-unsafe fn core::iter::traits::iterator::Iterator::__iterator_get_unchecked<'_0, Self>(@1: &'_0 mut (Self), @2: usize) -> Self::Item
-where
-    [@TraitClause0]: core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>,
+trait core::iter::adapters::zip::TrustedRandomAccessNoCoerce<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self>
+    const MAY_HAVE_SIDE_EFFECT : bool
+}
 
 fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self