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

Module array.
  Module equality.
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_array_N_U_for_array_N_T.
      Definition Self (N : Value.t) (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
      
      (*
          fn eq(&self, other: &[U; N]) -> bool {
              SpecArrayEq::spec_eq(self, other)
          }
      *)
      Definition eq
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N 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::array::equality::SpecArrayEq",
                T,
                [ U ],
                "spec_eq",
                []
              |),
              [ M.read (| self |); M.read (| other |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn ne(&self, other: &[U; N]) -> bool {
              SpecArrayEq::spec_ne(self, other)
          }
      *)
      Definition ne
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N 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::array::equality::SpecArrayEq",
                T,
                [ U ],
                "spec_ne",
                []
              |),
              [ M.read (| self |); M.read (| other |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self N T U)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "array") [ N ] [ U ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq N T U)); ("ne", InstanceField.Method (ne N T U)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_array_N_U_for_array_N_T.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_slice_U_for_array_N_T.
      Definition Self (N : Value.t) (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
      
      (*
          fn eq(&self, other: &[U]) -> bool {
              let b: Result<&[U; N], _> = other.try_into();
              match b {
                  Ok(b) => *self == *b,
                  Err(_) => false,
              }
          }
      *)
      Definition eq
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T U in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ b :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::convert::TryInto",
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ U ] ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ U ] ] ],
                      "try_into",
                      []
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.match_operator (|
                b,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let b := M.copy (| γ0_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply (Ty.path "array") [ N ] [ T ],
                            [ Ty.apply (Ty.path "array") [ N ] [ U ] ],
                            "eq",
                            []
                          |),
                          [ M.read (| self |); M.read (| b |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Err",
                          0
                        |) in
                      M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn ne(&self, other: &[U]) -> bool {
              let b: Result<&[U; N], _> = other.try_into();
              match b {
                  Ok(b) => *self != *b,
                  Err(_) => true,
              }
          }
      *)
      Definition ne
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T U in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ b :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::convert::TryInto",
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ U ] ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ U ] ] ],
                      "try_into",
                      []
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.match_operator (|
                b,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let b := M.copy (| γ0_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply (Ty.path "array") [ N ] [ T ],
                            [ Ty.apply (Ty.path "array") [ N ] [ U ] ],
                            "ne",
                            []
                          |),
                          [ M.read (| self |); M.read (| b |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Err",
                          0
                        |) in
                      M.alloc (| Value.Bool true |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self N T U)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "slice") [] [ U ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq N T U)); ("ne", InstanceField.Method (ne N T U)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_slice_U_for_array_N_T.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_array_N_U_for_slice_T.
      Definition Self (N : Value.t) (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn eq(&self, other: &[U; N]) -> bool {
              let b: Result<&[T; N], _> = self.try_into();
              match b {
                  Ok(b) => *b == *other,
                  Err(_) => false,
              }
          }
      *)
      Definition eq
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T U in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ b :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::convert::TryInto",
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ] ],
                      "try_into",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.match_operator (|
                b,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let b := M.copy (| γ0_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply (Ty.path "array") [ N ] [ T ],
                            [ Ty.apply (Ty.path "array") [ N ] [ U ] ],
                            "eq",
                            []
                          |),
                          [ M.read (| b |); M.read (| other |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Err",
                          0
                        |) in
                      M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn ne(&self, other: &[U; N]) -> bool {
              let b: Result<&[T; N], _> = self.try_into();
              match b {
                  Ok(b) => *b != *other,
                  Err(_) => true,
              }
          }
      *)
      Definition ne
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T U in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ b :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::convert::TryInto",
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ] ],
                      "try_into",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.match_operator (|
                b,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let b := M.copy (| γ0_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply (Ty.path "array") [ N ] [ T ],
                            [ Ty.apply (Ty.path "array") [ N ] [ U ] ],
                            "ne",
                            []
                          |),
                          [ M.read (| b |); M.read (| other |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Err",
                          0
                        |) in
                      M.alloc (| Value.Bool true |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self N T U)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "array") [ N ] [ U ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq N T U)); ("ne", InstanceField.Method (ne N T U)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_array_N_U_for_slice_T.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_ref__slice_U_for_array_N_T.
      Definition Self (N : Value.t) (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
      
      (*
          fn eq(&self, other: &&[U]) -> bool {
              *self == **other
          }
      *)
      Definition eq
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N 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 "array") [ N ] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [ M.read (| self |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn ne(&self, other: &&[U]) -> bool {
              *self != **other
          }
      *)
      Definition ne
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N 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 "array") [ N ] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [ M.read (| self |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self N T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ U ] ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq N T U)); ("ne", InstanceField.Method (ne N T U)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_ref__slice_U_for_array_N_T.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_array_N_U_for_ref__slice_T.
      Definition Self (N : Value.t) (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
          fn eq(&self, other: &[U; N]) -> bool {
              **self == *other
          }
      *)
      Definition eq
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N 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 "array") [ N ] [ U ] ],
                "eq",
                []
              |),
              [ M.read (| M.read (| self |) |); M.read (| other |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn ne(&self, other: &[U; N]) -> bool {
              **self != *other
          }
      *)
      Definition ne
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N 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 "array") [ N ] [ U ] ],
                "ne",
                []
              |),
              [ M.read (| M.read (| self |) |); M.read (| other |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self N T U)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "array") [ N ] [ U ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq N T U)); ("ne", InstanceField.Method (ne N T U)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_array_N_U_for_ref__slice_T.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_ref_mut_slice_U_for_array_N_T.
      Definition Self (N : Value.t) (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
      
      (*
          fn eq(&self, other: &&mut [U]) -> bool {
              *self == **other
          }
      *)
      Definition eq
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N 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 "array") [ N ] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "eq",
                []
              |),
              [ M.read (| self |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn ne(&self, other: &&mut [U]) -> bool {
              *self != **other
          }
      *)
      Definition ne
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N 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 "array") [ N ] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ U ] ],
                "ne",
                []
              |),
              [ M.read (| self |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self N T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ U ] ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq N T U)); ("ne", InstanceField.Method (ne N T U)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_ref_mut_slice_U_for_array_N_T.
    
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_array_N_U_for_ref_mut_slice_T.
      Definition Self (N : Value.t) (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
      
      (*
          fn eq(&self, other: &[U; N]) -> bool {
              **self == *other
          }
      *)
      Definition eq
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N 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 "array") [ N ] [ U ] ],
                "eq",
                []
              |),
              [ M.read (| M.read (| self |) |); M.read (| other |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn ne(&self, other: &[U; N]) -> bool {
              **self != *other
          }
      *)
      Definition ne
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N 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 "array") [ N ] [ U ] ],
                "ne",
                []
              |),
              [ M.read (| M.read (| self |) |); M.read (| other |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self N T U)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "array") [ N ] [ U ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq N T U)); ("ne", InstanceField.Method (ne N T U)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_array_N_U_for_ref_mut_slice_T.
    
    Module Impl_core_cmp_Eq_where_core_cmp_Eq_T_for_array_N_T.
      Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
      
      Axiom Implements :
        forall (N : Value.t) (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::Eq"
          (Self N T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_Eq_where_core_cmp_Eq_T_for_array_N_T.
    
    (* Trait *)
    (* Empty module 'SpecArrayEq' *)
    
    Module Impl_core_array_equality_SpecArrayEq_where_core_cmp_PartialEq_T_Other_Other_for_T.
      Definition Self (N : Value.t) (T Other : Ty.t) : Ty.t := T.
      
      (*
          default fn spec_eq(a: &[Self; N], b: &[Other; N]) -> bool {
              a[..] == b[..]
          }
      *)
      Definition spec_eq
          (N : Value.t)
          (T Other : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T Other in
        match ε, τ, α with
        | [], [], [ a; b ] =>
          ltac:(M.monadic
            (let a := M.alloc (| a |) in
            let b := M.alloc (| b |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ Other ] ],
                "eq",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| a |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ Other ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| b |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          default fn spec_ne(a: &[Self; N], b: &[Other; N]) -> bool {
              a[..] != b[..]
          }
      *)
      Definition spec_ne
          (N : Value.t)
          (T Other : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T Other in
        match ε, τ, α with
        | [], [], [ a; b ] =>
          ltac:(M.monadic
            (let a := M.alloc (| a |) in
            let b := M.alloc (| b |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ Ty.apply (Ty.path "slice") [] [ Other ] ],
                "ne",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| a |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ Other ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| b |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T Other : Ty.t),
        M.IsTraitInstance
          "core::array::equality::SpecArrayEq"
          (Self N T Other)
          (* Trait polymorphic types *) [ (* Other *) Other ]
          (* Instance *)
          [
            ("spec_eq", InstanceField.Method (spec_eq N T Other));
            ("spec_ne", InstanceField.Method (spec_ne N T Other))
          ].
    End Impl_core_array_equality_SpecArrayEq_where_core_cmp_PartialEq_T_Other_Other_for_T.
    
    Module Impl_core_array_equality_SpecArrayEq_where_core_cmp_bytewise_BytewiseEq_T_U_U_for_T.
      Definition Self (N : Value.t) (T U : Ty.t) : Ty.t := T.
      
      (*
          fn spec_eq(a: &[T; N], b: &[U; N]) -> bool {
              // SAFETY: Arrays are compared element-wise, and don't add any padding
              // between elements, so when the elements are `BytewiseEq`, we can
              // compare the entire array at once.
              unsafe { crate::intrinsics::raw_eq(a, crate::mem::transmute(b)) }
          }
      *)
      Definition spec_eq
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T U in
        match ε, τ, α with
        | [], [], [ a; b ] =>
          ltac:(M.monadic
            (let a := M.alloc (| a |) in
            let b := M.alloc (| b |) in
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::raw_eq",
                [ Ty.apply (Ty.path "array") [ N ] [ T ] ]
              |),
              [
                M.read (| a |);
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::transmute",
                    [
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ U ] ];
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ]
                    ]
                  |),
                  [ M.read (| b |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn spec_ne(a: &[T; N], b: &[U; N]) -> bool {
              !Self::spec_eq(a, b)
          }
      *)
      Definition spec_ne
          (N : Value.t)
          (T U : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self N T U in
        match ε, τ, α with
        | [], [], [ a; b ] =>
          ltac:(M.monadic
            (let a := M.alloc (| a |) in
            let b := M.alloc (| b |) in
            UnOp.not (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::array::equality::SpecArrayEq",
                  T,
                  [ U ],
                  "spec_eq",
                  []
                |),
                [ M.read (| a |); M.read (| b |) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (N : Value.t) (T U : Ty.t),
        M.IsTraitInstance
          "core::array::equality::SpecArrayEq"
          (Self N T U)
          (* Trait polymorphic types *) [ (* Other *) U ]
          (* Instance *)
          [
            ("spec_eq", InstanceField.Method (spec_eq N T U));
            ("spec_ne", InstanceField.Method (spec_ne N T U))
          ].
    End Impl_core_array_equality_SpecArrayEq_where_core_cmp_bytewise_BytewiseEq_T_U_U_for_T.
  End equality.
End array.
