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

Module vec.
  Module into_iter.
    (* StructRecord
      {
        name := "IntoIter";
        const_params := [];
        ty_params := [ "T"; "A" ];
        fields :=
          [
            ("buf", Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]);
            ("phantom", Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ]);
            ("cap", Ty.path "usize");
            ("alloc", Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ A ]);
            ("ptr", Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]);
            ("end_", Ty.apply (Ty.path "*const") [] [ T ])
          ];
      } *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.debug_tuple("IntoIter").field(&self.as_slice()).finish()
          }
      *)
      Definition fmt (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A 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::builders::DebugTuple",
                "finish",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugTuple",
                    "field",
                    []
                  |),
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "IntoIter" |) ]
                      |)
                    |);
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ],
                          "as_slice",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt T A)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*
          pub fn as_slice(&self) -> &[T] {
              unsafe { slice::from_raw_parts(self.ptr.as_ptr(), self.len()) }
          }
      *)
      Definition as_slice (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::slice::raw::from_raw_parts", [ T ] |),
              [
                (* MutToConstPointer *)
                M.pointer_coercion
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::vec::into_iter::IntoIter",
                          "ptr"
                        |)
                      |)
                    ]
                  |));
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::exact_size::ExactSizeIterator",
                    Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ],
                    [],
                    "len",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_slice :
        forall (T A : Ty.t),
        M.IsAssociatedFunction (Self T A) "as_slice" (as_slice T A).
      
      (*
          pub fn as_mut_slice(&mut self) -> &mut [T] {
              unsafe { &mut *self.as_raw_mut_slice() }
          }
      *)
      Definition as_mut_slice
          (T A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ],
                "as_raw_mut_slice",
                []
              |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_mut_slice :
        forall (T A : Ty.t),
        M.IsAssociatedFunction (Self T A) "as_mut_slice" (as_mut_slice T A).
      
      (*
          pub fn allocator(&self) -> &A {
              &self.alloc
          }
      *)
      Definition allocator (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::deref::Deref",
                Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ A ],
                [],
                "deref",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "alloc::vec::into_iter::IntoIter",
                  "alloc"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_allocator :
        forall (T A : Ty.t),
        M.IsAssociatedFunction (Self T A) "allocator" (allocator T A).
      
      (*
          fn as_raw_mut_slice(&mut self) -> *mut [T] {
              ptr::slice_from_raw_parts_mut(self.ptr.as_ptr(), self.len())
          }
      *)
      Definition as_raw_mut_slice
          (T A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ T ] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "as_ptr",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::vec::into_iter::IntoIter",
                        "ptr"
                      |)
                    |)
                  ]
                |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::exact_size::ExactSizeIterator",
                    Ty.apply
                      (Ty.path "&mut")
                      []
                      [ Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ] ],
                    [],
                    "len",
                    []
                  |),
                  [ self ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_raw_mut_slice :
        forall (T A : Ty.t),
        M.IsAssociatedFunction (Self T A) "as_raw_mut_slice" (as_raw_mut_slice T A).
      
      (*
          pub(super) fn forget_allocation_drop_remaining(&mut self) {
              let remaining = self.as_raw_mut_slice();
      
              // overwrite the individual fields instead of creating a new
              // struct and then overwriting &mut self.
              // this creates less assembly
              self.cap = 0;
              self.buf = RawVec::new().non_null();
              self.ptr = self.buf;
              self.end = self.buf.as_ptr();
      
              // Dropping the remaining elements can panic, so this needs to be
              // done only after updating the other fields.
              unsafe {
                  ptr::drop_in_place(remaining);
              }
          }
      *)
      Definition forget_allocation_drop_remaining
          (T A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ remaining :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ],
                      "as_raw_mut_slice",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "alloc::vec::into_iter::IntoIter",
                    "cap"
                  |),
                  Value.Integer IntegerKind.Usize 0
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "alloc::vec::into_iter::IntoIter",
                    "buf"
                  |),
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "alloc::raw_vec::RawVec")
                        []
                        [ T; Ty.path "alloc::alloc::Global" ],
                      "non_null",
                      []
                    |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::raw_vec::RawVec")
                              []
                              [ T; Ty.path "alloc::alloc::Global" ],
                            "new",
                            []
                          |),
                          []
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "alloc::vec::into_iter::IntoIter",
                    "ptr"
                  |),
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "alloc::vec::into_iter::IntoIter",
                      "buf"
                    |)
                  |)
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "alloc::vec::into_iter::IntoIter",
                    "end"
                  |),
                  (* MutToConstPointer *)
                  M.pointer_coercion
                    (M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                        "as_ptr",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "alloc::vec::into_iter::IntoIter",
                            "buf"
                          |)
                        |)
                      ]
                    |))
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::ptr::drop_in_place",
                      [ Ty.apply (Ty.path "slice") [] [ T ] ]
                    |),
                    [ M.read (| remaining |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_forget_allocation_drop_remaining :
        forall (T A : Ty.t),
        M.IsAssociatedFunction
          (Self T A)
          "forget_allocation_drop_remaining"
          (forget_allocation_drop_remaining T A).
      
      (*
          pub(crate) fn forget_remaining_elements(&mut self) {
              // For the ZST case, it is crucial that we mutate `end` here, not `ptr`.
              // `ptr` must stay aligned, while `end` may be unaligned.
              self.end = self.ptr.as_ptr();
          }
      *)
      Definition forget_remaining_elements
          (T A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "alloc::vec::into_iter::IntoIter",
                    "end"
                  |),
                  (* MutToConstPointer *)
                  M.pointer_coercion
                    (M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                        "as_ptr",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "alloc::vec::into_iter::IntoIter",
                            "ptr"
                          |)
                        |)
                      ]
                    |))
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_forget_remaining_elements :
        forall (T A : Ty.t),
        M.IsAssociatedFunction
          (Self T A)
          "forget_remaining_elements"
          (forget_remaining_elements T A).
      
      (*
          pub(crate) fn into_vecdeque(self) -> VecDeque<T, A> {
              // Keep our `Drop` impl from dropping the elements and the allocator
              let mut this = ManuallyDrop::new(self);
      
              // SAFETY: This allocation originally came from a `Vec`, so it passes
              // all those checks. We have `this.buf` ≤ `this.ptr` ≤ `this.end`,
              // so the `sub_ptr`s below cannot wrap, and will produce a well-formed
              // range. `end` ≤ `buf + cap`, so the range will be in-bounds.
              // Taking `alloc` is ok because nothing else is going to look at it,
              // since our `Drop` impl isn't going to run so there's no more code.
              unsafe {
                  let buf = this.buf.as_ptr();
                  let initialized = if T::IS_ZST {
                      // All the pointers are the same for ZSTs, so it's fine to
                      // say that they're all at the beginning of the "allocation".
                      0..this.len()
                  } else {
                      this.ptr.sub_ptr(this.buf)..this.end.sub_ptr(buf)
                  };
                  let cap = this.cap;
                  let alloc = ManuallyDrop::take(&mut this.alloc);
                  VecDeque::from_contiguous_raw_parts_in(buf, initialized, cap, alloc)
              }
          }
      *)
      Definition into_vecdeque
          (T A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ this :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::mem::manually_drop::ManuallyDrop")
                        []
                        [ Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ] ],
                      "new",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ buf :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                      "as_ptr",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.apply
                                (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                []
                                [ Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ]
                                ],
                              [],
                              "deref",
                              []
                            |),
                            [ this ]
                          |),
                          "alloc::vec::into_iter::IntoIter",
                          "buf"
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ initialized :=
                M.copy (|
                  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 (|
                            Value.StructRecord
                              "core::ops::range::Range"
                              [
                                ("start", Value.Integer IntegerKind.Usize 0);
                                ("end_",
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::exact_size::ExactSizeIterator",
                                      Ty.apply
                                        (Ty.path "alloc::vec::into_iter::IntoIter")
                                        []
                                        [ T; A ],
                                      [],
                                      "len",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::deref::Deref",
                                          Ty.apply
                                            (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "alloc::vec::into_iter::IntoIter")
                                                []
                                                [ T; A ]
                                            ],
                                          [],
                                          "deref",
                                          []
                                        |),
                                        [ this ]
                                      |)
                                    ]
                                  |))
                              ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            Value.StructRecord
                              "core::ops::range::Range"
                              [
                                ("start",
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                      "sub_ptr",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::deref::Deref",
                                              Ty.apply
                                                (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::into_iter::IntoIter")
                                                    []
                                                    [ T; A ]
                                                ],
                                              [],
                                              "deref",
                                              []
                                            |),
                                            [ this ]
                                          |),
                                          "alloc::vec::into_iter::IntoIter",
                                          "ptr"
                                        |)
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::deref::Deref",
                                              Ty.apply
                                                (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::into_iter::IntoIter")
                                                    []
                                                    [ T; A ]
                                                ],
                                              [],
                                              "deref",
                                              []
                                            |),
                                            [ this ]
                                          |),
                                          "alloc::vec::into_iter::IntoIter",
                                          "buf"
                                        |)
                                      |)
                                    ]
                                  |));
                                ("end_",
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "sub_ptr",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::deref::Deref",
                                              Ty.apply
                                                (Ty.path "core::mem::manually_drop::ManuallyDrop")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::into_iter::IntoIter")
                                                    []
                                                    [ T; A ]
                                                ],
                                              [],
                                              "deref",
                                              []
                                            |),
                                            [ this ]
                                          |),
                                          "alloc::vec::into_iter::IntoIter",
                                          "end"
                                        |)
                                      |);
                                      (* MutToConstPointer *) M.pointer_coercion (M.read (| buf |))
                                    ]
                                  |))
                              ]
                          |)))
                    ]
                  |)
                |) in
              let~ cap :=
                M.copy (|
                  M.SubPointer.get_struct_record_field (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply
                          (Ty.path "core::mem::manually_drop::ManuallyDrop")
                          []
                          [ Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ] ],
                        [],
                        "deref",
                        []
                      |),
                      [ this ]
                    |),
                    "alloc::vec::into_iter::IntoIter",
                    "cap"
                  |)
                |) in
              let~ alloc :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ A ],
                      "take",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::DerefMut",
                            Ty.apply
                              (Ty.path "core::mem::manually_drop::ManuallyDrop")
                              []
                              [ Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ] ],
                            [],
                            "deref_mut",
                            []
                          |),
                          [ this ]
                        |),
                        "alloc::vec::into_iter::IntoIter",
                        "alloc"
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                    "from_contiguous_raw_parts_in",
                    []
                  |),
                  [ M.read (| buf |); M.read (| initialized |); M.read (| cap |); M.read (| alloc |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_into_vecdeque :
        forall (T A : Ty.t),
        M.IsAssociatedFunction (Self T A) "into_vecdeque" (into_vecdeque T A).
    End Impl_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_convert_AsRef_where_core_alloc_Allocator_A_slice_T_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*
          fn as_ref(&self) -> &[T] {
              self.as_slice()
          }
      *)
      Definition as_ref (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ],
                "as_slice",
                []
              |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::convert::AsRef"
          (Self T A)
          (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
          (* Instance *) [ ("as_ref", InstanceField.Method (as_ref T A)) ].
    End Impl_core_convert_AsRef_where_core_alloc_Allocator_A_slice_T_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_marker_Send_where_core_marker_Send_T_where_core_alloc_Allocator_A_where_core_marker_Send_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::marker::Send"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Send_where_core_marker_Send_T_where_core_alloc_Allocator_A_where_core_marker_Send_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_marker_Sync_where_core_marker_Sync_T_where_core_alloc_Allocator_A_where_core_marker_Sync_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::marker::Sync"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Sync_where_core_marker_Sync_T_where_core_alloc_Allocator_A_where_core_marker_Sync_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_iter_traits_iterator_Iterator_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*     type Item = T; *)
      Definition _Item (T A : Ty.t) : Ty.t := T.
      
      (*
          fn next(&mut self) -> Option<T> {
              let ptr = if T::IS_ZST {
                  if self.ptr.as_ptr() == self.end as *mut T {
                      return None;
                  }
                  // `ptr` has to stay where it is to remain aligned, so we reduce the length by 1 by
                  // reducing the `end`.
                  self.end = self.end.wrapping_byte_sub(1);
                  self.ptr
              } else {
                  if self.ptr == non_null!(self.end, T) {
                      return None;
                  }
                  let old = self.ptr;
                  self.ptr = unsafe { old.add(1) };
                  old
              };
              Some(unsafe { ptr.read() })
          }
      *)
      Definition next (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ ptr :=
                    M.copy (|
                      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
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.eq (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::ptr::non_null::NonNull")
                                                      []
                                                      [ T ],
                                                    "as_ptr",
                                                    []
                                                  |),
                                                  [
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "alloc::vec::into_iter::IntoIter",
                                                        "ptr"
                                                      |)
                                                    |)
                                                  ]
                                                |),
                                                M.rust_cast
                                                  (M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "alloc::vec::into_iter::IntoIter",
                                                      "end"
                                                    |)
                                                  |))
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                Value.StructTuple "core::option::Option::None" []
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ _ :=
                                M.write (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::vec::into_iter::IntoIter",
                                    "end"
                                  |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*const") [] [ T ],
                                      "wrapping_byte_sub",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "alloc::vec::into_iter::IntoIter",
                                          "end"
                                        |)
                                      |);
                                      Value.Integer IntegerKind.Usize 1
                                    ]
                                  |)
                                |) in
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::vec::into_iter::IntoIter",
                                "ptr"
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::cmp::PartialEq",
                                                  Ty.apply
                                                    (Ty.path "core::ptr::non_null::NonNull")
                                                    []
                                                    [ T ],
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::ptr::non_null::NonNull")
                                                      []
                                                      [ T ]
                                                  ],
                                                  "eq",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "alloc::vec::into_iter::IntoIter",
                                                    "ptr"
                                                  |);
                                                  M.rust_cast
                                                    (M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "alloc::vec::into_iter::IntoIter",
                                                      "end"
                                                    |))
                                                ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                Value.StructTuple "core::option::Option::None" []
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              let~ old :=
                                M.copy (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::vec::into_iter::IntoIter",
                                    "ptr"
                                  |)
                                |) in
                              let~ _ :=
                                M.write (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::vec::into_iter::IntoIter",
                                    "ptr"
                                  |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                      "add",
                                      []
                                    |),
                                    [ M.read (| old |); Value.Integer IntegerKind.Usize 1 ]
                                  |)
                                |) in
                              old))
                        ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            "read",
                            []
                          |),
                          [ M.read (| ptr |) ]
                        |)
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn size_hint(&self) -> (usize, Option<usize>) {
              let exact = if T::IS_ZST {
                  self.end.addr().wrapping_sub(self.ptr.as_ptr().addr())
              } else {
                  unsafe { non_null!(self.end, T).sub_ptr(self.ptr) }
              };
              (exact, Some(exact))
          }
      *)
      Definition size_hint (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ exact :=
                M.copy (|
                  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.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "wrapping_sub", [] |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "*const") [] [ T ],
                                    "addr",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "alloc::vec::into_iter::IntoIter",
                                        "end"
                                      |)
                                    |)
                                  ]
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "*mut") [] [ T ],
                                    "addr",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                        "as_ptr",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "alloc::vec::into_iter::IntoIter",
                                            "ptr"
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                "sub_ptr",
                                []
                              |),
                              [
                                M.read (|
                                  M.rust_cast
                                    (M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "alloc::vec::into_iter::IntoIter",
                                      "end"
                                    |))
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::vec::into_iter::IntoIter",
                                    "ptr"
                                  |)
                                |)
                              ]
                            |)
                          |)))
                    ]
                  |)
                |) in
              M.alloc (|
                Value.Tuple
                  [
                    M.read (| exact |);
                    Value.StructTuple "core::option::Option::Some" [ M.read (| exact |) ]
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
              let step_size = self.len().min(n);
              let to_drop = ptr::slice_from_raw_parts_mut(self.ptr.as_ptr(), step_size);
              if T::IS_ZST {
                  // See `next` for why we sub `end` here.
                  self.end = self.end.wrapping_byte_sub(step_size);
              } else {
                  // SAFETY: the min() above ensures that step_size is in bounds
                  self.ptr = unsafe { self.ptr.add(step_size) };
              }
              // SAFETY: the min() above ensures that step_size is in bounds
              unsafe {
                  ptr::drop_in_place(to_drop);
              }
              NonZero::new(n - step_size).map_or(Ok(()), Err)
          }
      *)
      Definition advance_by
          (T A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ step_size :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (| "core::cmp::Ord", Ty.path "usize", [], "min", [] |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::exact_size::ExactSizeIterator",
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [ Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ] ],
                          [],
                          "len",
                          []
                        |),
                        [ self ]
                      |);
                      M.read (| n |)
                    ]
                  |)
                |) in
              let~ to_drop :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ T ] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                          "as_ptr",
                          []
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::vec::into_iter::IntoIter",
                              "ptr"
                            |)
                          |)
                        ]
                      |);
                      M.read (| step_size |)
                    ]
                  |)
                |) 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
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::vec::into_iter::IntoIter",
                              "end"
                            |),
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "*const") [] [ T ],
                                "wrapping_byte_sub",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::vec::into_iter::IntoIter",
                                    "end"
                                  |)
                                |);
                                M.read (| step_size |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::vec::into_iter::IntoIter",
                              "ptr"
                            |),
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                "add",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::vec::into_iter::IntoIter",
                                    "ptr"
                                  |)
                                |);
                                M.read (| step_size |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::ptr::drop_in_place",
                        [ Ty.apply (Ty.path "slice") [] [ T ] ]
                      |),
                      [ M.read (| to_drop |) ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ],
                    "map_or",
                    [
                      Ty.apply
                        (Ty.path "core::result::Result")
                        []
                        [
                          Ty.tuple [];
                          Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                        ];
                      Ty.function
                        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ]
                        (Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [
                            Ty.tuple [];
                            Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                          ])
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                        "new",
                        []
                      |),
                      [ BinOp.Wrap.sub (| M.read (| n |), M.read (| step_size |) |) ]
                    |);
                    Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ];
                    M.constructor_as_closure "core::result::Result::Err"
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn count(self) -> usize {
              self.len()
          }
      *)
      Definition count (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A 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",
                Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ],
                [],
                "len",
                []
              |),
              [ self ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn next_chunk<const N: usize>(&mut self) -> Result<[T; N], core::array::IntoIter<T, N>> {
              let mut raw_ary = [const { MaybeUninit::uninit() }; N];
      
              let len = self.len();
      
              if T::IS_ZST {
                  if len < N {
                      self.forget_remaining_elements();
                      // Safety: ZSTs can be conjured ex nihilo, only the amount has to be correct
                      return Err(unsafe { array::IntoIter::new_unchecked(raw_ary, 0..len) });
                  }
      
                  self.end = self.end.wrapping_byte_sub(N);
                  // Safety: ditto
                  return Ok(unsafe { raw_ary.transpose().assume_init() });
              }
      
              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.ptr.as_ptr(), raw_ary.as_mut_ptr() as *mut T, len);
                      self.forget_remaining_elements();
                      return Err(array::IntoIter::new_unchecked(raw_ary, 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.ptr.as_ptr(), raw_ary.as_mut_ptr() as *mut T, N);
                  self.ptr = self.ptr.add(N);
                  Ok(raw_ary.transpose().assume_init())
              }
          }
      *)
      Definition next_chunk
          (T A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [ N ], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ raw_ary :=
                    M.alloc (|
                      repeat (|
                        M.read (|
                          M.get_constant (| "alloc::vec::into_iter::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 "alloc::vec::into_iter::IntoIter") [] [ T; A ] ],
                          [],
                          "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 (|
                                                        "alloc::vec::into_iter::next_chunk::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_associated_function (|
                                                          Ty.apply
                                                            (Ty.path
                                                              "alloc::vec::into_iter::IntoIter")
                                                            []
                                                            [ T; A ],
                                                          "forget_remaining_elements",
                                                          []
                                                        |),
                                                        [ M.read (| self |) ]
                                                      |)
                                                    |) in
                                                  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_ary |);
                                                            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.write (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "alloc::vec::into_iter::IntoIter",
                                        "end"
                                      |),
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "*const") [] [ T ],
                                          "wrapping_byte_sub",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "alloc::vec::into_iter::IntoIter",
                                              "end"
                                            |)
                                          |);
                                          M.read (|
                                            M.get_constant (|
                                              "alloc::vec::into_iter::next_chunk::N"
                                            |)
                                          |)
                                        ]
                                      |)
                                    |) in
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Ok"
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                              []
                                              [ Ty.apply (Ty.path "array") [ N ] [ T ] ],
                                            "assume_init",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "array")
                                                  [ N ]
                                                  [
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::mem::maybe_uninit::MaybeUninit")
                                                      []
                                                      [ T ]
                                                  ],
                                                "transpose",
                                                []
                                              |),
                                              [ M.read (| raw_ary |) ]
                                            |)
                                          ]
                                        |)
                                      ]
                                  |)
                                |)
                              |)
                            |)));
                        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 (| "alloc::vec::into_iter::next_chunk::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 ]
                                        |),
                                        [
                                          (* MutToConstPointer *)
                                          M.pointer_coercion
                                            (M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::ptr::non_null::NonNull")
                                                  []
                                                  [ T ],
                                                "as_ptr",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "alloc::vec::into_iter::IntoIter",
                                                    "ptr"
                                                  |)
                                                |)
                                              ]
                                            |));
                                          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_ary ]
                                            |));
                                          M.read (| len |)
                                        ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::into_iter::IntoIter")
                                            []
                                            [ T; A ],
                                          "forget_remaining_elements",
                                          []
                                        |),
                                        [ M.read (| self |) ]
                                      |)
                                    |) in
                                  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_ary |);
                                            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 ] |),
                        [
                          (* MutToConstPointer *)
                          M.pointer_coercion
                            (M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                                "as_ptr",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::vec::into_iter::IntoIter",
                                    "ptr"
                                  |)
                                |)
                              ]
                            |));
                          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_ary ]
                            |));
                          M.read (| M.get_constant (| "alloc::vec::into_iter::next_chunk::N" |) |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.write (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::vec::into_iter::IntoIter",
                        "ptr"
                      |),
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                          "add",
                          []
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::vec::into_iter::IntoIter",
                              "ptr"
                            |)
                          |);
                          M.read (| M.get_constant (| "alloc::vec::into_iter::next_chunk::N" |) |)
                        ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                              []
                              [ Ty.apply (Ty.path "array") [ N ] [ T ] ],
                            "assume_init",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "array")
                                  [ N ]
                                  [
                                    Ty.apply
                                      (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                      []
                                      [ T ]
                                  ],
                                "transpose",
                                []
                              |),
                              [ M.read (| raw_ary |) ]
                            |)
                          ]
                        |)
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn fold<B, F>(mut self, mut accum: B, mut f: F) -> B
          where
              F: FnMut(B, Self::Item) -> B,
          {
              if T::IS_ZST {
                  while self.ptr.as_ptr() != self.end.cast_mut() {
                      // SAFETY: we just checked that `self.ptr` is in bounds.
                      let tmp = unsafe { self.ptr.read() };
                      // See `next` for why we subtract from `end` here.
                      self.end = self.end.wrapping_byte_sub(1);
                      accum = f(accum, tmp);
                  }
              } else {
                  // SAFETY: `self.end` can only be null if `T` is a ZST.
                  while self.ptr != non_null!(self.end, T) {
                      // SAFETY: we just checked that `self.ptr` is in bounds.
                      let tmp = unsafe { self.ptr.read() };
                      // SAFETY: the maximum this can be is `self.end`.
                      // Increment `self.ptr` first to avoid double dropping in the event of a panic.
                      self.ptr = unsafe { self.ptr.add(1) };
                      accum = f(accum, tmp);
                  }
              }
              accum
          }
      *)
      Definition fold (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [ B; F ], [ self; accum; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let accum := M.alloc (| accum |) in
            let f := M.alloc (| f |) in
            M.read (|
              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.loop (|
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.ne (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::ptr::non_null::NonNull")
                                                  []
                                                  [ T ],
                                                "as_ptr",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    self,
                                                    "alloc::vec::into_iter::IntoIter",
                                                    "ptr"
                                                  |)
                                                |)
                                              ]
                                            |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*const") [] [ T ],
                                                "cast_mut",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    self,
                                                    "alloc::vec::into_iter::IntoIter",
                                                    "end"
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ tmp :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ T ],
                                            "read",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "alloc::vec::into_iter::IntoIter",
                                                "ptr"
                                              |)
                                            |)
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "alloc::vec::into_iter::IntoIter",
                                          "end"
                                        |),
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "*const") [] [ T ],
                                            "wrapping_byte_sub",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "alloc::vec::into_iter::IntoIter",
                                                "end"
                                              |)
                                            |);
                                            Value.Integer IntegerKind.Usize 1
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        accum,
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::function::FnMut",
                                            F,
                                            [ Ty.tuple [ B; T ] ],
                                            "call_mut",
                                            []
                                          |),
                                          [ f; Value.Tuple [ M.read (| accum |); M.read (| tmp |) ]
                                          ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          let~ _ :=
                                            M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)
                                        |)
                                      |)
                                    |)))
                              ]
                            |)))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.loop (|
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::cmp::PartialEq",
                                              Ty.apply
                                                (Ty.path "core::ptr::non_null::NonNull")
                                                []
                                                [ T ],
                                              [
                                                Ty.apply
                                                  (Ty.path "core::ptr::non_null::NonNull")
                                                  []
                                                  [ T ]
                                              ],
                                              "ne",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "alloc::vec::into_iter::IntoIter",
                                                "ptr"
                                              |);
                                              M.rust_cast
                                                (M.SubPointer.get_struct_record_field (|
                                                  self,
                                                  "alloc::vec::into_iter::IntoIter",
                                                  "end"
                                                |))
                                            ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ tmp :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ T ],
                                            "read",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "alloc::vec::into_iter::IntoIter",
                                                "ptr"
                                              |)
                                            |)
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "alloc::vec::into_iter::IntoIter",
                                          "ptr"
                                        |),
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::ptr::non_null::NonNull")
                                              []
                                              [ T ],
                                            "add",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "alloc::vec::into_iter::IntoIter",
                                                "ptr"
                                              |)
                                            |);
                                            Value.Integer IntegerKind.Usize 1
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        accum,
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::function::FnMut",
                                            F,
                                            [ Ty.tuple [ B; T ] ],
                                            "call_mut",
                                            []
                                          |),
                                          [ f; Value.Tuple [ M.read (| accum |); M.read (| tmp |) ]
                                          ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          let~ _ :=
                                            M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)
                                        |)
                                      |)
                                    |)))
                              ]
                            |)))
                        |)))
                  ]
                |) in
              accum
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn try_fold<B, F, R>(&mut self, mut accum: B, mut f: F) -> R
          where
              Self: Sized,
              F: FnMut(B, Self::Item) -> R,
              R: core::ops::Try<Output = B>,
          {
              if T::IS_ZST {
                  while self.ptr.as_ptr() != self.end.cast_mut() {
                      // SAFETY: we just checked that `self.ptr` is in bounds.
                      let tmp = unsafe { self.ptr.read() };
                      // See `next` for why we subtract from `end` here.
                      self.end = self.end.wrapping_byte_sub(1);
                      accum = f(accum, tmp)?;
                  }
              } else {
                  // SAFETY: `self.end` can only be null if `T` is a ZST.
                  while self.ptr != non_null!(self.end, T) {
                      // SAFETY: we just checked that `self.ptr` is in bounds.
                      let tmp = unsafe { self.ptr.read() };
                      // SAFETY: the maximum this can be is `self.end`.
                      // Increment `self.ptr` first to avoid double dropping in the event of a panic.
                      self.ptr = unsafe { self.ptr.add(1) };
                      accum = f(accum, tmp)?;
                  }
              }
              R::from_output(accum)
          }
      *)
      Definition try_fold (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [ B; F; R ], [ self; accum; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let accum := M.alloc (| accum |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  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.loop (|
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              BinOp.ne (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::ptr::non_null::NonNull")
                                                      []
                                                      [ T ],
                                                    "as_ptr",
                                                    []
                                                  |),
                                                  [
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "alloc::vec::into_iter::IntoIter",
                                                        "ptr"
                                                      |)
                                                    |)
                                                  ]
                                                |),
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply (Ty.path "*const") [] [ T ],
                                                    "cast_mut",
                                                    []
                                                  |),
                                                  [
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "alloc::vec::into_iter::IntoIter",
                                                        "end"
                                                      |)
                                                    |)
                                                  ]
                                                |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ tmp :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::ptr::non_null::NonNull")
                                                  []
                                                  [ T ],
                                                "read",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "alloc::vec::into_iter::IntoIter",
                                                    "ptr"
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "alloc::vec::into_iter::IntoIter",
                                              "end"
                                            |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply (Ty.path "*const") [] [ T ],
                                                "wrapping_byte_sub",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "alloc::vec::into_iter::IntoIter",
                                                    "end"
                                                  |)
                                                |);
                                                Value.Integer IntegerKind.Usize 1
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            accum,
                                            M.read (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      R,
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::function::FnMut",
                                                          F,
                                                          [ Ty.tuple [ B; T ] ],
                                                          "call_mut",
                                                          []
                                                        |),
                                                        [
                                                          f;
                                                          Value.Tuple
                                                            [ M.read (| accum |); M.read (| tmp |) ]
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Break",
                                                          0
                                                        |) in
                                                      let residual := M.copy (| γ0_0 |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::try_trait::FromResidual",
                                                                  R,
                                                                  [ Ty.associated ],
                                                                  "from_residual",
                                                                  []
                                                                |),
                                                                [ M.read (| residual |) ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Continue",
                                                          0
                                                        |) in
                                                      let val := M.copy (| γ0_0 |) in
                                                      val))
                                                ]
                                              |)
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              let~ _ :=
                                                M.alloc (|
                                                  M.never_to_any (| M.read (| M.break (||) |) |)
                                                |) in
                                              M.alloc (| Value.Tuple [] |)
                                            |)
                                          |)
                                        |)))
                                  ]
                                |)))
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.loop (|
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::cmp::PartialEq",
                                                  Ty.apply
                                                    (Ty.path "core::ptr::non_null::NonNull")
                                                    []
                                                    [ T ],
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::ptr::non_null::NonNull")
                                                      []
                                                      [ T ]
                                                  ],
                                                  "ne",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "alloc::vec::into_iter::IntoIter",
                                                    "ptr"
                                                  |);
                                                  M.rust_cast
                                                    (M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "alloc::vec::into_iter::IntoIter",
                                                      "end"
                                                    |))
                                                ]
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        let~ tmp :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::ptr::non_null::NonNull")
                                                  []
                                                  [ T ],
                                                "read",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "alloc::vec::into_iter::IntoIter",
                                                    "ptr"
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "alloc::vec::into_iter::IntoIter",
                                              "ptr"
                                            |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::ptr::non_null::NonNull")
                                                  []
                                                  [ T ],
                                                "add",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "alloc::vec::into_iter::IntoIter",
                                                    "ptr"
                                                  |)
                                                |);
                                                Value.Integer IntegerKind.Usize 1
                                              ]
                                            |)
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            accum,
                                            M.read (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      R,
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::function::FnMut",
                                                          F,
                                                          [ Ty.tuple [ B; T ] ],
                                                          "call_mut",
                                                          []
                                                        |),
                                                        [
                                                          f;
                                                          Value.Tuple
                                                            [ M.read (| accum |); M.read (| tmp |) ]
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Break",
                                                          0
                                                        |) in
                                                      let residual := M.copy (| γ0_0 |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::try_trait::FromResidual",
                                                                  R,
                                                                  [ Ty.associated ],
                                                                  "from_residual",
                                                                  []
                                                                |),
                                                                [ M.read (| residual |) ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Continue",
                                                          0
                                                        |) in
                                                      let val := M.copy (| γ0_0 |) in
                                                      val))
                                                ]
                                              |)
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              let~ _ :=
                                                M.alloc (|
                                                  M.never_to_any (| M.read (| M.break (||) |) |)
                                                |) in
                                              M.alloc (| Value.Tuple [] |)
                                            |)
                                          |)
                                        |)))
                                  ]
                                |)))
                            |)))
                      ]
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        R,
                        [],
                        "from_output",
                        []
                      |),
                      [ M.read (| accum |) ]
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn __iterator_get_unchecked(&mut self, i: usize) -> Self::Item
          where
              Self: TrustedRandomAccessNoCoerce,
          {
              // SAFETY: the caller must guarantee that `i` is in bounds of the
              // `Vec<T>`, so `i` cannot overflow an `isize`, and the `self.ptr.add(i)`
              // is guaranteed to pointer to an element of the `Vec<T>` and
              // thus guaranteed to be valid to dereference.
              //
              // Also note the implementation of `Self: TrustedRandomAccess` requires
              // that `T: Copy` so reading elements from the buffer doesn't invalidate
              // them for `Drop`.
              unsafe { self.ptr.add(i).read() }
          }
      *)
      Definition __iterator_get_unchecked
          (T A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self; i ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let i := M.alloc (| i |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                "read",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                    "add",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "alloc::vec::into_iter::IntoIter",
                        "ptr"
                      |)
                    |);
                    M.read (| i |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item T A));
            ("next", InstanceField.Method (next T A));
            ("size_hint", InstanceField.Method (size_hint T A));
            ("advance_by", InstanceField.Method (advance_by T A));
            ("count", InstanceField.Method (count T A));
            ("next_chunk", InstanceField.Method (next_chunk T A));
            ("fold", InstanceField.Method (fold T A));
            ("try_fold", InstanceField.Method (try_fold T A));
            ("__iterator_get_unchecked", InstanceField.Method (__iterator_get_unchecked T A))
          ].
    End Impl_core_iter_traits_iterator_Iterator_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*
          fn next_back(&mut self) -> Option<T> {
              if T::IS_ZST {
                  if self.ptr.as_ptr() == self.end as *mut _ {
                      return None;
                  }
                  // See above for why 'ptr.offset' isn't used
                  self.end = self.end.wrapping_byte_sub(1);
                  // Note that even though this is next_back() we're reading from `self.ptr`, not
                  // `self.end`. We track our length using the byte offset from `self.ptr` to `self.end`,
                  // so the end pointer may not be suitably aligned for T.
                  Some(unsafe { ptr::read(self.ptr.as_ptr()) })
              } else {
                  if self.ptr == non_null!(self.end, T) {
                      return None;
                  }
                  unsafe {
                      self.end = self.end.sub(1);
                      Some(ptr::read(self.end))
                  }
              }
          }
      *)
      Definition next_back (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  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
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.eq (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::ptr::non_null::NonNull")
                                                  []
                                                  [ T ],
                                                "as_ptr",
                                                []
                                              |),
                                              [
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "alloc::vec::into_iter::IntoIter",
                                                    "ptr"
                                                  |)
                                                |)
                                              ]
                                            |),
                                            M.rust_cast
                                              (M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "alloc::vec::into_iter::IntoIter",
                                                  "end"
                                                |)
                                              |))
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          M.return_ (|
                                            Value.StructTuple "core::option::Option::None" []
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::vec::into_iter::IntoIter",
                                "end"
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*const") [] [ T ],
                                  "wrapping_byte_sub",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "alloc::vec::into_iter::IntoIter",
                                      "end"
                                    |)
                                  |);
                                  Value.Integer IntegerKind.Usize 1
                                ]
                              |)
                            |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::option::Option::Some"
                              [
                                M.call_closure (|
                                  M.get_function (| "core::ptr::read", [ T ] |),
                                  [
                                    (* MutToConstPointer *)
                                    M.pointer_coercion
                                      (M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::ptr::non_null::NonNull")
                                            []
                                            [ T ],
                                          "as_ptr",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "alloc::vec::into_iter::IntoIter",
                                              "ptr"
                                            |)
                                          |)
                                        ]
                                      |))
                                  ]
                                |)
                              ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::cmp::PartialEq",
                                              Ty.apply
                                                (Ty.path "core::ptr::non_null::NonNull")
                                                []
                                                [ T ],
                                              [
                                                Ty.apply
                                                  (Ty.path "core::ptr::non_null::NonNull")
                                                  []
                                                  [ T ]
                                              ],
                                              "eq",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "alloc::vec::into_iter::IntoIter",
                                                "ptr"
                                              |);
                                              M.rust_cast
                                                (M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "alloc::vec::into_iter::IntoIter",
                                                  "end"
                                                |))
                                            ]
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          M.return_ (|
                                            Value.StructTuple "core::option::Option::None" []
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::vec::into_iter::IntoIter",
                                "end"
                              |),
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "*const") [] [ T ],
                                  "sub",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "alloc::vec::into_iter::IntoIter",
                                      "end"
                                    |)
                                  |);
                                  Value.Integer IntegerKind.Usize 1
                                ]
                              |)
                            |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::option::Option::Some"
                              [
                                M.call_closure (|
                                  M.get_function (| "core::ptr::read", [ T ] |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "alloc::vec::into_iter::IntoIter",
                                        "end"
                                      |)
                                    |)
                                  ]
                                |)
                              ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
              let step_size = self.len().min(n);
              if T::IS_ZST {
                  // SAFETY: same as for advance_by()
                  self.end = self.end.wrapping_byte_sub(step_size);
              } else {
                  // SAFETY: same as for advance_by()
                  self.end = unsafe { self.end.sub(step_size) };
              }
              let to_drop = ptr::slice_from_raw_parts_mut(self.end as *mut T, step_size);
              // SAFETY: same as for advance_by()
              unsafe {
                  ptr::drop_in_place(to_drop);
              }
              NonZero::new(n - step_size).map_or(Ok(()), Err)
          }
      *)
      Definition advance_back_by
          (T A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ step_size :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (| "core::cmp::Ord", Ty.path "usize", [], "min", [] |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::exact_size::ExactSizeIterator",
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [ Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ] ],
                          [],
                          "len",
                          []
                        |),
                        [ self ]
                      |);
                      M.read (| n |)
                    ]
                  |)
                |) 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
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::vec::into_iter::IntoIter",
                              "end"
                            |),
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "*const") [] [ T ],
                                "wrapping_byte_sub",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::vec::into_iter::IntoIter",
                                    "end"
                                  |)
                                |);
                                M.read (| step_size |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::vec::into_iter::IntoIter",
                              "end"
                            |),
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "*const") [] [ T ],
                                "sub",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::vec::into_iter::IntoIter",
                                    "end"
                                  |)
                                |);
                                M.read (| step_size |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ to_drop :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ T ] |),
                    [
                      M.rust_cast
                        (M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "alloc::vec::into_iter::IntoIter",
                            "end"
                          |)
                        |));
                      M.read (| step_size |)
                    ]
                  |)
                |) in
              let~ _ :=
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::ptr::drop_in_place",
                        [ Ty.apply (Ty.path "slice") [] [ T ] ]
                      |),
                      [ M.read (| to_drop |) ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ],
                    "map_or",
                    [
                      Ty.apply
                        (Ty.path "core::result::Result")
                        []
                        [
                          Ty.tuple [];
                          Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                        ];
                      Ty.function
                        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ]
                        (Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [
                            Ty.tuple [];
                            Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                          ])
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                        "new",
                        []
                      |),
                      [ BinOp.Wrap.sub (| M.read (| n |), M.read (| step_size |) |) ]
                    |);
                    Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ];
                    M.constructor_as_closure "core::result::Result::Err"
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::double_ended::DoubleEndedIterator"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("next_back", InstanceField.Method (next_back T A));
            ("advance_back_by", InstanceField.Method (advance_back_by T A))
          ].
    End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*
          fn is_empty(&self) -> bool {
              if T::IS_ZST {
                  self.ptr.as_ptr() == self.end as *mut _
              } else {
                  self.ptr == non_null!(self.end, T)
              }
          }
      *)
      Definition is_empty (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              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 (|
                        BinOp.eq (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                              "as_ptr",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::vec::into_iter::IntoIter",
                                  "ptr"
                                |)
                              |)
                            ]
                          |),
                          M.rust_cast
                            (M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::vec::into_iter::IntoIter",
                                "end"
                              |)
                            |))
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            [ Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ] ],
                            "eq",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::vec::into_iter::IntoIter",
                              "ptr"
                            |);
                            M.rust_cast
                              (M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::vec::into_iter::IntoIter",
                                "end"
                              |))
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::exact_size::ExactSizeIterator"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("is_empty", InstanceField.Method (is_empty T A)) ].
    End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_iter_traits_marker_FusedIterator_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_iter_traits_marker_TrustedFused_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::TrustedFused"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_TrustedFused_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_iter_traits_marker_TrustedLen_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::TrustedLen"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_TrustedLen_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_default_Default_where_core_alloc_Allocator_A_where_core_default_Default_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*
          fn default() -> Self {
              super::Vec::new_in(Default::default()).into_iter()
          }
      *)
      Definition default (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::collect::IntoIterator",
                Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                [],
                "into_iter",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    "new_in",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (| "core::default::Default", A, [], "default", [] |),
                      []
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::default::Default"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method (default T A)) ].
    End Impl_core_default_Default_where_core_alloc_Allocator_A_where_core_default_Default_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    (* Trait *)
    (* Empty module 'NonDrop' *)
    
    Module Impl_alloc_vec_into_iter_NonDrop_where_core_marker_Copy_T_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "alloc::vec::into_iter::NonDrop"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_alloc_vec_into_iter_NonDrop_where_core_marker_Copy_T_for_T.
    
    Module Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_where_core_alloc_Allocator_A_where_alloc_vec_into_iter_NonDrop_T_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*     const MAY_HAVE_SIDE_EFFECT: bool = false; *)
      (* Ty.path "bool" *)
      Definition value_MAY_HAVE_SIDE_EFFECT (T A : Ty.t) : Value.t :=
        let Self : Ty.t := Self T A in
        M.run ltac:(M.monadic (M.alloc (| Value.Bool false |))).
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::adapters::zip::TrustedRandomAccessNoCoerce"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("value_MAY_HAVE_SIDE_EFFECT", InstanceField.Constant (value_MAY_HAVE_SIDE_EFFECT T A))
          ].
    End Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_where_core_alloc_Allocator_A_where_alloc_vec_into_iter_NonDrop_T_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_clone_Clone_where_core_clone_Clone_T_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*
          fn clone(&self) -> Self {
              self.as_slice().to_vec_in(self.alloc.deref().clone()).into_iter()
          }
      *)
      Definition clone (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::collect::IntoIterator",
                Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                [],
                "into_iter",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ T ],
                    "to_vec_in",
                    [ A ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ],
                        "as_slice",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.call_closure (|
                      M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.apply (Ty.path "core::mem::manually_drop::ManuallyDrop") [] [ A ],
                            [],
                            "deref",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "alloc::vec::into_iter::IntoIter",
                              "alloc"
                            |)
                          ]
                        |)
                      ]
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::clone::Clone"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method (clone T A)) ].
    End Impl_core_clone_Clone_where_core_clone_Clone_T_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_ops_drop_Drop_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*
          fn drop(&mut self) {
              struct DropGuard<'a, T, A: Allocator>(&'a mut IntoIter<T, A>);
      
              impl<T, A: Allocator> Drop for DropGuard<'_, T, A> {
                  fn drop(&mut self) {
                      unsafe {
                          // `IntoIter::alloc` is not used anymore after this and will be dropped by RawVec
                          let alloc = ManuallyDrop::take(&mut self.0.alloc);
                          // RawVec handles deallocation
                          let _ = RawVec::from_nonnull_in(self.0.buf, self.0.cap, alloc);
                      }
                  }
              }
      
              let guard = DropGuard(self);
              // destroy the remaining elements
              unsafe {
                  ptr::drop_in_place(guard.0.as_raw_mut_slice());
              }
              // now `guard` will be dropped and do the rest
          }
      *)
      Definition drop (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ guard :=
                M.alloc (|
                  Value.StructTuple "alloc::vec::into_iter::drop::DropGuard" [ M.read (| self |) ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::ptr::drop_in_place",
                      [ Ty.apply (Ty.path "slice") [] [ T ] ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ],
                          "as_raw_mut_slice",
                          []
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_tuple_field (|
                              guard,
                              "alloc::vec::into_iter::drop::DropGuard",
                              0
                            |)
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::ops::drop::Drop"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("drop", InstanceField.Method (drop T A)) ].
    End Impl_core_ops_drop_Drop_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_iter_traits_marker_InPlaceIterable_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*     const EXPAND_BY: Option<NonZero<usize>> = NonZero::new(1); *)
      (* Ty.apply
        (Ty.path "core::option::Option")
        []
        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ] *)
      Definition value_EXPAND_BY (T A : Ty.t) : Value.t :=
        let Self : Ty.t := Self T A in
        M.run
          ltac:(M.monadic
            (M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                  "new",
                  []
                |),
                [ Value.Integer IntegerKind.Usize 1 ]
              |)
            |))).
      
      (*     const MERGE_BY: Option<NonZero<usize>> = NonZero::new(1); *)
      (* Ty.apply
        (Ty.path "core::option::Option")
        []
        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ] *)
      Definition value_MERGE_BY (T A : Ty.t) : Value.t :=
        let Self : Ty.t := Self T A in
        M.run
          ltac:(M.monadic
            (M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                  "new",
                  []
                |),
                [ Value.Integer IntegerKind.Usize 1 ]
              |)
            |))).
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::InPlaceIterable"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("value_EXPAND_BY", InstanceField.Constant (value_EXPAND_BY T A));
            ("value_MERGE_BY", InstanceField.Constant (value_MERGE_BY T A))
          ].
    End Impl_core_iter_traits_marker_InPlaceIterable_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_core_iter_adapters_SourceIter_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
      Definition Self (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*     type Source = Self; *)
      Definition _Source (T A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::into_iter::IntoIter") [] [ T; A ].
      
      (*
          unsafe fn as_inner(&mut self) -> &mut Self::Source {
              self
          }
      *)
      Definition as_inner (T A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T A in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| self |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T A : Ty.t),
        M.IsTraitInstance
          "core::iter::adapters::SourceIter"
          (Self T A)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Source", InstanceField.Ty (_Source T A));
            ("as_inner", InstanceField.Method (as_inner T A))
          ].
    End Impl_core_iter_adapters_SourceIter_where_core_alloc_Allocator_A_for_alloc_vec_into_iter_IntoIter_T_A.
    
    Module Impl_alloc_vec_in_place_collect_AsVecIntoIter_for_alloc_vec_into_iter_IntoIter_T_alloc_alloc_Global.
      Definition Self (T : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "alloc::vec::into_iter::IntoIter")
          []
          [ T; Ty.path "alloc::alloc::Global" ].
      
      (*     type Item = T; *)
      Definition _Item (T : Ty.t) : Ty.t := T.
      
      (*
          fn as_into_iter(&mut self) -> &mut IntoIter<Self::Item> {
              self
          }
      *)
      Definition as_into_iter
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| self |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "alloc::vec::in_place_collect::AsVecIntoIter"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item T));
            ("as_into_iter", InstanceField.Method (as_into_iter T))
          ].
    End Impl_alloc_vec_in_place_collect_AsVecIntoIter_for_alloc_vec_into_iter_IntoIter_T_alloc_alloc_Global.
  End into_iter.
End vec.
