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

Module vec.
  Module partial_eq.
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A1_where_core_alloc_Allocator_A2_where_core_cmp_PartialEq_T_U_alloc_vec_Vec_U_A2_for_alloc_vec_Vec_T_A1.
      Definition Self (T U A1 A2 : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A1 ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      Definition eq (T U A1 A2 : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U A1 A2 in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A1 ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ U; A2 ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| other |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne (T U A1 A2 : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U A1 A2 in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A1 ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ U; A2 ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| other |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T U A1 A2 : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self T U A1 A2)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "alloc::vec::Vec") [] [ U; A2 ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq T U A1 A2)); ("ne", InstanceField.Method (ne T U A1 A2))
          ].
    End Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A1_where_core_alloc_Allocator_A2_where_core_cmp_PartialEq_T_U_alloc_vec_Vec_U_A2_for_alloc_vec_Vec_T_A1.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref__slice_U_for_alloc_vec_Vec_T_A.
      Definition Self (T U A : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne (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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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.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)); ("ne", InstanceField.Method (ne T U A)) ].
    End Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref__slice_U_for_alloc_vec_Vec_T_A.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref_mut_slice_U_for_alloc_vec_Vec_T_A.
      Definition Self (T U A : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne (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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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.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)); ("ne", InstanceField.Method (ne 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_vec_Vec_T_A.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_alloc_vec_Vec_U_A_for_ref__slice_T.
      Definition Self (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [
                    M.read (| M.read (| self |) |);
                    Value.StructTuple "core::ops::range::RangeFull" []
                  ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne (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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [
                    M.read (| M.read (| self |) |);
                    Value.StructTuple "core::ops::range::RangeFull" []
                  ]
                |);
                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.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)); ("ne", InstanceField.Method (ne 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_ref__slice_T.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_alloc_vec_Vec_U_A_for_ref_mut_slice_T.
      Definition Self (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [
                    M.read (| M.read (| self |) |);
                    Value.StructTuple "core::ops::range::RangeFull" []
                  ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne (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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [
                    M.read (| M.read (| self |) |);
                    Value.StructTuple "core::ops::range::RangeFull" []
                  ]
                |);
                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.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)); ("ne", InstanceField.Method (ne 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_ref_mut_slice_T.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_slice_U_for_alloc_vec_Vec_T_A.
      Definition Self (T U A : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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 (| other |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne (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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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 (| other |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              ]
            |)))
        | _, _, _ => 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 "slice") [] [ U ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq T U A)); ("ne", InstanceField.Method (ne T U A)) ].
    End Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_slice_U_for_alloc_vec_Vec_T_A.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_alloc_vec_Vec_U_A_for_slice_T.
      Definition Self (T U A : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne (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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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.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)); ("ne", InstanceField.Method (ne 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_slice_T.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_where_core_clone_Clone_T_alloc_vec_Vec_U_A_for_alloc_borrow_Cow_slice_T.
      Definition Self (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply
                          (Ty.path "alloc::borrow::Cow")
                          []
                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                        [],
                        "deref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    Value.StructTuple "core::ops::range::RangeFull" []
                  ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne (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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply
                          (Ty.path "alloc::borrow::Cow")
                          []
                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                        [],
                        "deref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    Value.StructTuple "core::ops::range::RangeFull" []
                  ]
                |);
                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.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)); ("ne", InstanceField.Method (ne T U A)) ].
    End Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_where_core_clone_Clone_T_alloc_vec_Vec_U_A_for_alloc_borrow_Cow_slice_T.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_where_core_clone_Clone_T_ref__slice_U_for_alloc_borrow_Cow_slice_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      Definition eq (T U : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply
                          (Ty.path "alloc::borrow::Cow")
                          []
                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                        [],
                        "deref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    Value.StructTuple "core::ops::range::RangeFull" []
                  ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne (T U : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply
                          (Ty.path "alloc::borrow::Cow")
                          []
                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                        [],
                        "deref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    Value.StructTuple "core::ops::range::RangeFull" []
                  ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ U ] ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq T U)); ("ne", InstanceField.Method (ne T U)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_where_core_clone_Clone_T_ref__slice_U_for_alloc_borrow_Cow_slice_T.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_where_core_clone_Clone_T_ref_mut_slice_U_for_alloc_borrow_Cow_slice_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      Definition eq (T U : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply
                          (Ty.path "alloc::borrow::Cow")
                          []
                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                        [],
                        "deref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    Value.StructTuple "core::ops::range::RangeFull" []
                  ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne (T U : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "slice") [] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply
                          (Ty.path "alloc::borrow::Cow")
                          []
                          [ Ty.apply (Ty.path "slice") [] [ T ] ],
                        [],
                        "deref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    Value.StructTuple "core::ops::range::RangeFull" []
                  ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ U ] ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq T U)); ("ne", InstanceField.Method (ne T U)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_where_core_clone_Clone_T_ref_mut_slice_U_for_alloc_borrow_Cow_slice_T.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_array_N_U_for_alloc_vec_Vec_T_A.
      Definition Self (N : Value.t) (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne
          (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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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.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)); ("ne", InstanceField.Method (ne 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_vec_Vec_T_A.
    
    Module Impl_core_cmp_PartialEq_where_core_alloc_Allocator_A_where_core_cmp_PartialEq_T_U_ref__array_N_U_for_alloc_vec_Vec_T_A.
      Definition Self (N : Value.t) (T U A : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ].
      
      (*             fn eq(&self, other: &$rhs) -> bool { self[..] == other[..] } *)
      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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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.impossible "wrong number of arguments"
        end.
      
      (*             fn ne(&self, other: &$rhs) -> bool { self[..] != other[..] } *)
      Definition ne
          (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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; A ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                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.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)); ("ne", InstanceField.Method (ne 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_vec_Vec_T_A.
  End partial_eq.
End vec.
