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

Module iter.
  Module adapters.
    Module fuse.
      (* StructRecord
        {
          name := "Fuse";
          const_params := [];
          ty_params := [ "I" ];
          fields := [ ("iter", Ty.apply (Ty.path "core::option::Option") [] [ I ]) ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (* Clone *)
        Definition clone (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "core::iter::adapters::fuse::Fuse"
                [
                  ("iter",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply (Ty.path "core::option::Option") [] [ I ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::iter::adapters::fuse::Fuse",
                          "iter"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::clone::Clone"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method (clone I)) ].
      End Impl_core_clone_Clone_where_core_clone_Clone_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (* Debug *)
        Definition fmt (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_field1_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "Fuse" |);
                  M.read (| Value.String "iter" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::iter::adapters::fuse::Fuse",
                      "iter"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt I)) ].
      End Impl_core_fmt_Debug_where_core_fmt_Debug_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (*
            pub(in crate::iter) fn new(iter: I) -> Fuse<I> {
                Fuse { iter: Some(iter) }
            }
        *)
        Definition new (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ iter ] =>
            ltac:(M.monadic
              (let iter := M.alloc (| iter |) in
              Value.StructRecord
                "core::iter::adapters::fuse::Fuse"
                [ ("iter", Value.StructTuple "core::option::Option::Some" [ M.read (| iter |) ]) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (I : Ty.t),
          M.IsAssociatedFunction (Self I) "new" (new I).
        
        (*
            pub(crate) fn into_inner(self) -> Option<I> {
                self.iter
            }
        *)
        Definition into_inner
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  self,
                  "core::iter::adapters::fuse::Fuse",
                  "iter"
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_into_inner :
          forall (I : Ty.t),
          M.IsAssociatedFunction (Self I) "into_inner" (into_inner I).
      End Impl_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_iterator_Iterator_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::FusedIterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_iterator_Iterator_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_traits_marker_TrustedFused_where_core_iter_traits_marker_TrustedFused_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::TrustedFused"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_TrustedFused_where_core_iter_traits_marker_TrustedFused_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (*     type Item = <I as Iterator>::Item; *)
        Definition _Item (I : Ty.t) : Ty.t := Ty.associated.
        
        (*
            fn next(&mut self) -> Option<Self::Item> {
                FuseImpl::next(self)
            }
        *)
        Definition next (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::adapters::fuse::FuseImpl",
                  Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                  [ I ],
                  "next",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth(&mut self, n: usize) -> Option<I::Item> {
                FuseImpl::nth(self, n)
            }
        *)
        Definition nth (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::adapters::fuse::FuseImpl",
                  Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                  [ I ],
                  "nth",
                  []
                |),
                [ M.read (| self |); M.read (| n |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn last(self) -> Option<Self::Item> {
                match self.iter {
                    Some(iter) => iter.last(),
                    None => None,
                }
            }
        *)
        Definition last (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let iter := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              I,
                              [],
                              "last",
                              []
                            |),
                            [ M.read (| iter |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn count(self) -> usize {
                match self.iter {
                    Some(iter) => iter.count(),
                    None => 0,
                }
            }
        *)
        Definition count (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let iter := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              I,
                              [],
                              "count",
                              []
                            |),
                            [ M.read (| iter |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn size_hint(&self) -> (usize, Option<usize>) {
                match self.iter {
                    Some(ref iter) => iter.size_hint(),
                    None => (0, Some(0)),
                }
            }
        *)
        Definition size_hint (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let iter := M.alloc (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              I,
                              [],
                              "size_hint",
                              []
                            |),
                            [ M.read (| iter |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              Value.Integer IntegerKind.Usize 0;
                              Value.StructTuple
                                "core::option::Option::Some"
                                [ Value.Integer IntegerKind.Usize 0 ]
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_fold<Acc, Fold, R>(&mut self, acc: Acc, fold: Fold) -> R
            where
                Self: Sized,
                Fold: FnMut(Acc, Self::Item) -> R,
                R: Try<Output = Acc>,
            {
                FuseImpl::try_fold(self, acc, fold)
            }
        *)
        Definition try_fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold; R ], [ self; acc; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let acc := M.alloc (| acc |) in
              let fold := M.alloc (| fold |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::adapters::fuse::FuseImpl",
                  Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                  [ I ],
                  "try_fold",
                  [ Acc; Fold; R ]
                |),
                [ M.read (| self |); M.read (| acc |); M.read (| fold |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn fold<Acc, Fold>(self, mut acc: Acc, fold: Fold) -> Acc
            where
                Fold: FnMut(Acc, Self::Item) -> Acc,
            {
                if let Some(iter) = self.iter {
                    acc = iter.fold(acc, fold);
                }
                acc
            }
        *)
        Definition fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold ], [ self; acc; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let acc := M.alloc (| acc |) in
              let fold := M.alloc (| fold |) in
              M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::iter::adapters::fuse::Fuse",
                              "iter"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let iter := M.copy (| γ0_0 |) in
                          let~ _ :=
                            M.write (|
                              acc,
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  I,
                                  [],
                                  "fold",
                                  [ Acc; Fold ]
                                |),
                                [ M.read (| iter |); M.read (| acc |); M.read (| fold |) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                acc
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn find<P>(&mut self, predicate: P) -> Option<Self::Item>
            where
                P: FnMut(&Self::Item) -> bool,
            {
                FuseImpl::find(self, predicate)
            }
        *)
        Definition find (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::adapters::fuse::FuseImpl",
                  Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                  [ I ],
                  "find",
                  [ P ]
                |),
                [ M.read (| self |); M.read (| predicate |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
            where
                Self: TrustedRandomAccessNoCoerce,
            {
                match self.iter {
                    // SAFETY: the caller must uphold the contract for
                    // `Iterator::__iterator_get_unchecked`.
                    Some(ref mut iter) => unsafe { try_get_unchecked(iter, idx) },
                    // SAFETY: the caller asserts there is an item at `i`, so we're not exhausted.
                    None => unsafe { intrinsics::unreachable() },
                }
            }
        *)
        Definition __iterator_get_unchecked
            (I : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; idx ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let idx := M.alloc (| idx |) in
              M.read (|
                M.match_operator (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let iter := M.alloc (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::iter::adapters::zip::try_get_unchecked",
                              [ I ]
                            |),
                            [ M.read (| iter |); M.read (| idx |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::intrinsics::unreachable", [] |),
                              []
                            |)
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::iterator::Iterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item I));
              ("next", InstanceField.Method (next I));
              ("nth", InstanceField.Method (nth I));
              ("last", InstanceField.Method (last I));
              ("count", InstanceField.Method (count I));
              ("size_hint", InstanceField.Method (size_hint I));
              ("try_fold", InstanceField.Method (try_fold I));
              ("fold", InstanceField.Method (fold I));
              ("find", InstanceField.Method (find I));
              ("__iterator_get_unchecked", InstanceField.Method (__iterator_get_unchecked I))
            ].
      End Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (*
            fn next_back(&mut self) -> Option<<I as Iterator>::Item> {
                FuseImpl::next_back(self)
            }
        *)
        Definition next_back (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::adapters::fuse::FuseImpl",
                  Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                  [ I ],
                  "next_back",
                  []
                |),
                [ M.read (| self |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth_back(&mut self, n: usize) -> Option<<I as Iterator>::Item> {
                FuseImpl::nth_back(self, n)
            }
        *)
        Definition nth_back (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::adapters::fuse::FuseImpl",
                  Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                  [ I ],
                  "nth_back",
                  []
                |),
                [ M.read (| self |); M.read (| n |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_rfold<Acc, Fold, R>(&mut self, acc: Acc, fold: Fold) -> R
            where
                Self: Sized,
                Fold: FnMut(Acc, Self::Item) -> R,
                R: Try<Output = Acc>,
            {
                FuseImpl::try_rfold(self, acc, fold)
            }
        *)
        Definition try_rfold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold; R ], [ self; acc; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let acc := M.alloc (| acc |) in
              let fold := M.alloc (| fold |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::adapters::fuse::FuseImpl",
                  Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                  [ I ],
                  "try_rfold",
                  [ Acc; Fold; R ]
                |),
                [ M.read (| self |); M.read (| acc |); M.read (| fold |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfold<Acc, Fold>(self, mut acc: Acc, fold: Fold) -> Acc
            where
                Fold: FnMut(Acc, Self::Item) -> Acc,
            {
                if let Some(iter) = self.iter {
                    acc = iter.rfold(acc, fold);
                }
                acc
            }
        *)
        Definition rfold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold ], [ self; acc; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let acc := M.alloc (| acc |) in
              let fold := M.alloc (| fold |) in
              M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::iter::adapters::fuse::Fuse",
                              "iter"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let iter := M.copy (| γ0_0 |) in
                          let~ _ :=
                            M.write (|
                              acc,
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::double_ended::DoubleEndedIterator",
                                  I,
                                  [],
                                  "rfold",
                                  [ Acc; Fold ]
                                |),
                                [ M.read (| iter |); M.read (| acc |); M.read (| fold |) ]
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                acc
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfind<P>(&mut self, predicate: P) -> Option<Self::Item>
            where
                P: FnMut(&Self::Item) -> bool,
            {
                FuseImpl::rfind(self, predicate)
            }
        *)
        Definition rfind (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::adapters::fuse::FuseImpl",
                  Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ],
                  [ I ],
                  "rfind",
                  [ P ]
                |),
                [ M.read (| self |); M.read (| predicate |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::double_ended::DoubleEndedIterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("next_back", InstanceField.Method (next_back I));
              ("nth_back", InstanceField.Method (nth_back I));
              ("try_rfold", InstanceField.Method (try_rfold I));
              ("rfold", InstanceField.Method (rfold I));
              ("rfind", InstanceField.Method (rfind I))
            ].
      End Impl_core_iter_traits_double_ended_DoubleEndedIterator_where_core_iter_traits_double_ended_DoubleEndedIterator_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (*
            fn len(&self) -> usize {
                match self.iter {
                    Some(ref iter) => iter.len(),
                    None => 0,
                }
            }
        *)
        Definition len (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let iter := M.alloc (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::exact_size::ExactSizeIterator",
                              I,
                              [],
                              "len",
                              []
                            |),
                            [ M.read (| iter |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (| Value.Integer IntegerKind.Usize 0 |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn is_empty(&self) -> bool {
                match self.iter {
                    Some(ref iter) => iter.is_empty(),
                    None => true,
                }
            }
        *)
        Definition is_empty (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::option::Option::Some",
                            0
                          |) in
                        let iter := M.alloc (| γ0_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::exact_size::ExactSizeIterator",
                              I,
                              [],
                              "is_empty",
                              []
                            |),
                            [ M.read (| iter |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                        M.alloc (| Value.Bool true |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::exact_size::ExactSizeIterator"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("len", InstanceField.Method (len I)); ("is_empty", InstanceField.Method (is_empty I))
            ].
      End Impl_core_iter_traits_exact_size_ExactSizeIterator_where_core_iter_traits_exact_size_ExactSizeIterator_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_default_Default_where_core_default_Default_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (*
            fn default() -> Self {
                Fuse { iter: Default::default() }
            }
        *)
        Definition default (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "core::iter::adapters::fuse::Fuse"
                [
                  ("iter",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.apply (Ty.path "core::option::Option") [] [ I ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::default::Default"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method (default I)) ].
      End Impl_core_default_Default_where_core_default_Default_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_traits_marker_TrustedLen_where_core_iter_traits_marker_TrustedLen_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::traits::marker::TrustedLen"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_traits_marker_TrustedLen_where_core_iter_traits_marker_TrustedLen_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_adapters_zip_TrustedRandomAccess_where_core_iter_adapters_zip_TrustedRandomAccess_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::zip::TrustedRandomAccess"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_iter_adapters_zip_TrustedRandomAccess_where_core_iter_adapters_zip_TrustedRandomAccess_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_where_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (*     const MAY_HAVE_SIDE_EFFECT: bool = I::MAY_HAVE_SIDE_EFFECT; *)
        (* Ty.path "bool" *)
        Definition value_MAY_HAVE_SIDE_EFFECT (I : Ty.t) : Value.t :=
          let Self : Ty.t := Self I in
          M.run
            ltac:(M.monadic
              (M.get_constant (|
                "core::iter::adapters::zip::TrustedRandomAccessNoCoerce::MAY_HAVE_SIDE_EFFECT"
              |))).
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::zip::TrustedRandomAccessNoCoerce"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("value_MAY_HAVE_SIDE_EFFECT", InstanceField.Constant (value_MAY_HAVE_SIDE_EFFECT I))
            ].
      End Impl_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_where_core_iter_adapters_zip_TrustedRandomAccessNoCoerce_I_for_core_iter_adapters_fuse_Fuse_I.
      
      (* Trait *)
      (* Empty module 'FuseImpl' *)
      
      Module Impl_core_iter_adapters_fuse_FuseImpl_where_core_iter_traits_iterator_Iterator_I_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (*     type Item = <I as Iterator>::Item; *)
        Definition _Item (I : Ty.t) : Ty.t := Ty.associated.
        
        (*
            default fn next(&mut self) -> Option<<I as Iterator>::Item> {
                and_then_or_clear(&mut self.iter, Iterator::next)
            }
        *)
        Definition next (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_function (|
                  "core::iter::adapters::fuse::and_then_or_clear",
                  [
                    I;
                    Ty.associated;
                    Ty.function
                      [ Ty.apply (Ty.path "&mut") [] [ I ] ]
                      (Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ])
                  ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |);
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    I,
                    [],
                    "next",
                    []
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            default fn nth(&mut self, n: usize) -> Option<I::Item> {
                and_then_or_clear(&mut self.iter, |iter| iter.nth(n))
            }
        *)
        Definition nth (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_function (|
                  "core::iter::adapters::fuse::and_then_or_clear",
                  [
                    I;
                    Ty.associated;
                    Ty.function
                      [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ I ] ] ]
                      (Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ])
                  ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        I,
                                        [],
                                        "nth",
                                        []
                                      |),
                                      [ M.read (| iter |); M.read (| n |) ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            default fn try_fold<Acc, Fold, R>(&mut self, mut acc: Acc, fold: Fold) -> R
            where
                Self: Sized,
                Fold: FnMut(Acc, Self::Item) -> R,
                R: Try<Output = Acc>,
            {
                if let Some(ref mut iter) = self.iter {
                    acc = iter.try_fold(acc, fold)?;
                    self.iter = None;
                }
                try { acc }
            }
        *)
        Definition try_fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold; R ], [ self; acc; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let acc := M.alloc (| acc |) in
              let fold := M.alloc (| fold |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::iter::adapters::fuse::Fuse",
                                  "iter"
                                |) in
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let iter := M.alloc (| γ0_0 |) in
                              let~ _ :=
                                M.write (|
                                  acc,
                                  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::iter::traits::iterator::Iterator",
                                                I,
                                                [],
                                                "try_fold",
                                                [ Acc; Fold; R ]
                                              |),
                                              [
                                                M.read (| iter |);
                                                M.read (| acc |);
                                                M.read (| fold |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        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
                              let~ _ :=
                                M.write (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::adapters::fuse::Fuse",
                                    "iter"
                                  |),
                                  Value.StructTuple "core::option::Option::None" []
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          R,
                          [],
                          "from_output",
                          []
                        |),
                        [ M.read (| acc |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            default fn find<P>(&mut self, predicate: P) -> Option<Self::Item>
            where
                P: FnMut(&Self::Item) -> bool,
            {
                and_then_or_clear(&mut self.iter, |iter| iter.find(predicate))
            }
        *)
        Definition find (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.call_closure (|
                M.get_function (|
                  "core::iter::adapters::fuse::and_then_or_clear",
                  [
                    I;
                    Ty.associated;
                    Ty.function
                      [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ I ] ] ]
                      (Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ])
                  ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        I,
                                        [],
                                        "find",
                                        [ P ]
                                      |),
                                      [ M.read (| iter |); M.read (| predicate |) ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            default fn next_back(&mut self) -> Option<<I as Iterator>::Item>
            where
                I: DoubleEndedIterator,
            {
                and_then_or_clear(&mut self.iter, |iter| iter.next_back())
            }
        *)
        Definition next_back (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_function (|
                  "core::iter::adapters::fuse::and_then_or_clear",
                  [
                    I;
                    Ty.associated;
                    Ty.function
                      [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ I ] ] ]
                      (Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ])
                  ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::double_ended::DoubleEndedIterator",
                                        I,
                                        [],
                                        "next_back",
                                        []
                                      |),
                                      [ M.read (| iter |) ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            default fn nth_back(&mut self, n: usize) -> Option<<I as Iterator>::Item>
            where
                I: DoubleEndedIterator,
            {
                and_then_or_clear(&mut self.iter, |iter| iter.nth_back(n))
            }
        *)
        Definition nth_back (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.call_closure (|
                M.get_function (|
                  "core::iter::adapters::fuse::and_then_or_clear",
                  [
                    I;
                    Ty.associated;
                    Ty.function
                      [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ I ] ] ]
                      (Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ])
                  ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::double_ended::DoubleEndedIterator",
                                        I,
                                        [],
                                        "nth_back",
                                        []
                                      |),
                                      [ M.read (| iter |); M.read (| n |) ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            default fn try_rfold<Acc, Fold, R>(&mut self, mut acc: Acc, fold: Fold) -> R
            where
                Self: Sized,
                Fold: FnMut(Acc, Self::Item) -> R,
                R: Try<Output = Acc>,
                I: DoubleEndedIterator,
            {
                if let Some(ref mut iter) = self.iter {
                    acc = iter.try_rfold(acc, fold)?;
                    self.iter = None;
                }
                try { acc }
            }
        *)
        Definition try_rfold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold; R ], [ self; acc; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let acc := M.alloc (| acc |) in
              let fold := M.alloc (| fold |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::iter::adapters::fuse::Fuse",
                                  "iter"
                                |) in
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let iter := M.alloc (| γ0_0 |) in
                              let~ _ :=
                                M.write (|
                                  acc,
                                  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::iter::traits::double_ended::DoubleEndedIterator",
                                                I,
                                                [],
                                                "try_rfold",
                                                [ Acc; Fold; R ]
                                              |),
                                              [
                                                M.read (| iter |);
                                                M.read (| acc |);
                                                M.read (| fold |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        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
                              let~ _ :=
                                M.write (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::iter::adapters::fuse::Fuse",
                                    "iter"
                                  |),
                                  Value.StructTuple "core::option::Option::None" []
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          R,
                          [],
                          "from_output",
                          []
                        |),
                        [ M.read (| acc |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            default fn rfind<P>(&mut self, predicate: P) -> Option<Self::Item>
            where
                P: FnMut(&Self::Item) -> bool,
                I: DoubleEndedIterator,
            {
                and_then_or_clear(&mut self.iter, |iter| iter.rfind(predicate))
            }
        *)
        Definition rfind (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.call_closure (|
                M.get_function (|
                  "core::iter::adapters::fuse::and_then_or_clear",
                  [
                    I;
                    Ty.associated;
                    Ty.function
                      [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ I ] ] ]
                      (Ty.apply (Ty.path "core::option::Option") [] [ Ty.associated ])
                  ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::iter::adapters::fuse::Fuse",
                    "iter"
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::double_ended::DoubleEndedIterator",
                                        I,
                                        [],
                                        "rfind",
                                        [ P ]
                                      |),
                                      [ M.read (| iter |); M.read (| predicate |) ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::fuse::FuseImpl"
            (Self I)
            (* Trait polymorphic types *) [ (* I *) I ]
            (* Instance *)
            [
              ("Item", InstanceField.Ty (_Item I));
              ("next", InstanceField.Method (next I));
              ("nth", InstanceField.Method (nth I));
              ("try_fold", InstanceField.Method (try_fold I));
              ("find", InstanceField.Method (find I));
              ("next_back", InstanceField.Method (next_back I));
              ("nth_back", InstanceField.Method (nth_back I));
              ("try_rfold", InstanceField.Method (try_rfold I));
              ("rfind", InstanceField.Method (rfind I))
            ].
      End Impl_core_iter_adapters_fuse_FuseImpl_where_core_iter_traits_iterator_Iterator_I_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_adapters_fuse_FuseImpl_where_core_iter_traits_marker_FusedIterator_I_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (*
            fn next(&mut self) -> Option<<I as Iterator>::Item> {
                self.iter.as_mut()?.next()
            }
        *)
        Definition next (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      I,
                      [],
                      "next",
                      []
                    |),
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.apply (Ty.path "&mut") [] [ I ] ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::option::Option") [] [ I ],
                                    "as_mut",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::fuse::Fuse",
                                      "iter"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.associated ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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))
                          ]
                        |)
                      |)
                    ]
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth(&mut self, n: usize) -> Option<I::Item> {
                self.iter.as_mut()?.nth(n)
            }
        *)
        Definition nth (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      I,
                      [],
                      "nth",
                      []
                    |),
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.apply (Ty.path "&mut") [] [ I ] ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::option::Option") [] [ I ],
                                    "as_mut",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::fuse::Fuse",
                                      "iter"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.associated ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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))
                          ]
                        |)
                      |);
                      M.read (| n |)
                    ]
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_fold<Acc, Fold, R>(&mut self, mut acc: Acc, fold: Fold) -> R
            where
                Self: Sized,
                Fold: FnMut(Acc, Self::Item) -> R,
                R: Try<Output = Acc>,
            {
                if let Some(ref mut iter) = self.iter {
                    acc = iter.try_fold(acc, fold)?;
                }
                try { acc }
            }
        *)
        Definition try_fold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold; R ], [ self; acc; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let acc := M.alloc (| acc |) in
              let fold := M.alloc (| fold |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::iter::adapters::fuse::Fuse",
                                  "iter"
                                |) in
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let iter := M.alloc (| γ0_0 |) in
                              let~ _ :=
                                M.write (|
                                  acc,
                                  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::iter::traits::iterator::Iterator",
                                                I,
                                                [],
                                                "try_fold",
                                                [ Acc; Fold; R ]
                                              |),
                                              [
                                                M.read (| iter |);
                                                M.read (| acc |);
                                                M.read (| fold |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        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 (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          R,
                          [],
                          "from_output",
                          []
                        |),
                        [ M.read (| acc |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn find<P>(&mut self, predicate: P) -> Option<Self::Item>
            where
                P: FnMut(&Self::Item) -> bool,
            {
                self.iter.as_mut()?.find(predicate)
            }
        *)
        Definition find (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      I,
                      [],
                      "find",
                      [ P ]
                    |),
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.apply (Ty.path "&mut") [] [ I ] ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::option::Option") [] [ I ],
                                    "as_mut",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::fuse::Fuse",
                                      "iter"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.associated ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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))
                          ]
                        |)
                      |);
                      M.read (| predicate |)
                    ]
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn next_back(&mut self) -> Option<<I as Iterator>::Item>
            where
                I: DoubleEndedIterator,
            {
                self.iter.as_mut()?.next_back()
            }
        *)
        Definition next_back (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::double_ended::DoubleEndedIterator",
                      I,
                      [],
                      "next_back",
                      []
                    |),
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.apply (Ty.path "&mut") [] [ I ] ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::option::Option") [] [ I ],
                                    "as_mut",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::fuse::Fuse",
                                      "iter"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.associated ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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))
                          ]
                        |)
                      |)
                    ]
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn nth_back(&mut self, n: usize) -> Option<<I as Iterator>::Item>
            where
                I: DoubleEndedIterator,
            {
                self.iter.as_mut()?.nth_back(n)
            }
        *)
        Definition nth_back (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self; n ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let n := M.alloc (| n |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::double_ended::DoubleEndedIterator",
                      I,
                      [],
                      "nth_back",
                      []
                    |),
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.apply (Ty.path "&mut") [] [ I ] ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::option::Option") [] [ I ],
                                    "as_mut",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::fuse::Fuse",
                                      "iter"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.associated ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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))
                          ]
                        |)
                      |);
                      M.read (| n |)
                    ]
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn try_rfold<Acc, Fold, R>(&mut self, mut acc: Acc, fold: Fold) -> R
            where
                Self: Sized,
                Fold: FnMut(Acc, Self::Item) -> R,
                R: Try<Output = Acc>,
                I: DoubleEndedIterator,
            {
                if let Some(ref mut iter) = self.iter {
                    acc = iter.try_rfold(acc, fold)?;
                }
                try { acc }
            }
        *)
        Definition try_rfold (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ Acc; Fold; R ], [ self; acc; fold ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let acc := M.alloc (| acc |) in
              let fold := M.alloc (| fold |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::iter::adapters::fuse::Fuse",
                                  "iter"
                                |) in
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let iter := M.alloc (| γ0_0 |) in
                              let~ _ :=
                                M.write (|
                                  acc,
                                  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::iter::traits::double_ended::DoubleEndedIterator",
                                                I,
                                                [],
                                                "try_rfold",
                                                [ Acc; Fold; R ]
                                              |),
                                              [
                                                M.read (| iter |);
                                                M.read (| acc |);
                                                M.read (| fold |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        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 (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::try_trait::Try",
                          R,
                          [],
                          "from_output",
                          []
                        |),
                        [ M.read (| acc |) ]
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        (*
            fn rfind<P>(&mut self, predicate: P) -> Option<Self::Item>
            where
                P: FnMut(&Self::Item) -> bool,
                I: DoubleEndedIterator,
            {
                self.iter.as_mut()?.rfind(predicate)
            }
        *)
        Definition rfind (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [ P ], [ self; predicate ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let predicate := M.alloc (| predicate |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::double_ended::DoubleEndedIterator",
                      I,
                      [],
                      "rfind",
                      [ P ]
                    |),
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.apply (Ty.path "&mut") [] [ I ] ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::option::Option") [] [ I ],
                                    "as_mut",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::iter::adapters::fuse::Fuse",
                                      "iter"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.associated ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "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))
                          ]
                        |)
                      |);
                      M.read (| predicate |)
                    ]
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::fuse::FuseImpl"
            (Self I)
            (* Trait polymorphic types *) [ (* I *) I ]
            (* Instance *)
            [
              ("next", InstanceField.Method (next I));
              ("nth", InstanceField.Method (nth I));
              ("try_fold", InstanceField.Method (try_fold I));
              ("find", InstanceField.Method (find I));
              ("next_back", InstanceField.Method (next_back I));
              ("nth_back", InstanceField.Method (nth_back I));
              ("try_rfold", InstanceField.Method (try_rfold I));
              ("rfind", InstanceField.Method (rfind I))
            ].
      End Impl_core_iter_adapters_fuse_FuseImpl_where_core_iter_traits_marker_FusedIterator_I_I_for_core_iter_adapters_fuse_Fuse_I.
      
      Module Impl_core_iter_adapters_SourceIter_where_core_iter_adapters_SourceIter_I_where_core_iter_traits_marker_TrustedFused_I_for_core_iter_adapters_fuse_Fuse_I.
        Definition Self (I : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "core::iter::adapters::fuse::Fuse") [] [ I ].
        
        (*     type Source = I::Source; *)
        Definition _Source (I : Ty.t) : Ty.t := Ty.associated.
        
        (*
            unsafe fn as_inner(&mut self) -> &mut I::Source {
                // SAFETY: unsafe function forwarding to unsafe function with the same requirements.
                // TrustedFused guarantees that we'll never encounter a case where `self.iter` would
                // be set to None.
                unsafe { SourceIter::as_inner(self.iter.as_mut().unwrap_unchecked()) }
            }
        *)
        Definition as_inner (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self I in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (| "core::iter::adapters::SourceIter", I, [], "as_inner", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.apply (Ty.path "&mut") [] [ I ] ],
                      "unwrap_unchecked",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [] [ I ],
                          "as_mut",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::iter::adapters::fuse::Fuse",
                            "iter"
                          |)
                        ]
                      |)
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (I : Ty.t),
          M.IsTraitInstance
            "core::iter::adapters::SourceIter"
            (Self I)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Source", InstanceField.Ty (_Source I));
              ("as_inner", InstanceField.Method (as_inner I))
            ].
      End Impl_core_iter_adapters_SourceIter_where_core_iter_adapters_SourceIter_I_where_core_iter_traits_marker_TrustedFused_I_for_core_iter_adapters_fuse_Fuse_I.
      
      (*
      fn and_then_or_clear<T, U>(opt: &mut Option<T>, f: impl FnOnce(&mut T) -> Option<U>) -> Option<U> {
          let x = f(opt.as_mut()?);
          if x.is_none() {
              *opt = None;
          }
          x
      }
      *)
      Definition and_then_or_clear (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ T; U; impl_FnOnce__mut_T__arrow_Option_U_ ], [ opt; f ] =>
          ltac:(M.monadic
            (let opt := M.alloc (| opt |) in
            let f := M.alloc (| f |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ x :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          impl_FnOnce__mut_T__arrow_Option_U_,
                          [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ] ],
                          "call_once",
                          []
                        |),
                        [
                          M.read (| f |);
                          Value.Tuple
                            [
                              M.read (|
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::Try",
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                                        [],
                                        "branch",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply (Ty.path "core::option::Option") [] [ T ],
                                            "as_mut",
                                            []
                                          |),
                                          [ M.read (| opt |) ]
                                        |)
                                      ]
                                    |)
                                  |),
                                  [
                                    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",
                                                    Ty.apply
                                                      (Ty.path "core::option::Option")
                                                      []
                                                      [ U ],
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::option::Option")
                                                        []
                                                        [ Ty.path "core::convert::Infallible" ]
                                                    ],
                                                    "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
                                        M.alloc (| M.read (| val |) |)))
                                  ]
                                |)
                              |)
                            ]
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "core::option::Option") [] [ U ],
                                      "is_none",
                                      []
                                    |),
                                    [ x ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.write (|
                                M.read (| opt |),
                                Value.StructTuple "core::option::Option::None" []
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  x
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_and_then_or_clear :
        M.IsFunction "core::iter::adapters::fuse::and_then_or_clear" and_then_or_clear.
    End fuse.
  End adapters.
End iter.
