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

Module cmp.
  Module bytewise.
    (* Trait *)
    (* Empty module 'BytewiseEq' *)
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_u8.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_u16.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_u32.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_u64.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_u128.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_usize.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_i8.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_i16.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_i32.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_i64.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_i128.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_isize.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_bool.
      Definition Self : Ty.t := Ty.path "bool".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_bool.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_char.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_cmp_Ordering.
      Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_cmp_Ordering.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_u8.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u8" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_u8.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_u16.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u16" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_u16.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_u32.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u32" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_u32.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_u64.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u64" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_u64.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_u128.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u128" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_u128.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_usize.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_usize.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_i8.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "i8" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_i8.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_i16.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "i16" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_i16.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_i32.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "i32" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_i32.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_i64.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "i64" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_i64.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_i128.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "i128" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_i128.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_isize.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "isize" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_num_nonzero_NonZero_isize.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_u8.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u8" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_u8.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_u16.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u16" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_u16.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_u32.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u32" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_u32.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_u64.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u64" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_u64.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_u128.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u128" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_u128.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_usize.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_usize.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_i8.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "i8" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_i8.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_i16.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "i16" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_i16.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_i32.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "i32" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_i32.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_i64.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "i64" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_i64.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_i128.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "i128" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_i128.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_isize.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "isize" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_for_core_option_Option_core_num_nonzero_NonZero_isize.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_0_U_for_array_Usize_0_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 0 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 0 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_0_U_for_array_Usize_0_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_1_U_for_array_Usize_1_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 1 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 1 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_1_U_for_array_Usize_1_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_2_U_for_array_Usize_2_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_2_U_for_array_Usize_2_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_3_U_for_array_Usize_3_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 3 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 3 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_3_U_for_array_Usize_3_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_4_U_for_array_Usize_4_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_4_U_for_array_Usize_4_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_6_U_for_array_Usize_6_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 6 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 6 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_6_U_for_array_Usize_6_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_8_U_for_array_Usize_8_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_8_U_for_array_Usize_8_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_12_U_for_array_Usize_12_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 12 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 12 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_12_U_for_array_Usize_12_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_16_U_for_array_Usize_16_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_16_U_for_array_Usize_16_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_24_U_for_array_Usize_24_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 24 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 24 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_24_U_for_array_Usize_24_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_32_U_for_array_Usize_32_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_32_U_for_array_Usize_32_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_48_U_for_array_Usize_48_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 48 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 48 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_48_U_for_array_Usize_48_T.
    
    Module Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_64_U_for_array_Usize_64_T.
      Definition Self (T U : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 64 ] [ T ].
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::bytewise::BytewiseEq"
          (Self T U)
          (* Trait polymorphic types *)
          [ (* Rhs *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 64 ] [ U ] ]
          (* Instance *) [].
    End Impl_core_cmp_bytewise_BytewiseEq_where_core_cmp_bytewise_BytewiseEq_T_U_array_Usize_64_U_for_array_Usize_64_T.
  End bytewise.
End cmp.
