(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module iter.
  Module adapters.
    Module copied.
      (* StructRecord
        {
          name := "Copied";
          const_params := [];
          ty_params := [ "I" ];
          fields := [ ("it", I) ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_I_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        (* Clone *)
        Definition clone (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "core::iter::adapters::copied::Copied"
                [
                  ("it",
                    M.call_closure (|
                      M.get_trait_method (| "core::clone::Clone", I, [], "clone", [] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::copied::Copied",
                          "it"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::clone::Clone"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method (clone I)) ].
      End Impl_core_clone_Clone_where_core_clone_Clone_I_for_core_iter_adapters_copied_Copied_I.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_I_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        (* Debug *)
        Definition fmt (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_field1_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "Copied" |);
                  M.read (| Value.String "it" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::copied::Copied",
                      "it"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt I)) ].
      End Impl_core_fmt_Debug_where_core_fmt_Debug_I_for_core_iter_adapters_copied_Copied_I.
      
      Module Impl_core_iter_adapters_copied_Copied_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        (*
            pub(in crate::iter) fn new(it: I) -> Copied<I> {
                Copied { it }
            }
        *)
        Definition new (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ it ] =>
            ltac:(M.monadic
              (let it := M.alloc (| it |) in
              Value.StructRecord
                "core::iter::adapters::copied::Copied"
                [ ("it", M.read (| it |)) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (I : Ty.t),
          M.IsAssociatedFunction (Self I) "new" (new I).
      End Impl_core_iter_adapters_copied_Copied_I.
      
      (*
      fn copy_fold<T: Copy, Acc>(mut f: impl FnMut(Acc, T) -> Acc) -> impl FnMut(Acc, &T) -> Acc {
          move |acc, &elt| f(acc, elt)
      }
      *)
      Definition copy_fold (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; Acc; impl_FnMut_Acc__T__arrow_Acc ], [ f ] =>
          ltac:(M.monadic
            (let f := M.alloc (| f |) in
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0; α1 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let acc := M.copy (| γ |) in
                              M.match_operator (|
                                M.alloc (| α1 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ := M.read (| γ |) in
                                      let elt := M.copy (| γ |) in
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::function::FnMut",
                                          impl_FnMut_Acc__T__arrow_Acc,
                                          [ Ty.tuple [ Acc; T ] ],
                                          "call_mut",
                                          []
                                        |),
                                        [ f; Value.Tuple [ M.read (| acc |); M.read (| elt |) ] ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_copy_fold : M.IsFunction "core::iter::adapters::copied::copy_fold" copy_fold.
      
      Module copy_fold.
        (* Error OpaqueTy *)
      End copy_fold.
      
      (*
      fn copy_try_fold<T: Copy, Acc, R>(mut f: impl FnMut(Acc, T) -> R) -> impl FnMut(Acc, &T) -> R {
          move |acc, &elt| f(acc, elt)
      }
      *)
      Definition copy_try_fold (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; Acc; R; impl_FnMut_Acc__T__arrow_R ], [ f ] =>
          ltac:(M.monadic
            (let f := M.alloc (| f |) in
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0; α1 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let acc := M.copy (| γ |) in
                              M.match_operator (|
                                M.alloc (| α1 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ := M.read (| γ |) in
                                      let elt := M.copy (| γ |) in
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::function::FnMut",
                                          impl_FnMut_Acc__T__arrow_R,
                                          [ Ty.tuple [ Acc; T ] ],
                                          "call_mut",
                                          []
                                        |),
                                        [ f; Value.Tuple [ M.read (| acc |); M.read (| elt |) ] ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_copy_try_fold :
        M.IsFunction "core::iter::adapters::copied::copy_try_fold" copy_try_fold.
      
      Module copy_try_fold.
        (* Error OpaqueTy *)
      End copy_try_fold.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_where_core_marker_Copy_T_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        (*     type Item = T; *)
        Definition _Item (I T : Ty.t) : Ty.t := T.
        
        (*
            fn next(&mut self) -> Option<T> {
                self.it.next().copied()
            }
        *)
        Definition next (I T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ],
                  "copied",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      I,
                      [],
                      "next",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::adapters::copied::Copied",
                        "it"
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn next_chunk<const N: usize>(
                &mut self,
            ) -> Result<[Self::Item; N], array::IntoIter<Self::Item, N>>
            where
                Self: Sized,
            {
                <I as SpecNextChunk<'_, N, T>>::spec_next_chunk(&mut self.it)
            }
        *)
        Definition next_chunk
            (I T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [ N ], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::adapters::copied::SpecNextChunk",
                  I,
                  [ T ],
                  "spec_next_chunk",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::copied::Copied",
                    "it"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                self.it.size_hint()
            }
        *)
        Definition size_hint
            (I T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "size_hint",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::copied::Copied",
                    "it"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_fold<B, F, R>(&mut self, init: B, f: F) -> R
            where
                Self: Sized,
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                self.it.try_fold(init, copy_try_fold(f))
            }
        *)
        Definition try_fold
            (I T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [ B; F; R ], [ self; init; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "try_fold",
                  [ B; Ty.associated; R ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::copied::Copied",
                    "it"
                  |);
                  M.read (| init |);
                  M.call_closure (|
                    M.get_function (|
                      "core::iter::adapters::copied::copy_try_fold",
                      [ T; B; R; F ]
                    |),
                    [ M.read (| f |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn fold<Acc, F>(self, init: Acc, f: F) -> Acc
            where
                F: FnMut(Acc, Self::Item) -> Acc,
            {
                self.it.fold(init, copy_fold(f))
            }
        *)
        Definition fold (I T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [ Acc; F ], [ self; init; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "fold",
                  [ Acc; Ty.associated ]
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::copied::Copied",
                      "it"
                    |)
                  |);
                  M.read (| init |);
                  M.call_closure (|
                    M.get_function (| "core::iter::adapters::copied::copy_fold", [ T; Acc; F ] |),
                    [ M.read (| f |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth(&mut self, n: usize) -> Option<T> {
                self.it.nth(n).copied()
            }
        *)
        Definition nth (I T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ],
                  "copied",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      I,
                      [],
                      "nth",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::adapters::copied::Copied",
                        "it"
                      |);
                      M.read (| n |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn last(self) -> Option<T> {
                self.it.last().copied()
            }
        *)
        Definition last (I T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ],
                  "copied",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      I,
                      [],
                      "last",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::iter::adapters::copied::Copied",
                          "it"
                        |)
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn count(self) -> usize {
                self.it.count()
            }
        *)
        Definition count (I T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "count",
                  []
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::copied::Copied",
                      "it"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                self.it.advance_by(n)
            }
        *)
        Definition advance_by
            (I T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  I,
                  [],
                  "advance_by",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::copied::Copied",
                    "it"
                  |);
                  M.read (| n |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> T
            where
                Self: TrustedRandomAccessNoCoerce,
            {
                // SAFETY: the caller must uphold the contract for
                // `Iterator::__iterator_get_unchecked`.
                *unsafe { try_get_unchecked(&mut self.it, idx) }
            }
        *)
        Definition __iterator_get_unchecked
            (I T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self; idx ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let idx := M.alloc (| idx |) in
              M.read (|
                M.call_closure (|
                  M.get_function (| "core::iter::adapters::zip::try_get_unchecked", [ I ] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::copied::Copied",
                      "it"
                    |);
                    M.read (| idx |)
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self I T)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item I T));
              ("next", InstanceField.Method (next I T));
              ("next_chunk", InstanceField.Method (next_chunk I T));
              ("size_hint", InstanceField.Method (size_hint I T));
              ("try_fold", InstanceField.Method (try_fold I T));
              ("fold", InstanceField.Method (fold I T));
              ("nth", InstanceField.Method (nth I T));
              ("last", InstanceField.Method (last I T));
              ("count", InstanceField.Method (count I T));
              ("advance_by", InstanceField.Method (advance_by I T));
              ("__iterator_get_unchecked", InstanceField.Method (__iterator_get_unchecked I T))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_where_core_marker_Copy_T_for_core_iter_adapters_copied_Copied_I.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_where_core_marker_Copy_T_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        (*
            fn next_back(&mut self) -> Option<T> {
                self.it.next_back().copied()
            }
        *)
        Definition next_back
            (I T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ],
                  "copied",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::double_ended::DoubleEndedIterator",
                      I,
                      [],
                      "next_back",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::iter::adapters::copied::Copied",
                        "it"
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_rfold<B, F, R>(&mut self, init: B, f: F) -> R
            where
                Self: Sized,
                F: FnMut(B, Self::Item) -> R,
                R: Try<Output = B>,
            {
                self.it.try_rfold(init, copy_try_fold(f))
            }
        *)
        Definition try_rfold
            (I T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [ B; F; R ], [ self; init; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "try_rfold",
                  [ B; Ty.associated; R ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::copied::Copied",
                    "it"
                  |);
                  M.read (| init |);
                  M.call_closure (|
                    M.get_function (|
                      "core::iter::adapters::copied::copy_try_fold",
                      [ T; B; R; F ]
                    |),
                    [ M.read (| f |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfold<Acc, F>(self, init: Acc, f: F) -> Acc
            where
                F: FnMut(Acc, Self::Item) -> Acc,
            {
                self.it.rfold(init, copy_fold(f))
            }
        *)
        Definition rfold (I T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [ Acc; F ], [ self; init; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let init := M.alloc (| init |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "rfold",
                  [ Acc; Ty.associated ]
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "core::iter::adapters::copied::Copied",
                      "it"
                    |)
                  |);
                  M.read (| init |);
                  M.call_closure (|
                    M.get_function (| "core::iter::adapters::copied::copy_fold", [ T; Acc; F ] |),
                    [ M.read (| f |) ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
                self.it.advance_back_by(n)
            }
        *)
        Definition advance_back_by
            (I T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::double_ended::DoubleEndedIterator",
                  I,
                  [],
                  "advance_back_by",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::copied::Copied",
                    "it"
                  |);
                  M.read (| n |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIterator"
            (Self I T)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("next_back", InstanceField.Method (next_back I T));
              ("try_rfold", InstanceField.Method (try_rfold I T));
              ("rfold", InstanceField.Method (rfold I T));
              ("advance_back_by", InstanceField.Method (advance_back_by I T))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_where_core_marker_Copy_T_for_core_iter_adapters_copied_Copied_I.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_where_core_marker_Copy_T_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        (*
            fn len(&self) -> usize {
                self.it.len()
            }
        *)
        Definition len (I T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::exact_size::ExactSizeIterator",
                  I,
                  [],
                  "len",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::copied::Copied",
                    "it"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn is_empty(&self) -> bool {
                self.it.is_empty()
            }
        *)
        Definition is_empty
            (I T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::exact_size::ExactSizeIterator",
                  I,
                  [],
                  "is_empty",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::copied::Copied",
                    "it"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self I T)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("len", InstanceField.Method (len I T));
              ("is_empty", InstanceField.Method (is_empty I T))
            ].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_where_core_marker_Copy_T_for_core_iter_adapters_copied_Copied_I.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_marker_FusedIterator_I_where_core_marker_Copy_T_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        Axiom Implements :
          forall (I T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self I T)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_marker_FusedIterator_I_where_core_marker_Copy_T_for_core_iter_adapters_copied_Copied_I.
      
      Module Impl_core_iter_adapters_zip_TrustedRandomAccess_where_core_iter_adapters_zip_TrustedRandomAccess_I_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::zip::TrustedRandomAccess"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_adapters_zip_TrustedRandomAccess_where_core_iter_adapters_zip_TrustedRandomAccess_I_for_core_iter_adapters_copied_Copied_I.
      
      Module Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_where_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_I_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        (*     const MAY_HAVE_SIDE_EFFECT: bool = I::MAY_HAVE_SIDE_EFFECT; *)
        (* Ty.path "bool" *)
        Definition value_MAY_HAVE_SIDE_EFFECT (I : Ty.t) : Value.t :=
          let Self : Ty.t := Self I in
          M.run
            ltac:(M.monadic
              (M.get_constant (|
                "core::iter::adapters::zip::TrustedRandomAccessNoCoerce::MAY_HAVE_SIDE_EFFECT"
              |))).
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::zip::TrustedRandomAccessNoCoerce"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("value_MAY_HAVE_SIDE_EFFECT", InstanceField.Constant (value_MAY_HAVE_SIDE_EFFECT I))
            ].
      End Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_where_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_I_for_core_iter_adapters_copied_Copied_I.
      
      Module Impl_core_iter_traits_marker_TrustedLen_where_core_iter_traits_marker_TrustedLen_I_where_core_marker_Copy_T_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        Axiom Implements :
          forall (I T : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::TrustedLen"
            (Self I T)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_TrustedLen_where_core_iter_traits_marker_TrustedLen_I_where_core_marker_Copy_T_for_core_iter_adapters_copied_Copied_I.
      
      (* Trait *)
      (* Empty module 'SpecNextChunk' *)
      
      Module Impl_core_iter_adapters_copied_SpecNextChunk_where_core_iter_traits_iterator_Iterator_I_where_core_marker_Copy_T_T_for_I.
        Definition Self (N : Value.t) (I T : Ty.t) : Ty.t := I.
        
        (*
            default fn spec_next_chunk(&mut self) -> Result<[T; N], array::IntoIter<T, N>> {
                array::iter_next_chunk(&mut self.copied())
            }
        *)
        Definition spec_next_chunk
            (N : Value.t)
            (I T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self N I T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_function (|
                  "core::array::iter_next_chunk",
                  [
                    T;
                    Ty.apply
                      (Ty.path "core::iter::adapters::copied::Copied")
                      []
                      [ Ty.apply (Ty.path "&mut") [] [ I ] ]
                  ]
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "&mut") [] [ I ],
                        [],
                        "copied",
                        [ T ]
                      |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (N : Value.t) (I T : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::copied::SpecNextChunk"
            (Self N I T)
            (* Trait polymorphic types *) [ (* T *) T ]
            (* Instance *) [ ("spec_next_chunk", InstanceField.Method (spec_next_chunk N I T)) ].
      End Impl_core_iter_adapters_copied_SpecNextChunk_where_core_iter_traits_iterator_Iterator_I_where_core_marker_Copy_T_T_for_I.
      
      Module Impl_core_iter_adapters_copied_SpecNextChunk_where_core_marker_Copy_T_T_for_core_slice_iter_Iter_T.
        Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ].
        
        (*
            fn spec_next_chunk(&mut self) -> Result<[T; N], array::IntoIter<T, N>> {
                let mut raw_array = [const { MaybeUninit::uninit() }; N];
        
                let len = self.len();
        
                if T::IS_ZST {
                    if len < N {
                        let _ = self.advance_by(len);
                        // SAFETY: ZSTs can be conjured ex nihilo; only the amount has to be correct
                        return Err(unsafe { array::IntoIter::new_unchecked(raw_array, 0..len) });
                    }
        
                    let _ = self.advance_by(N);
                    // SAFETY: ditto
                    return Ok(unsafe { MaybeUninit::array_assume_init(raw_array) });
                }
        
                if len < N {
                    // SAFETY: `len` indicates that this many elements are available and we just checked that
                    // it fits into the array.
                    unsafe {
                        ptr::copy_nonoverlapping(
                            self.as_ref().as_ptr(),
                            raw_array.as_mut_ptr() as *mut T,
                            len,
                        );
                        let _ = self.advance_by(len);
                        return Err(array::IntoIter::new_unchecked(raw_array, 0..len));
                    }
                }
        
                // SAFETY: `len` is larger than the array size. Copy a fixed amount here to fully initialize
                // the array.
                unsafe {
                    ptr::copy_nonoverlapping(self.as_ref().as_ptr(), raw_array.as_mut_ptr() as *mut T, N);
                    let _ = self.advance_by(N);
                    Ok(MaybeUninit::array_assume_init(raw_array))
                }
            }
        *)
        Definition spec_next_chunk
            (N : Value.t)
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self N T in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ raw_array :=
                      M.alloc (|
                        repeat (|
                          M.read (|
                            M.get_constant (|
                              "core::iter::adapters::copied::spec_next_chunk_discriminant"
                            |)
                          |),
                          N
                        |)
                      |) in
                    let~ len :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::exact_size::ExactSizeIterator",
                            Ty.apply
                              (Ty.path "&mut")
                              []
                              [ Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ] ],
                            [],
                            "len",
                            []
                          |),
                          [ self ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.get_constant (| "core::mem::SizedTypeProperties::IS_ZST" |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    BinOp.lt (|
                                                      M.read (| len |),
                                                      M.read (|
                                                        M.get_constant (|
                                                          "core::iter::adapters::copied::N"
                                                        |)
                                                      |)
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::iter::traits::iterator::Iterator",
                                                            Ty.apply
                                                              (Ty.path "core::slice::iter::Iter")
                                                              []
                                                              [ T ],
                                                            [],
                                                            "advance_by",
                                                            []
                                                          |),
                                                          [ M.read (| self |); M.read (| len |) ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.return_ (|
                                                              Value.StructTuple
                                                                "core::result::Result::Err"
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::array::iter::IntoIter")
                                                                        [ N ]
                                                                        [ T ],
                                                                      "new_unchecked",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.read (| raw_array |);
                                                                      Value.StructRecord
                                                                        "core::ops::range::Range"
                                                                        [
                                                                          ("start",
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              0);
                                                                          ("end_", M.read (| len |))
                                                                        ]
                                                                    ]
                                                                  |)
                                                                ]
                                                            |)))
                                                      ]
                                                    |)
                                                  |)
                                                |)
                                              |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                            [],
                                            "advance_by",
                                            []
                                          |),
                                          [
                                            M.read (| self |);
                                            M.read (|
                                              M.get_constant (| "core::iter::adapters::copied::N" |)
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.return_ (|
                                              Value.StructTuple
                                                "core::result::Result::Ok"
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path
                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                        []
                                                        [ T ],
                                                      "array_assume_init",
                                                      []
                                                    |),
                                                    [ M.read (| raw_array |) ]
                                                  |)
                                                ]
                                            |)))
                                      ]
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.lt (|
                                      M.read (| len |),
                                      M.read (|
                                        M.get_constant (| "core::iter::adapters::copied::N" |)
                                      |)
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_function (|
                                            "core::intrinsics::copy_nonoverlapping",
                                            [ T ]
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "slice") [] [ T ],
                                                "as_ptr",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::convert::AsRef",
                                                    Ty.apply
                                                      (Ty.path "&mut")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "core::slice::iter::Iter")
                                                          []
                                                          [ T ]
                                                      ],
                                                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                                    "as_ref",
                                                    []
                                                  |),
                                                  [ self ]
                                                |)
                                              ]
                                            |);
                                            M.rust_cast
                                              (M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "slice")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path
                                                          "core::mem::maybe_uninit::MaybeUninit")
                                                        []
                                                        [ T ]
                                                    ],
                                                  "as_mut_ptr",
                                                  []
                                                |),
                                                [ raw_array ]
                                              |));
                                            M.read (| len |)
                                          ]
                                        |)
                                      |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                                            [],
                                            "advance_by",
                                            []
                                          |),
                                          [ M.read (| self |); M.read (| len |) ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.return_ (|
                                              Value.StructTuple
                                                "core::result::Result::Err"
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "core::array::iter::IntoIter")
                                                        [ N ]
                                                        [ T ],
                                                      "new_unchecked",
                                                      []
                                                    |),
                                                    [
                                                      M.read (| raw_array |);
                                                      Value.StructRecord
                                                        "core::ops::range::Range"
                                                        [
                                                          ("start",
                                                            Value.Integer IntegerKind.Usize 0);
                                                          ("end_", M.read (| len |))
                                                        ]
                                                    ]
                                                  |)
                                                ]
                                            |)))
                                      ]
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (| "core::intrinsics::copy_nonoverlapping", [ T ] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ T ],
                                "as_ptr",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::AsRef",
                                    Ty.apply
                                      (Ty.path "&mut")
                                      []
                                      [ Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ] ],
                                    [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                    "as_ref",
                                    []
                                  |),
                                  [ self ]
                                |)
                              ]
                            |);
                            M.rust_cast
                              (M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                        []
                                        [ T ]
                                    ],
                                  "as_mut_ptr",
                                  []
                                |),
                                [ raw_array ]
                              |));
                            M.read (| M.get_constant (| "core::iter::adapters::copied::N" |) |)
                          ]
                        |)
                      |) in
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                            [],
                            "advance_by",
                            []
                          |),
                          [
                            M.read (| self |);
                            M.read (| M.get_constant (| "core::iter::adapters::copied::N" |) |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              Value.StructTuple
                                "core::result::Result::Ok"
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                        []
                                        [ T ],
                                      "array_assume_init",
                                      []
                                    |),
                                    [ M.read (| raw_array |) ]
                                  |)
                                ]
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (N : Value.t) (T : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::copied::SpecNextChunk"
            (Self N T)
            (* Trait polymorphic types *) [ (* T *) T ]
            (* Instance *) [ ("spec_next_chunk", InstanceField.Method (spec_next_chunk N T)) ].
      End Impl_core_iter_adapters_copied_SpecNextChunk_where_core_marker_Copy_T_T_for_core_slice_iter_Iter_T.
      
      Module Impl_core_default_Default_where_core_default_Default_I_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        (*
            fn default() -> Self {
                Self::new(Default::default())
            }
        *)
        Definition default (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ],
                  "new",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", I, [], "default", [] |),
                    []
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::default::Default"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method (default I)) ].
      End Impl_core_default_Default_where_core_default_Default_I_for_core_iter_adapters_copied_Copied_I.
      
      Module Impl_core_iter_adapters_SourceIter_where_core_iter_adapters_SourceIter_I_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        (*     type Source = I::Source; *)
        Definition _Source (I : Ty.t) : Ty.t := Ty.associated.
        
        (*
            unsafe fn as_inner(&mut self) -> &mut I::Source {
                // SAFETY: unsafe function forwarding to unsafe function with the same requirements
                unsafe { SourceIter::as_inner(&mut self.it) }
            }
        *)
        Definition as_inner (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (| "core::iter::adapters::SourceIter", I, [], "as_inner", [] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::copied::Copied",
                    "it"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::SourceIter"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Source", InstanceField.Ty (_Source I));
              ("as_inner", InstanceField.Method (as_inner I))
            ].
      End Impl_core_iter_adapters_SourceIter_where_core_iter_adapters_SourceIter_I_for_core_iter_adapters_copied_Copied_I.
      
      Module Impl_core_iter_traits_marker_InPlaceIterable_where_core_iter_traits_marker_InPlaceIterable_I_for_core_iter_adapters_copied_Copied_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::copied::Copied") [] [ I ].
        
        (*     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY; *)
        (* Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ] *)
        Definition value_EXPAND_BY (I : Ty.t) : Value.t :=
          let Self : Ty.t := Self I in
          M.run
            ltac:(M.monadic
              (M.get_constant (| "core::iter::traits::marker::InPlaceIterable::EXPAND_BY" |))).
        
        (*     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY; *)
        (* Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ] *)
        Definition value_MERGE_BY (I : Ty.t) : Value.t :=
          let Self : Ty.t := Self I in
          M.run
            ltac:(M.monadic
              (M.get_constant (| "core::iter::traits::marker::InPlaceIterable::MERGE_BY" |))).
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::InPlaceIterable"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("value_EXPAND_BY", InstanceField.Constant (value_EXPAND_BY I));
              ("value_MERGE_BY", InstanceField.Constant (value_MERGE_BY I))
            ].
      End Impl_core_iter_traits_marker_InPlaceIterable_where_core_iter_traits_marker_InPlaceIterable_I_for_core_iter_adapters_copied_Copied_I.
    End copied.
  End adapters.
End iter.
