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

Module collections.
  Module vec_deque.
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_alloc_vec_Vec_U_A_for_alloc_collections_vec_deque_VecDeque_T_A.
      Definition Self (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
      
      (*
                  fn eq(&self, other: &$rhs) -> bool {
                      if self.len() != other.len() {
                          return false;
                      }
                      let (sa, sb) = self.as_slices();
                      let (oa, ob) = other[..].split_at(sa.len());
                      sa == oa && sb == ob
                  }
      *)
      Definition eq (T U A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U A in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::vec_deque::VecDeque")
                                          []
                                          [ T; A ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "alloc::vec::Vec") [] [ U; A ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| other |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Bool false |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                          "as_slices",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let sa := M.copy (| γ0_0 |) in
                          let sb := M.copy (| γ0_1 |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ U ],
                                  "split_at",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::index::Index",
                                      Ty.apply (Ty.path "alloc::vec::Vec") [] [ U; A ],
                                      [ Ty.path "core::ops::range::RangeFull" ],
                                      "index",
                                      []
                                    |),
                                    [
                                      M.read (| other |);
                                      Value.StructTuple "core::ops::range::RangeFull" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| sa |) ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let oa := M.copy (| γ0_0 |) in
                                  let ob := M.copy (| γ0_1 |) in
                                  M.alloc (|
                                    LogicalOp.and (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                          ],
                                          "eq",
                                          []
                                        |),
                                        [ sa; oa ]
                                      |),
                                      ltac:(M.monadic
                                        (M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                            ],
                                            "eq",
                                            []
                                          |),
                                          [ sb; ob ]
                                        |)))
                                    |)
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T U A : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self T U A)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "alloc::vec::Vec") [] [ U; A ] ]
          (* Instance *) [ ("eq", InstanceField.Method (eq T U A)) ].
    End Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_alloc_vec_Vec_U_A_for_alloc_collections_vec_deque_VecDeque_T_A.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref__slice_U_for_alloc_collections_vec_deque_VecDeque_T_A.
      Definition Self (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
      
      (*
                  fn eq(&self, other: &$rhs) -> bool {
                      if self.len() != other.len() {
                          return false;
                      }
                      let (sa, sb) = self.as_slices();
                      let (oa, ob) = other[..].split_at(sa.len());
                      sa == oa && sb == ob
                  }
      *)
      Definition eq (T U A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U A in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::vec_deque::VecDeque")
                                          []
                                          [ T; A ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ U ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| M.read (| other |) |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Bool false |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                          "as_slices",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let sa := M.copy (| γ0_0 |) in
                          let sb := M.copy (| γ0_1 |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ U ],
                                  "split_at",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::index::Index",
                                      Ty.apply (Ty.path "slice") [] [ U ],
                                      [ Ty.path "core::ops::range::RangeFull" ],
                                      "index",
                                      []
                                    |),
                                    [
                                      M.read (| M.read (| other |) |);
                                      Value.StructTuple "core::ops::range::RangeFull" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| sa |) ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let oa := M.copy (| γ0_0 |) in
                                  let ob := M.copy (| γ0_1 |) in
                                  M.alloc (|
                                    LogicalOp.and (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                          ],
                                          "eq",
                                          []
                                        |),
                                        [ sa; oa ]
                                      |),
                                      ltac:(M.monadic
                                        (M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                            ],
                                            "eq",
                                            []
                                          |),
                                          [ sb; ob ]
                                        |)))
                                    |)
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T U A : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self T U A)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ U ] ] ]
          (* Instance *) [ ("eq", InstanceField.Method (eq T U A)) ].
    End Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref__slice_U_for_alloc_collections_vec_deque_VecDeque_T_A.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref_mut_slice_U_for_alloc_collections_vec_deque_VecDeque_T_A.
      Definition Self (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
      
      (*
                  fn eq(&self, other: &$rhs) -> bool {
                      if self.len() != other.len() {
                          return false;
                      }
                      let (sa, sb) = self.as_slices();
                      let (oa, ob) = other[..].split_at(sa.len());
                      sa == oa && sb == ob
                  }
      *)
      Definition eq (T U A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U A in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::vec_deque::VecDeque")
                                          []
                                          [ T; A ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ U ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| M.read (| other |) |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Bool false |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                          "as_slices",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let sa := M.copy (| γ0_0 |) in
                          let sb := M.copy (| γ0_1 |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ U ],
                                  "split_at",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::index::Index",
                                      Ty.apply (Ty.path "slice") [] [ U ],
                                      [ Ty.path "core::ops::range::RangeFull" ],
                                      "index",
                                      []
                                    |),
                                    [
                                      M.read (| M.read (| other |) |);
                                      Value.StructTuple "core::ops::range::RangeFull" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| sa |) ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let oa := M.copy (| γ0_0 |) in
                                  let ob := M.copy (| γ0_1 |) in
                                  M.alloc (|
                                    LogicalOp.and (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                          ],
                                          "eq",
                                          []
                                        |),
                                        [ sa; oa ]
                                      |),
                                      ltac:(M.monadic
                                        (M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                            ],
                                            "eq",
                                            []
                                          |),
                                          [ sb; ob ]
                                        |)))
                                    |)
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T U A : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self T U A)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ U ] ] ]
          (* Instance *) [ ("eq", InstanceField.Method (eq T U A)) ].
    End Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref_mut_slice_U_for_alloc_collections_vec_deque_VecDeque_T_A.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_array_N_U_for_alloc_collections_vec_deque_VecDeque_T_A.
      Definition Self (N : Value.t) (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
      
      (*
                  fn eq(&self, other: &$rhs) -> bool {
                      if self.len() != other.len() {
                          return false;
                      }
                      let (sa, sb) = self.as_slices();
                      let (oa, ob) = other[..].split_at(sa.len());
                      sa == oa && sb == ob
                  }
      *)
      Definition eq
          (N : Value.t)
          (T U A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T U A in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::vec_deque::VecDeque")
                                          []
                                          [ T; A ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ U ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| other |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Bool false |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                          "as_slices",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let sa := M.copy (| γ0_0 |) in
                          let sb := M.copy (| γ0_1 |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ U ],
                                  "split_at",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::index::Index",
                                      Ty.apply (Ty.path "array") [ N ] [ U ],
                                      [ Ty.path "core::ops::range::RangeFull" ],
                                      "index",
                                      []
                                    |),
                                    [
                                      M.read (| other |);
                                      Value.StructTuple "core::ops::range::RangeFull" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| sa |) ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let oa := M.copy (| γ0_0 |) in
                                  let ob := M.copy (| γ0_1 |) in
                                  M.alloc (|
                                    LogicalOp.and (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                          ],
                                          "eq",
                                          []
                                        |),
                                        [ sa; oa ]
                                      |),
                                      ltac:(M.monadic
                                        (M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                            ],
                                            "eq",
                                            []
                                          |),
                                          [ sb; ob ]
                                        |)))
                                    |)
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U A : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self N T U A)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "array") [ N ] [ U ] ]
          (* Instance *) [ ("eq", InstanceField.Method (eq N T U A)) ].
    End Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_array_N_U_for_alloc_collections_vec_deque_VecDeque_T_A.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref__array_N_U_for_alloc_collections_vec_deque_VecDeque_T_A.
      Definition Self (N : Value.t) (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
      
      (*
                  fn eq(&self, other: &$rhs) -> bool {
                      if self.len() != other.len() {
                          return false;
                      }
                      let (sa, sb) = self.as_slices();
                      let (oa, ob) = other[..].split_at(sa.len());
                      sa == oa && sb == ob
                  }
      *)
      Definition eq
          (N : Value.t)
          (T U A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T U A in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::vec_deque::VecDeque")
                                          []
                                          [ T; A ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ U ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| M.read (| other |) |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Bool false |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                          "as_slices",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let sa := M.copy (| γ0_0 |) in
                          let sb := M.copy (| γ0_1 |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ U ],
                                  "split_at",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::index::Index",
                                      Ty.apply (Ty.path "array") [ N ] [ U ],
                                      [ Ty.path "core::ops::range::RangeFull" ],
                                      "index",
                                      []
                                    |),
                                    [
                                      M.read (| M.read (| other |) |);
                                      Value.StructTuple "core::ops::range::RangeFull" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| sa |) ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let oa := M.copy (| γ0_0 |) in
                                  let ob := M.copy (| γ0_1 |) in
                                  M.alloc (|
                                    LogicalOp.and (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                          ],
                                          "eq",
                                          []
                                        |),
                                        [ sa; oa ]
                                      |),
                                      ltac:(M.monadic
                                        (M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                            ],
                                            "eq",
                                            []
                                          |),
                                          [ sb; ob ]
                                        |)))
                                    |)
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U A : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self N T U A)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ U ] ] ]
          (* Instance *) [ ("eq", InstanceField.Method (eq N T U A)) ].
    End Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref__array_N_U_for_alloc_collections_vec_deque_VecDeque_T_A.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref_mut_array_N_U_for_alloc_collections_vec_deque_VecDeque_T_A.
      Definition Self (N : Value.t) (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ].
      
      (*
                  fn eq(&self, other: &$rhs) -> bool {
                      if self.len() != other.len() {
                          return false;
                      }
                      let (sa, sb) = self.as_slices();
                      let (oa, ob) = other[..].split_at(sa.len());
                      sa == oa && sb == ob
                  }
      *)
      Definition eq
          (N : Value.t)
          (T U A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T U A in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::vec_deque::VecDeque")
                                          []
                                          [ T; A ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ U ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| M.read (| other |) |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Bool false |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "alloc::collections::vec_deque::VecDeque") [] [ T; A ],
                          "as_slices",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                          let sa := M.copy (| γ0_0 |) in
                          let sb := M.copy (| γ0_1 |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ U ],
                                  "split_at",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::index::Index",
                                      Ty.apply (Ty.path "array") [ N ] [ U ],
                                      [ Ty.path "core::ops::range::RangeFull" ],
                                      "index",
                                      []
                                    |),
                                    [
                                      M.read (| M.read (| other |) |);
                                      Value.StructTuple "core::ops::range::RangeFull" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ T ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| sa |) ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let oa := M.copy (| γ0_0 |) in
                                  let ob := M.copy (| γ0_1 |) in
                                  M.alloc (|
                                    LogicalOp.and (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                          ],
                                          "eq",
                                          []
                                        |),
                                        [ sa; oa ]
                                      |),
                                      ltac:(M.monadic
                                        (M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::PartialEq",
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.apply (Ty.path "slice") [] [ T ] ],
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [ Ty.apply (Ty.path "slice") [] [ U ] ]
                                            ],
                                            "eq",
                                            []
                                          |),
                                          [ sb; ob ]
                                        |)))
                                    |)
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U A : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self N T U A)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "array") [ N ] [ U ] ] ]
          (* Instance *) [ ("eq", InstanceField.Method (eq N T U A)) ].
    End Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref_mut_array_N_U_for_alloc_collections_vec_deque_VecDeque_T_A.
  End vec_deque.
End collections.
