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

Module cmp.
  (* Trait *)
  Module PartialEq.
    Definition ne (Rhs Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          UnOp.not (|
            M.call_closure (|
              M.get_trait_method (| "core::cmp::PartialEq", Self, [ Rhs ], "eq", [] |),
              [ M.read (| self |); M.read (| other |) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_ne :
      forall (Rhs : Ty.t),
      M.IsProvidedMethod "core::cmp::PartialEq" "ne" (ne Rhs).
  End PartialEq.
  
  (* Trait *)
  Module Eq.
    Definition assert_receiver_is_total_eq
        (Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.Tuple []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_assert_receiver_is_total_eq :
      M.IsProvidedMethod "core::cmp::Eq" "assert_receiver_is_total_eq" assert_receiver_is_total_eq.
  End Eq.
  
  (* StructRecord
    {
      name := "AssertParamIsEq";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ ("_field", Ty.apply (Ty.path "core::marker::PhantomData") [] [ T ]) ];
    } *)
  
  (*
  Enum Ordering
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Less";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Equal";
          item := StructTuple [];
          discriminant := Some 0;
        };
        {
          name := "Greater";
          item := StructTuple [];
          discriminant := Some 1;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_core_cmp_Ordering.
    Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| M.read (| self |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_core_cmp_Ordering.
  
  Module Impl_core_marker_Copy_for_core_cmp_Ordering.
    Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_core_cmp_Ordering.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_cmp_Ordering.
    Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_cmp_Ordering.
  
  Module Impl_core_cmp_PartialEq_for_core_cmp_Ordering.
    Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "core::cmp::Ordering" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "core::cmp::Ordering" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_core_cmp_Ordering.
  
  Module Impl_core_cmp_Eq_for_core_cmp_Ordering.
    Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.Tuple []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_core_cmp_Ordering.
  
  Module Impl_core_cmp_PartialOrd_for_core_cmp_Ordering.
    Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
    
    (* PartialOrd *)
    Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "core::cmp::Ordering" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "core::cmp::Ordering" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialOrd",
                  Ty.path "i8",
                  [ Ty.path "i8" ],
                  "partial_cmp",
                  []
                |),
                [ __self_discr; __arg1_discr ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
  End Impl_core_cmp_PartialOrd_for_core_cmp_Ordering.
  
  Module Impl_core_cmp_Ord_for_core_cmp_Ordering.
    Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
    
    (* Ord *)
    Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "core::cmp::Ordering" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "core::cmp::Ordering" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::cmp::Ord", Ty.path "i8", [], "cmp", [] |),
                [ __self_discr; __arg1_discr ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Ord"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
  End Impl_core_cmp_Ord_for_core_cmp_Ordering.
  
  Module Impl_core_fmt_Debug_for_core_cmp_Ordering.
    Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
            [
              M.read (| f |);
              M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
                        M.alloc (| M.read (| Value.String "Less" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                        M.alloc (| M.read (| Value.String "Equal" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
                        M.alloc (| M.read (| Value.String "Greater" |) |)))
                  ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_core_cmp_Ordering.
  
  Module Impl_core_hash_Hash_for_core_cmp_Ordering.
    Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "core::cmp::Ordering" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Ty.path "i8", [], "hash", [ __H ] |),
                [ __self_discr; M.read (| state |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_core_cmp_Ordering.
  
  Module Impl_core_cmp_Ordering.
    Definition Self : Ty.t := Ty.path "core::cmp::Ordering".
    
    (*
        pub const fn is_eq(self) -> bool {
            matches!(self, Equal)
        }
    *)
    Definition is_eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_eq : M.IsAssociatedFunction Self "is_eq" is_eq.
    
    (*
        pub const fn is_ne(self) -> bool {
            !matches!(self, Equal)
        }
    *)
    Definition is_ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          UnOp.not (|
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                      M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_ne : M.IsAssociatedFunction Self "is_ne" is_ne.
    
    (*
        pub const fn is_lt(self) -> bool {
            matches!(self, Less)
        }
    *)
    Definition is_lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_lt : M.IsAssociatedFunction Self "is_lt" is_lt.
    
    (*
        pub const fn is_gt(self) -> bool {
            matches!(self, Greater)
        }
    *)
    Definition is_gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_gt : M.IsAssociatedFunction Self "is_gt" is_gt.
    
    (*
        pub const fn is_le(self) -> bool {
            !matches!(self, Greater)
        }
    *)
    Definition is_le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          UnOp.not (|
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
                      M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_le : M.IsAssociatedFunction Self "is_le" is_le.
    
    (*
        pub const fn is_ge(self) -> bool {
            !matches!(self, Less)
        }
    *)
    Definition is_ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          UnOp.not (|
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
                      M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_ge : M.IsAssociatedFunction Self "is_ge" is_ge.
    
    (*
        pub const fn reverse(self) -> Ordering {
            match self {
                Less => Greater,
                Equal => Equal,
                Greater => Less,
            }
        }
    *)
    Definition reverse (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
                    M.alloc (| Value.StructTuple "core::cmp::Ordering::Greater" [] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                    M.alloc (| Value.StructTuple "core::cmp::Ordering::Equal" [] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
                    M.alloc (| Value.StructTuple "core::cmp::Ordering::Less" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_reverse : M.IsAssociatedFunction Self "reverse" reverse.
    
    (*
        pub const fn then(self, other: Ordering) -> Ordering {
            match self {
                Equal => other,
                _ => self,
            }
        }
    *)
    Definition then_ (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                    other));
                fun γ => ltac:(M.monadic self)
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_then_ : M.IsAssociatedFunction Self "then_" then_.
    
    (*
        pub fn then_with<F: FnOnce() -> Ordering>(self, f: F) -> Ordering {
            match self {
                Equal => f(),
                _ => self,
            }
        }
    *)
    Definition then_with (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          F,
                          [ Ty.tuple [] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [] ]
                      |)
                    |)));
                fun γ => ltac:(M.monadic self)
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_then_with : M.IsAssociatedFunction Self "then_with" then_with.
  End Impl_core_cmp_Ordering.
  
  (* StructTuple
    {
      name := "Reverse";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ T ];
    } *)
  
  Module Impl_core_marker_StructuralPartialEq_for_core_cmp_Reverse_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cmp::Reverse") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_cmp_Reverse_T.
  
  Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_for_core_cmp_Reverse_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cmp::Reverse") [] [ T ].
    
    (* PartialEq *)
    Definition eq (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T 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", T, [ T ], "eq", [] |),
            [
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "core::cmp::Reverse", 0 |);
              M.SubPointer.get_struct_tuple_field (| M.read (| other |), "core::cmp::Reverse", 0 |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method (eq T)) ].
  End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_for_core_cmp_Reverse_T.
  
  Module Impl_core_cmp_Eq_where_core_cmp_Eq_T_for_core_cmp_Reverse_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cmp::Reverse") [] [ T ].
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::Eq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method (assert_receiver_is_total_eq T)) ].
  End Impl_core_cmp_Eq_where_core_cmp_Eq_T_for_core_cmp_Reverse_T.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_cmp_Reverse_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cmp::Reverse") [] [ T ].
    
    (* Debug *)
    Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_tuple_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "Reverse" |);
              M.alloc (|
                M.SubPointer.get_struct_tuple_field (| M.read (| self |), "core::cmp::Reverse", 0 |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_cmp_Reverse_T.
  
  Module Impl_core_marker_Copy_where_core_marker_Copy_T_for_core_cmp_Reverse_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cmp::Reverse") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Copy_T_for_core_cmp_Reverse_T.
  
  Module Impl_core_default_Default_where_core_default_Default_T_for_core_cmp_Reverse_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cmp::Reverse") [] [ T ].
    
    (* Default *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructTuple
            "core::cmp::Reverse"
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
  End Impl_core_default_Default_where_core_default_Default_T_for_core_cmp_Reverse_T.
  
  Module Impl_core_hash_Hash_where_core_hash_Hash_T_for_core_cmp_Reverse_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cmp::Reverse") [] [ T ].
    
    (* Hash *)
    Definition hash (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.call_closure (|
            M.get_trait_method (| "core::hash::Hash", T, [], "hash", [ __H ] |),
            [
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "core::cmp::Reverse", 0 |);
              M.read (| state |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash T)) ].
  End Impl_core_hash_Hash_where_core_hash_Hash_T_for_core_cmp_Reverse_T.
  
  Module Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_for_core_cmp_Reverse_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cmp::Reverse") [] [ T ].
    
    (*
        fn partial_cmp(&self, other: &Reverse<T>) -> Option<Ordering> {
            other.0.partial_cmp(&self.0)
        }
    *)
    Definition partial_cmp (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T 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::PartialOrd", T, [ T ], "partial_cmp", [] |),
            [
              M.SubPointer.get_struct_tuple_field (| M.read (| other |), "core::cmp::Reverse", 0 |);
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "core::cmp::Reverse", 0 |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn lt(&self, other: &Self) -> bool {
            other.0 < self.0
        }
    *)
    Definition lt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T 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::PartialOrd", T, [ T ], "lt", [] |),
            [
              M.SubPointer.get_struct_tuple_field (| M.read (| other |), "core::cmp::Reverse", 0 |);
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "core::cmp::Reverse", 0 |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn le(&self, other: &Self) -> bool {
            other.0 <= self.0
        }
    *)
    Definition le (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T 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::PartialOrd", T, [ T ], "le", [] |),
            [
              M.SubPointer.get_struct_tuple_field (| M.read (| other |), "core::cmp::Reverse", 0 |);
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "core::cmp::Reverse", 0 |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn gt(&self, other: &Self) -> bool {
            other.0 > self.0
        }
    *)
    Definition gt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T 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::PartialOrd", T, [ T ], "gt", [] |),
            [
              M.SubPointer.get_struct_tuple_field (| M.read (| other |), "core::cmp::Reverse", 0 |);
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "core::cmp::Reverse", 0 |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn ge(&self, other: &Self) -> bool {
            other.0 >= self.0
        }
    *)
    Definition ge (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T 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::PartialOrd", T, [ T ], "ge", [] |),
            [
              M.SubPointer.get_struct_tuple_field (| M.read (| other |), "core::cmp::Reverse", 0 |);
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "core::cmp::Reverse", 0 |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("partial_cmp", InstanceField.Method (partial_cmp T));
          ("lt", InstanceField.Method (lt T));
          ("le", InstanceField.Method (le T));
          ("gt", InstanceField.Method (gt T));
          ("ge", InstanceField.Method (ge T))
        ].
  End Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_for_core_cmp_Reverse_T.
  
  Module Impl_core_cmp_Ord_where_core_cmp_Ord_T_for_core_cmp_Reverse_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cmp::Reverse") [] [ T ].
    
    (*
        fn cmp(&self, other: &Reverse<T>) -> Ordering {
            other.0.cmp(&self.0)
        }
    *)
    Definition cmp (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T 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::Ord", T, [], "cmp", [] |),
            [
              M.SubPointer.get_struct_tuple_field (| M.read (| other |), "core::cmp::Reverse", 0 |);
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "core::cmp::Reverse", 0 |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::Ord"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method (cmp T)) ].
  End Impl_core_cmp_Ord_where_core_cmp_Ord_T_for_core_cmp_Reverse_T.
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_cmp_Reverse_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cmp::Reverse") [] [ T ].
    
    (*
        fn clone(&self) -> Reverse<T> {
            Reverse(self.0.clone())
        }
    *)
    Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructTuple
            "core::cmp::Reverse"
            [
              M.call_closure (|
                M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                [
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::cmp::Reverse",
                    0
                  |)
                ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn clone_from(&mut self, source: &Self) {
            self.0.clone_from(&source.0)
        }
    *)
    Definition clone_from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; source ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let source := M.alloc (| source |) in
          M.call_closure (|
            M.get_trait_method (| "core::clone::Clone", T, [], "clone_from", [] |),
            [
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "core::cmp::Reverse", 0 |);
              M.SubPointer.get_struct_tuple_field (| M.read (| source |), "core::cmp::Reverse", 0 |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("clone", InstanceField.Method (clone T));
          ("clone_from", InstanceField.Method (clone_from T))
        ].
  End Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_cmp_Reverse_T.
  
  (* Trait *)
  Module Ord.
    Definition max (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_function (|
              "core::cmp::max_by",
              [
                Self;
                Ty.function
                  [ Ty.apply (Ty.path "&") [] [ Self ]; Ty.apply (Ty.path "&") [] [ Self ] ]
                  (Ty.path "core::cmp::Ordering")
              ]
            |),
            [
              M.read (| self |);
              M.read (| other |);
              M.get_trait_method (| "core::cmp::Ord", Self, [], "cmp", [] |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_max : M.IsProvidedMethod "core::cmp::Ord" "max" max.
    Definition min (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_function (|
              "core::cmp::min_by",
              [
                Self;
                Ty.function
                  [ Ty.apply (Ty.path "&") [] [ Self ]; Ty.apply (Ty.path "&") [] [ Self ] ]
                  (Ty.path "core::cmp::Ordering")
              ]
            |),
            [
              M.read (| self |);
              M.read (| other |);
              M.get_trait_method (| "core::cmp::Ord", Self, [], "cmp", [] |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_min : M.IsProvidedMethod "core::cmp::Ord" "min" min.
    Definition clamp (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; min; max ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let min := M.alloc (| min |) in
          let max := M.alloc (| max |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialOrd",
                                  Self,
                                  [ Self ],
                                  "le",
                                  []
                                |),
                                [ min; max ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic", [] |),
                            [ M.read (| Value.String "assertion failed: min <= max" |) ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::cmp::PartialOrd",
                              Self,
                              [ Self ],
                              "lt",
                              []
                            |),
                            [ self; min ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    min));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialOrd",
                                      Self,
                                      [ Self ],
                                      "gt",
                                      []
                                    |),
                                    [ self; max ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            max));
                        fun γ => ltac:(M.monadic self)
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_clamp : M.IsProvidedMethod "core::cmp::Ord" "clamp" clamp.
  End Ord.
  
  (* Trait *)
  Module PartialOrd.
    Definition lt (Rhs Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialOrd",
                    Self,
                    [ Rhs ],
                    "partial_cmp",
                    []
                  |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::cmp::Ordering::Less" |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_lt :
      forall (Rhs : Ty.t),
      M.IsProvidedMethod "core::cmp::PartialOrd" "lt" (lt Rhs).
    Definition le (Rhs Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialOrd",
                    Self,
                    [ Rhs ],
                    "partial_cmp",
                    []
                  |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    M.find_or_pattern (|
                      γ0_0,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_le :
      forall (Rhs : Ty.t),
      M.IsProvidedMethod "core::cmp::PartialOrd" "le" (le Rhs).
    Definition gt (Rhs Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialOrd",
                    Self,
                    [ Rhs ],
                    "partial_cmp",
                    []
                  |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::cmp::Ordering::Greater" |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_gt :
      forall (Rhs : Ty.t),
      M.IsProvidedMethod "core::cmp::PartialOrd" "gt" (gt Rhs).
    Definition ge (Rhs Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialOrd",
                    Self,
                    [ Rhs ],
                    "partial_cmp",
                    []
                  |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    M.find_or_pattern (|
                      γ0_0,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
                            Value.Tuple []));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                            Value.Tuple []))
                      ],
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_ge :
      forall (Rhs : Ty.t),
      M.IsProvidedMethod "core::cmp::PartialOrd" "ge" (ge Rhs).
  End PartialOrd.
  
  (*
  pub fn min<T: Ord>(v1: T, v2: T) -> T {
      v1.min(v2)
  }
  *)
  Definition min (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ v1; v2 ] =>
      ltac:(M.monadic
        (let v1 := M.alloc (| v1 |) in
        let v2 := M.alloc (| v2 |) in
        M.call_closure (|
          M.get_trait_method (| "core::cmp::Ord", T, [], "min", [] |),
          [ M.read (| v1 |); M.read (| v2 |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_min : M.IsFunction "core::cmp::min" min.
  
  (*
  pub fn min_by<T, F: FnOnce(&T, &T) -> Ordering>(v1: T, v2: T, compare: F) -> T {
      match compare(&v1, &v2) {
          Ordering::Less | Ordering::Equal => v1,
          Ordering::Greater => v2,
      }
  }
  *)
  Definition min_by (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; F ], [ v1; v2; compare ] =>
      ltac:(M.monadic
        (let v1 := M.alloc (| v1 |) in
        let v2 := M.alloc (| v2 |) in
        let compare := M.alloc (| compare |) in
        M.read (|
          M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::FnOnce",
                  F,
                  [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ] ],
                  "call_once",
                  []
                |),
                [ M.read (| compare |); Value.Tuple [ v1; v2 ] ]
              |)
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (M.find_or_pattern (|
                    γ,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                          Value.Tuple []))
                    ],
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [] => ltac:(M.monadic v1)
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
                  v2))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_min_by : M.IsFunction "core::cmp::min_by" min_by.
  
  (*
  pub fn min_by_key<T, F: FnMut(&T) -> K, K: Ord>(v1: T, v2: T, mut f: F) -> T {
      min_by(v1, v2, |v1, v2| f(v1).cmp(&f(v2)))
  }
  *)
  Definition min_by_key (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; F; K ], [ v1; v2; f ] =>
      ltac:(M.monadic
        (let v1 := M.alloc (| v1 |) in
        let v2 := M.alloc (| v2 |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_function (|
            "core::cmp::min_by",
            [
              T;
              Ty.function
                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ] ]
                (Ty.path "core::cmp::Ordering")
            ]
          |),
          [
            M.read (| v1 |);
            M.read (| v2 |);
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0; α1 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let v1 := M.copy (| γ |) in
                              M.match_operator (|
                                M.alloc (| α1 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let v2 := M.copy (| γ |) in
                                      M.call_closure (|
                                        M.get_trait_method (| "core::cmp::Ord", K, [], "cmp", [] |),
                                        [
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnMut",
                                                F,
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                                                "call_mut",
                                                []
                                              |),
                                              [ f; Value.Tuple [ M.read (| v1 |) ] ]
                                            |)
                                          |);
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnMut",
                                                F,
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                                                "call_mut",
                                                []
                                              |),
                                              [ f; Value.Tuple [ M.read (| v2 |) ] ]
                                            |)
                                          |)
                                        ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_min_by_key : M.IsFunction "core::cmp::min_by_key" min_by_key.
  
  (*
  pub fn max<T: Ord>(v1: T, v2: T) -> T {
      v1.max(v2)
  }
  *)
  Definition max (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ v1; v2 ] =>
      ltac:(M.monadic
        (let v1 := M.alloc (| v1 |) in
        let v2 := M.alloc (| v2 |) in
        M.call_closure (|
          M.get_trait_method (| "core::cmp::Ord", T, [], "max", [] |),
          [ M.read (| v1 |); M.read (| v2 |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_max : M.IsFunction "core::cmp::max" max.
  
  (*
  pub fn max_by<T, F: FnOnce(&T, &T) -> Ordering>(v1: T, v2: T, compare: F) -> T {
      match compare(&v1, &v2) {
          Ordering::Less | Ordering::Equal => v2,
          Ordering::Greater => v1,
      }
  }
  *)
  Definition max_by (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; F ], [ v1; v2; compare ] =>
      ltac:(M.monadic
        (let v1 := M.alloc (| v1 |) in
        let v2 := M.alloc (| v2 |) in
        let compare := M.alloc (| compare |) in
        M.read (|
          M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::FnOnce",
                  F,
                  [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ] ],
                  "call_once",
                  []
                |),
                [ M.read (| compare |); Value.Tuple [ v1; v2 ] ]
              |)
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (M.find_or_pattern (|
                    γ,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                          Value.Tuple []))
                    ],
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [] => ltac:(M.monadic v2)
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ := M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
                  v1))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_max_by : M.IsFunction "core::cmp::max_by" max_by.
  
  (*
  pub fn max_by_key<T, F: FnMut(&T) -> K, K: Ord>(v1: T, v2: T, mut f: F) -> T {
      max_by(v1, v2, |v1, v2| f(v1).cmp(&f(v2)))
  }
  *)
  Definition max_by_key (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; F; K ], [ v1; v2; f ] =>
      ltac:(M.monadic
        (let v1 := M.alloc (| v1 |) in
        let v2 := M.alloc (| v2 |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_function (|
            "core::cmp::max_by",
            [
              T;
              Ty.function
                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ] ]
                (Ty.path "core::cmp::Ordering")
            ]
          |),
          [
            M.read (| v1 |);
            M.read (| v2 |);
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0; α1 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let v1 := M.copy (| γ |) in
                              M.match_operator (|
                                M.alloc (| α1 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let v2 := M.copy (| γ |) in
                                      M.call_closure (|
                                        M.get_trait_method (| "core::cmp::Ord", K, [], "cmp", [] |),
                                        [
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnMut",
                                                F,
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                                                "call_mut",
                                                []
                                              |),
                                              [ f; Value.Tuple [ M.read (| v1 |) ] ]
                                            |)
                                          |);
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnMut",
                                                F,
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                                                "call_mut",
                                                []
                                              |),
                                              [ f; Value.Tuple [ M.read (| v2 |) ] ]
                                            |)
                                          |)
                                        ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_max_by_key : M.IsFunction "core::cmp::max_by_key" max_by_key.
  
  (*
  pub fn minmax<T>(v1: T, v2: T) -> [T; 2]
  where
      T: Ord,
  {
      if v1 <= v2 { [v1, v2] } else { [v2, v1] }
  }
  *)
  Definition minmax (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ v1; v2 ] =>
      ltac:(M.monadic
        (let v1 := M.alloc (| v1 |) in
        let v2 := M.alloc (| v2 |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (| "core::cmp::PartialOrd", T, [ T ], "le", [] |),
                          [ v1; v2 ]
                        |)
                      |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (| Value.Array [ M.read (| v1 |); M.read (| v2 |) ] |)));
              fun γ =>
                ltac:(M.monadic (M.alloc (| Value.Array [ M.read (| v2 |); M.read (| v1 |) ] |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_minmax : M.IsFunction "core::cmp::minmax" minmax.
  
  (*
  pub fn minmax_by<T, F>(v1: T, v2: T, compare: F) -> [T; 2]
  where
      F: FnOnce(&T, &T) -> Ordering,
  {
      if compare(&v1, &v2).is_le() { [v1, v2] } else { [v2, v1] }
  }
  *)
  Definition minmax_by (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; F ], [ v1; v2; compare ] =>
      ltac:(M.monadic
        (let v1 := M.alloc (| v1 |) in
        let v2 := M.alloc (| v2 |) in
        let compare := M.alloc (| compare |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::cmp::Ordering",
                            "is_le",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::function::FnOnce",
                                F,
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply (Ty.path "&") [] [ T ];
                                      Ty.apply (Ty.path "&") [] [ T ]
                                    ]
                                ],
                                "call_once",
                                []
                              |),
                              [ M.read (| compare |); Value.Tuple [ v1; v2 ] ]
                            |)
                          ]
                        |)
                      |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (| Value.Array [ M.read (| v1 |); M.read (| v2 |) ] |)));
              fun γ =>
                ltac:(M.monadic (M.alloc (| Value.Array [ M.read (| v2 |); M.read (| v1 |) ] |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_minmax_by : M.IsFunction "core::cmp::minmax_by" minmax_by.
  
  (*
  pub fn minmax_by_key<T, F, K>(v1: T, v2: T, mut f: F) -> [T; 2]
  where
      F: FnMut(&T) -> K,
      K: Ord,
  {
      minmax_by(v1, v2, |v1, v2| f(v1).cmp(&f(v2)))
  }
  *)
  Definition minmax_by_key (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; F; K ], [ v1; v2; f ] =>
      ltac:(M.monadic
        (let v1 := M.alloc (| v1 |) in
        let v2 := M.alloc (| v2 |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_function (|
            "core::cmp::minmax_by",
            [
              T;
              Ty.function
                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ]; Ty.apply (Ty.path "&") [] [ T ] ] ]
                (Ty.path "core::cmp::Ordering")
            ]
          |),
          [
            M.read (| v1 |);
            M.read (| v2 |);
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0; α1 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let v1 := M.copy (| γ |) in
                              M.match_operator (|
                                M.alloc (| α1 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let v2 := M.copy (| γ |) in
                                      M.call_closure (|
                                        M.get_trait_method (| "core::cmp::Ord", K, [], "cmp", [] |),
                                        [
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnMut",
                                                F,
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                                                "call_mut",
                                                []
                                              |),
                                              [ f; Value.Tuple [ M.read (| v1 |) ] ]
                                            |)
                                          |);
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnMut",
                                                F,
                                                [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                                                "call_mut",
                                                []
                                              |),
                                              [ f; Value.Tuple [ M.read (| v2 |) ] ]
                                            |)
                                          |)
                                        ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_minmax_by_key : M.IsFunction "core::cmp::minmax_by_key" minmax_by_key.
  
  Module impls.
    Module Impl_core_cmp_PartialEq_for_Tuple_.
      Definition Self : Ty.t := Ty.tuple [].
      
      (*
              fn eq(&self, _other: &()) -> bool {
                  true
              }
      *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _other := M.alloc (| _other |) in
            Value.Bool true))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn ne(&self, _other: &()) -> bool {
                  false
              }
      *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _other := M.alloc (| _other |) in
            Value.Bool false))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_Tuple_.
    
    Module Impl_core_cmp_PartialEq_for_bool.
      Definition Self : Ty.t := Ty.path "bool".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_bool.
    
    Module Impl_core_cmp_PartialEq_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_char.
    
    Module Impl_core_cmp_PartialEq_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_usize.
    
    Module Impl_core_cmp_PartialEq_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_u8.
    
    Module Impl_core_cmp_PartialEq_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_u16.
    
    Module Impl_core_cmp_PartialEq_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_u32.
    
    Module Impl_core_cmp_PartialEq_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_u64.
    
    Module Impl_core_cmp_PartialEq_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_u128.
    
    Module Impl_core_cmp_PartialEq_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_isize.
    
    Module Impl_core_cmp_PartialEq_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_i8.
    
    Module Impl_core_cmp_PartialEq_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_i16.
    
    Module Impl_core_cmp_PartialEq_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_i32.
    
    Module Impl_core_cmp_PartialEq_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_i64.
    
    Module Impl_core_cmp_PartialEq_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_i128.
    
    Module Impl_core_cmp_PartialEq_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_f16.
    
    Module Impl_core_cmp_PartialEq_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_f32.
    
    Module Impl_core_cmp_PartialEq_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_f64.
    
    Module Impl_core_cmp_PartialEq_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*                 fn eq(&self, other: &$t) -> bool { ( *self) == ( *other) } *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ne(&self, other: &$t) -> bool { ( *self) != ( *other) } *)
      Definition ne (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ne (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq); ("ne", InstanceField.Method ne) ].
    End Impl_core_cmp_PartialEq_for_f128.
    
    Module Impl_core_cmp_Eq_for_Tuple_.
      Definition Self : Ty.t := Ty.tuple [].
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_Tuple_.
    
    Module Impl_core_cmp_Eq_for_bool.
      Definition Self : Ty.t := Ty.path "bool".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_bool.
    
    Module Impl_core_cmp_Eq_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_char.
    
    Module Impl_core_cmp_Eq_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_usize.
    
    Module Impl_core_cmp_Eq_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_u8.
    
    Module Impl_core_cmp_Eq_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_u16.
    
    Module Impl_core_cmp_Eq_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_u32.
    
    Module Impl_core_cmp_Eq_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_u64.
    
    Module Impl_core_cmp_Eq_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_u128.
    
    Module Impl_core_cmp_Eq_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_isize.
    
    Module Impl_core_cmp_Eq_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_i8.
    
    Module Impl_core_cmp_Eq_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_i16.
    
    Module Impl_core_cmp_Eq_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_i32.
    
    Module Impl_core_cmp_Eq_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_i64.
    
    Module Impl_core_cmp_Eq_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_i128.
    
    Module Impl_core_cmp_PartialOrd_for_Tuple_.
      Definition Self : Ty.t := Ty.tuple [].
      
      (*
              fn partial_cmp(&self, _: &()) -> Option<Ordering> {
                  Some(Equal)
              }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; β1 ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let β1 := M.alloc (| β1 |) in
            M.match_operator (|
              β1,
              [
                fun γ =>
                  ltac:(M.monadic
                    (Value.StructTuple
                      "core::option::Option::Some"
                      [ Value.StructTuple "core::cmp::Ordering::Equal" [] ]))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
    End Impl_core_cmp_PartialOrd_for_Tuple_.
    
    Module Impl_core_cmp_PartialOrd_for_bool.
      Definition Self : Ty.t := Ty.path "bool".
      
      (*
              fn partial_cmp(&self, other: &bool) -> Option<Ordering> {
                  Some(self.cmp(other))
              }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_trait_method (| "core::cmp::Ord", Ty.path "bool", [], "cmp", [] |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
    End Impl_core_cmp_PartialOrd_for_bool.
    
    Module Impl_core_cmp_PartialOrd_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          match ( *self <= *other, *self >= *other) {
                              (false, false) => None,
                              (false, true) => Some(Greater),
                              (true, false) => Some(Less),
                              (true, true) => Some(Equal),
                          }
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      BinOp.le (|
                        M.read (| M.read (| self |) |),
                        M.read (| M.read (| other |) |)
                      |);
                      BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)
                    ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool false |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool false |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool false |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Greater" [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool true |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool false |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Less" [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool true |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Equal" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_f16.
    
    Module Impl_core_cmp_PartialOrd_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          match ( *self <= *other, *self >= *other) {
                              (false, false) => None,
                              (false, true) => Some(Greater),
                              (true, false) => Some(Less),
                              (true, true) => Some(Equal),
                          }
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      BinOp.le (|
                        M.read (| M.read (| self |) |),
                        M.read (| M.read (| other |) |)
                      |);
                      BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)
                    ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool false |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool false |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool false |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Greater" [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool true |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool false |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Less" [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool true |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Equal" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_f32.
    
    Module Impl_core_cmp_PartialOrd_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          match ( *self <= *other, *self >= *other) {
                              (false, false) => None,
                              (false, true) => Some(Greater),
                              (true, false) => Some(Less),
                              (true, true) => Some(Equal),
                          }
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      BinOp.le (|
                        M.read (| M.read (| self |) |),
                        M.read (| M.read (| other |) |)
                      |);
                      BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)
                    ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool false |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool false |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool false |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Greater" [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool true |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool false |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Less" [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool true |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Equal" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_f64.
    
    Module Impl_core_cmp_PartialOrd_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          match ( *self <= *other, *self >= *other) {
                              (false, false) => None,
                              (false, true) => Some(Greater),
                              (true, false) => Some(Less),
                              (true, true) => Some(Equal),
                          }
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      BinOp.le (|
                        M.read (| M.read (| self |) |),
                        M.read (| M.read (| other |) |)
                      |);
                      BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)
                    ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool false |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool false |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool false |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Greater" [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool true |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool false |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Less" [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_0 |), Value.Bool true |) in
                      let _ :=
                        M.is_constant_or_break_match (| M.read (| γ0_1 |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [ Value.StructTuple "core::cmp::Ordering::Equal" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_f128.
    
    Module Impl_core_cmp_Ord_for_Tuple_.
      Definition Self : Ty.t := Ty.tuple [].
      
      (*
              fn cmp(&self, _other: &()) -> Ordering {
                  Equal
              }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _other := M.alloc (| _other |) in
            Value.StructTuple "core::cmp::Ordering::Equal" []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_Tuple_.
    
    Module Impl_core_cmp_Ord_for_bool.
      Definition Self : Ty.t := Ty.path "bool".
      
      (*
              fn cmp(&self, other: &bool) -> Ordering {
                  // Casting to i8's and converting the difference to an Ordering generates
                  // more optimal assembly.
                  // See <https://github.com/rust-lang/rust/issues/66780> for more info.
                  match ( *self as i8) - ( *other as i8) {
                      -1 => Less,
                      0 => Equal,
                      1 => Greater,
                      // SAFETY: bool as i8 returns 0 or 1, so the difference can't be anything else
                      _ => unsafe { unreachable_unchecked() },
                  }
              }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  BinOp.Wrap.sub (|
                    M.rust_cast (M.read (| M.read (| self |) |)),
                    M.rust_cast (M.read (| M.read (| other |) |))
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (|
                          M.read (| γ |),
                          Value.Integer IntegerKind.I8 (-1)
                        |) in
                      M.alloc (| Value.StructTuple "core::cmp::Ordering::Less" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (|
                          M.read (| γ |),
                          Value.Integer IntegerKind.I8 0
                        |) in
                      M.alloc (| Value.StructTuple "core::cmp::Ordering::Equal" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (|
                          M.read (| γ |),
                          Value.Integer IntegerKind.I8 1
                        |) in
                      M.alloc (| Value.StructTuple "core::cmp::Ordering::Greater" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::hint::unreachable_unchecked", [] |),
                            []
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn min(self, other: bool) -> bool {
                  self & other
              }
      *)
      Definition min (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.bit_and (M.read (| self |)) (M.read (| other |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn max(self, other: bool) -> bool {
                  self | other
              }
      *)
      Definition max (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.bit_or (M.read (| self |)) (M.read (| other |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn clamp(self, min: bool, max: bool) -> bool {
                  assert!(min <= max);
                  self.max(min).min(max)
              }
      *)
      Definition clamp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; min; max ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let min := M.alloc (| min |) in
            let max := M.alloc (| max |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (| BinOp.le (| M.read (| min |), M.read (| max |) |) |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic", [] |),
                              [ M.read (| Value.String "assertion failed: min <= max" |) ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::cmp::Ord", Ty.path "bool", [], "min", [] |),
                  [
                    M.call_closure (|
                      M.get_trait_method (| "core::cmp::Ord", Ty.path "bool", [], "max", [] |),
                      [ M.read (| self |); M.read (| min |) ]
                    |);
                    M.read (| max |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("cmp", InstanceField.Method cmp);
            ("min", InstanceField.Method min);
            ("max", InstanceField.Method max);
            ("clamp", InstanceField.Method clamp)
          ].
    End Impl_core_cmp_Ord_for_bool.
    
    Module Impl_core_cmp_PartialOrd_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "char" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_char.
    
    Module Impl_core_cmp_Ord_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "char" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_char.
    
    Module Impl_core_cmp_PartialOrd_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "usize" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_usize.
    
    Module Impl_core_cmp_Ord_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "usize" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_usize.
    
    Module Impl_core_cmp_PartialOrd_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "u8" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_u8.
    
    Module Impl_core_cmp_Ord_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "u8" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_u8.
    
    Module Impl_core_cmp_PartialOrd_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "u16" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_u16.
    
    Module Impl_core_cmp_Ord_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "u16" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_u16.
    
    Module Impl_core_cmp_PartialOrd_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "u32" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_u32.
    
    Module Impl_core_cmp_Ord_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "u32" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_u32.
    
    Module Impl_core_cmp_PartialOrd_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "u64" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_u64.
    
    Module Impl_core_cmp_Ord_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "u64" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_u64.
    
    Module Impl_core_cmp_PartialOrd_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "u128" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_u128.
    
    Module Impl_core_cmp_Ord_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "u128" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_u128.
    
    Module Impl_core_cmp_PartialOrd_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "isize" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_isize.
    
    Module Impl_core_cmp_Ord_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "isize" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_isize.
    
    Module Impl_core_cmp_PartialOrd_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "i8" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_i8.
    
    Module Impl_core_cmp_Ord_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "i8" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_i8.
    
    Module Impl_core_cmp_PartialOrd_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "i16" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_i16.
    
    Module Impl_core_cmp_Ord_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "i16" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_i16.
    
    Module Impl_core_cmp_PartialOrd_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "i32" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_i32.
    
    Module Impl_core_cmp_Ord_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "i32" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_i32.
    
    Module Impl_core_cmp_PartialOrd_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "i64" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_i64.
    
    Module Impl_core_cmp_Ord_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "i64" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_i64.
    
    Module Impl_core_cmp_PartialOrd_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*
                      fn partial_cmp(&self, other: &$t) -> Option<Ordering> {
                          Some(crate::intrinsics::three_way_compare( *self, *other))
                      }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "i128" ] |),
                  [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn lt(&self, other: &$t) -> bool { ( *self) < ( *other) } *)
      Definition lt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.lt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn le(&self, other: &$t) -> bool { ( *self) <= ( *other) } *)
      Definition le (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.le (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn ge(&self, other: &$t) -> bool { ( *self) >= ( *other) } *)
      Definition ge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.ge (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*                 fn gt(&self, other: &$t) -> bool { ( *self) > ( *other) } *)
      Definition gt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.gt (| M.read (| M.read (| self |) |), M.read (| M.read (| other |) |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method partial_cmp);
            ("lt", InstanceField.Method lt);
            ("le", InstanceField.Method le);
            ("ge", InstanceField.Method ge);
            ("gt", InstanceField.Method gt)
          ].
    End Impl_core_cmp_PartialOrd_for_i128.
    
    Module Impl_core_cmp_Ord_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*
                      fn cmp(&self, other: &$t) -> Ordering {
                          crate::intrinsics::three_way_compare( *self, *other)
                      }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_function (| "core::intrinsics::three_way_compare", [ Ty.path "i128" ] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_i128.
    
    Module Impl_core_cmp_PartialEq_for_never.
      Definition Self : Ty.t := Ty.path "never".
      
      (*
              fn eq(&self, _: &!) -> bool {
                  *self
              }
      *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; β1 ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let β1 := M.alloc (| β1 |) in
            M.match_operator (|
              β1,
              [ fun γ => ltac:(M.monadic (M.never_to_any (| M.read (| M.read (| self |) |) |))) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_never.
    
    Module Impl_core_cmp_Eq_for_never.
      Definition Self : Ty.t := Ty.path "never".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_never.
    
    Module Impl_core_cmp_PartialOrd_for_never.
      Definition Self : Ty.t := Ty.path "never".
      
      (*
              fn partial_cmp(&self, _: &!) -> Option<Ordering> {
                  *self
              }
      *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; β1 ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let β1 := M.alloc (| β1 |) in
            M.match_operator (|
              β1,
              [ fun γ => ltac:(M.monadic (M.never_to_any (| M.read (| M.read (| self |) |) |))) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
    End Impl_core_cmp_PartialOrd_for_never.
    
    Module Impl_core_cmp_Ord_for_never.
      Definition Self : Ty.t := Ty.path "never".
      
      (*
              fn cmp(&self, _: &!) -> Ordering {
                  *self
              }
      *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; β1 ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let β1 := M.alloc (| β1 |) in
            M.match_operator (|
              β1,
              [ fun γ => ltac:(M.monadic (M.never_to_any (| M.read (| M.read (| self |) |) |))) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_never.
    
    Module Impl_core_cmp_PartialEq_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialEq_A_B_ref__B_for_ref__A.
      Definition Self (A B : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ A ].
      
      (*
              fn eq(&self, other: &&B) -> bool {
                  PartialEq::eq( *self, *other)
              }
      *)
      Definition eq (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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", A, [ B ], "eq", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn ne(&self, other: &&B) -> bool {
                  PartialEq::ne( *self, *other)
              }
      *)
      Definition ne (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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", A, [ B ], "ne", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A B : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self A B)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "&") [] [ B ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq A B)); ("ne", InstanceField.Method (ne A B)) ].
    End Impl_core_cmp_PartialEq_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialEq_A_B_ref__B_for_ref__A.
    
    Module Impl_core_cmp_PartialOrd_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialOrd_A_B_ref__B_for_ref__A.
      Definition Self (A B : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ A ].
      
      (*
              fn partial_cmp(&self, other: &&B) -> Option<Ordering> {
                  PartialOrd::partial_cmp( *self, *other)
              }
      *)
      Definition partial_cmp
          (A B : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self A B 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::PartialOrd", A, [ B ], "partial_cmp", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn lt(&self, other: &&B) -> bool {
                  PartialOrd::lt( *self, *other)
              }
      *)
      Definition lt (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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::PartialOrd", A, [ B ], "lt", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn le(&self, other: &&B) -> bool {
                  PartialOrd::le( *self, *other)
              }
      *)
      Definition le (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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::PartialOrd", A, [ B ], "le", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn gt(&self, other: &&B) -> bool {
                  PartialOrd::gt( *self, *other)
              }
      *)
      Definition gt (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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::PartialOrd", A, [ B ], "gt", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn ge(&self, other: &&B) -> bool {
                  PartialOrd::ge( *self, *other)
              }
      *)
      Definition ge (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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::PartialOrd", A, [ B ], "ge", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A B : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          (Self A B)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "&") [] [ B ] ]
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method (partial_cmp A B));
            ("lt", InstanceField.Method (lt A B));
            ("le", InstanceField.Method (le A B));
            ("gt", InstanceField.Method (gt A B));
            ("ge", InstanceField.Method (ge A B))
          ].
    End Impl_core_cmp_PartialOrd_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialOrd_A_B_ref__B_for_ref__A.
    
    Module Impl_core_cmp_Ord_where_core_marker_Sized_A_where_core_cmp_Ord_A_for_ref__A.
      Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ A ].
      
      (*
              fn cmp(&self, other: &Self) -> Ordering {
                  Ord::cmp( *self, *other)
              }
      *)
      Definition cmp (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self 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::Ord", A, [], "cmp", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A : Ty.t),
        M.IsTraitInstance
          "core::cmp::Ord"
          (Self A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method (cmp A)) ].
    End Impl_core_cmp_Ord_where_core_marker_Sized_A_where_core_cmp_Ord_A_for_ref__A.
    
    Module Impl_core_cmp_Eq_where_core_marker_Sized_A_where_core_cmp_Eq_A_for_ref__A.
      Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ A ].
      
      Axiom Implements :
        forall (A : Ty.t),
        M.IsTraitInstance
          "core::cmp::Eq"
          (Self A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_Eq_where_core_marker_Sized_A_where_core_cmp_Eq_A_for_ref__A.
    
    Module Impl_core_cmp_PartialEq_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialEq_A_B_ref_mut_B_for_ref_mut_A.
      Definition Self (A B : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ A ].
      
      (*
              fn eq(&self, other: &&mut B) -> bool {
                  PartialEq::eq( *self, *other)
              }
      *)
      Definition eq (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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", A, [ B ], "eq", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn ne(&self, other: &&mut B) -> bool {
                  PartialEq::ne( *self, *other)
              }
      *)
      Definition ne (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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", A, [ B ], "ne", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A B : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self A B)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "&mut") [] [ B ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq A B)); ("ne", InstanceField.Method (ne A B)) ].
    End Impl_core_cmp_PartialEq_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialEq_A_B_ref_mut_B_for_ref_mut_A.
    
    Module Impl_core_cmp_PartialOrd_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialOrd_A_B_ref_mut_B_for_ref_mut_A.
      Definition Self (A B : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ A ].
      
      (*
              fn partial_cmp(&self, other: &&mut B) -> Option<Ordering> {
                  PartialOrd::partial_cmp( *self, *other)
              }
      *)
      Definition partial_cmp
          (A B : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self A B 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::PartialOrd", A, [ B ], "partial_cmp", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn lt(&self, other: &&mut B) -> bool {
                  PartialOrd::lt( *self, *other)
              }
      *)
      Definition lt (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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::PartialOrd", A, [ B ], "lt", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn le(&self, other: &&mut B) -> bool {
                  PartialOrd::le( *self, *other)
              }
      *)
      Definition le (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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::PartialOrd", A, [ B ], "le", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn gt(&self, other: &&mut B) -> bool {
                  PartialOrd::gt( *self, *other)
              }
      *)
      Definition gt (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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::PartialOrd", A, [ B ], "gt", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn ge(&self, other: &&mut B) -> bool {
                  PartialOrd::ge( *self, *other)
              }
      *)
      Definition ge (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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::PartialOrd", A, [ B ], "ge", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A B : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          (Self A B)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "&mut") [] [ B ] ]
          (* Instance *)
          [
            ("partial_cmp", InstanceField.Method (partial_cmp A B));
            ("lt", InstanceField.Method (lt A B));
            ("le", InstanceField.Method (le A B));
            ("gt", InstanceField.Method (gt A B));
            ("ge", InstanceField.Method (ge A B))
          ].
    End Impl_core_cmp_PartialOrd_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialOrd_A_B_ref_mut_B_for_ref_mut_A.
    
    Module Impl_core_cmp_Ord_where_core_marker_Sized_A_where_core_cmp_Ord_A_for_ref_mut_A.
      Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ A ].
      
      (*
              fn cmp(&self, other: &Self) -> Ordering {
                  Ord::cmp( *self, *other)
              }
      *)
      Definition cmp (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self 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::Ord", A, [], "cmp", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A : Ty.t),
        M.IsTraitInstance
          "core::cmp::Ord"
          (Self A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method (cmp A)) ].
    End Impl_core_cmp_Ord_where_core_marker_Sized_A_where_core_cmp_Ord_A_for_ref_mut_A.
    
    Module Impl_core_cmp_Eq_where_core_marker_Sized_A_where_core_cmp_Eq_A_for_ref_mut_A.
      Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ A ].
      
      Axiom Implements :
        forall (A : Ty.t),
        M.IsTraitInstance
          "core::cmp::Eq"
          (Self A)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_Eq_where_core_marker_Sized_A_where_core_cmp_Eq_A_for_ref_mut_A.
    
    Module Impl_core_cmp_PartialEq_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialEq_A_B_ref_mut_B_for_ref__A.
      Definition Self (A B : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ A ].
      
      (*
              fn eq(&self, other: &&mut B) -> bool {
                  PartialEq::eq( *self, *other)
              }
      *)
      Definition eq (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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", A, [ B ], "eq", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn ne(&self, other: &&mut B) -> bool {
                  PartialEq::ne( *self, *other)
              }
      *)
      Definition ne (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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", A, [ B ], "ne", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A B : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self A B)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "&mut") [] [ B ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq A B)); ("ne", InstanceField.Method (ne A B)) ].
    End Impl_core_cmp_PartialEq_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialEq_A_B_ref_mut_B_for_ref__A.
    
    Module Impl_core_cmp_PartialEq_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialEq_A_B_ref__B_for_ref_mut_A.
      Definition Self (A B : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ A ].
      
      (*
              fn eq(&self, other: &&B) -> bool {
                  PartialEq::eq( *self, *other)
              }
      *)
      Definition eq (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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", A, [ B ], "eq", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
              fn ne(&self, other: &&B) -> bool {
                  PartialEq::ne( *self, *other)
              }
      *)
      Definition ne (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B 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", A, [ B ], "ne", [] |),
              [ M.read (| M.read (| self |) |); M.read (| M.read (| other |) |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A B : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self A B)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "&") [] [ B ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq A B)); ("ne", InstanceField.Method (ne A B)) ].
    End Impl_core_cmp_PartialEq_where_core_marker_Sized_A_where_core_marker_Sized_B_where_core_cmp_PartialEq_A_B_ref__B_for_ref_mut_A.
  End impls.
End cmp.
