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

Module borrow.
  Module Impl_core_borrow_Borrow_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*
        fn borrow(&self) -> &B {
            &**self
        }
    *)
    Definition borrow (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::deref::Deref",
              Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ],
              [],
              "deref",
              []
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance
        "core::borrow::Borrow"
        (Self B)
        (* Trait polymorphic types *) [ (* Borrowed *) B ]
        (* Instance *) [ ("borrow", InstanceField.Method (borrow B)) ].
  End Impl_core_borrow_Borrow_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_B_for_alloc_borrow_Cow_B.
  
  (* Trait *)
  Module ToOwned.
    Definition clone_into (Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; target ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let target := M.alloc (| target |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| target |),
                M.call_closure (|
                  M.get_trait_method (| "alloc::borrow::ToOwned", Self, [], "to_owned", [] |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_clone_into :
      M.IsProvidedMethod "alloc::borrow::ToOwned" "clone_into" clone_into.
  End ToOwned.
  
  Module Impl_alloc_borrow_ToOwned_where_core_clone_Clone_T_for_T.
    Definition Self (T : Ty.t) : Ty.t := T.
    
    (*     type Owned = T; *)
    Definition _Owned (T : Ty.t) : Ty.t := T.
    
    (*
        fn to_owned(&self) -> T {
            self.clone()
        }
    *)
    Definition to_owned (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.call_closure (|
            M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn clone_into(&self, target: &mut T) {
            target.clone_from(self);
        }
    *)
    Definition clone_into (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; target ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let target := M.alloc (| target |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", T, [], "clone_from", [] |),
                  [ M.read (| target |); M.read (| self |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "alloc::borrow::ToOwned"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Owned", InstanceField.Ty (_Owned T));
          ("to_owned", InstanceField.Method (to_owned T));
          ("clone_into", InstanceField.Method (clone_into T))
        ].
  End Impl_alloc_borrow_ToOwned_where_core_clone_Clone_T_for_T.
  
  (*
  Enum Cow
  {
    const_params := [];
    ty_params := [ "B" ];
    variants :=
      [
        {
          name := "Borrowed";
          item := StructTuple [ Ty.apply (Ty.path "&") [] [ B ] ];
          discriminant := None;
        };
        {
          name := "Owned";
          item := StructTuple [ Ty.associated ];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*
        fn clone(&self) -> Self {
            match *self {
                Borrowed(b) => Borrowed(b),
                Owned(ref o) => {
                    let b: &B = o.borrow();
                    Owned(b.to_owned())
                }
            }
        }
    *)
    Definition clone (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.read (| self |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "alloc::borrow::Cow::Borrowed",
                        0
                      |) in
                    let b := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "alloc::borrow::Cow::Borrowed" [ M.read (| b |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "alloc::borrow::Cow::Owned", 0 |) in
                    let o := M.alloc (| γ0_0 |) in
                    let~ b :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::borrow::Borrow",
                            Ty.associated,
                            [ B ],
                            "borrow",
                            []
                          |),
                          [ M.read (| o |) ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "alloc::borrow::Cow::Owned"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "alloc::borrow::ToOwned",
                              B,
                              [],
                              "to_owned",
                              []
                            |),
                            [ M.read (| b |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn clone_from(&mut self, source: &Self) {
            match (self, source) {
                (&mut Owned(ref mut dest), &Owned(ref o)) => o.borrow().clone_into(dest),
                (t, s) => *t = s.clone(),
            }
        }
    *)
    Definition clone_from (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [ self; source ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let source := M.alloc (| source |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| source |) ] |),
              [
                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 γ0_0 := M.read (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "alloc::borrow::Cow::Owned",
                        0
                      |) in
                    let dest := M.alloc (| γ2_0 |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "alloc::borrow::Cow::Owned",
                        0
                      |) in
                    let o := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "alloc::borrow::ToOwned", B, [], "clone_into", [] |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::borrow::Borrow",
                              Ty.associated,
                              [ B ],
                              "borrow",
                              []
                            |),
                            [ M.read (| o |) ]
                          |);
                          M.read (| dest |)
                        ]
                      |)
                    |)));
                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 t := M.copy (| γ0_0 |) in
                    let s := M.copy (| γ0_1 |) in
                    M.write (|
                      M.read (| t |),
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::clone::Clone",
                          Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ],
                          [],
                          "clone",
                          []
                        |),
                        [ M.read (| s |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self B)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("clone", InstanceField.Method (clone B));
          ("clone_from", InstanceField.Method (clone_from B))
        ].
  End Impl_core_clone_Clone_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
  
  Module Impl_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*
        pub const fn is_borrowed(&self) -> bool {
            match *self {
                Borrowed(_) => true,
                Owned(_) => false,
            }
        }
    *)
    Definition is_borrowed (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.read (| self |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "alloc::borrow::Cow::Borrowed",
                        0
                      |) in
                    M.alloc (| Value.Bool true |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "alloc::borrow::Cow::Owned", 0 |) in
                    M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_borrowed :
      forall (B : Ty.t),
      M.IsAssociatedFunction (Self B) "is_borrowed" (is_borrowed B).
    
    (*
        pub const fn is_owned(&self) -> bool {
            !self.is_borrowed()
        }
    *)
    Definition is_owned (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          UnOp.not (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ],
                "is_borrowed",
                []
              |),
              [ M.read (| self |) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_owned :
      forall (B : Ty.t),
      M.IsAssociatedFunction (Self B) "is_owned" (is_owned B).
    
    (*
        pub fn to_mut(&mut self) -> &mut <B as ToOwned>::Owned {
            match *self {
                Borrowed(borrowed) => {
                    *self = Owned(borrowed.to_owned());
                    match *self {
                        Borrowed(..) => unreachable!(),
                        Owned(ref mut owned) => owned,
                    }
                }
                Owned(ref mut owned) => owned,
            }
        }
    *)
    Definition to_mut (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.read (| self |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "alloc::borrow::Cow::Borrowed",
                        0
                      |) in
                    let borrowed := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.read (|
                        let~ _ :=
                          M.write (|
                            M.read (| self |),
                            Value.StructTuple
                              "alloc::borrow::Cow::Owned"
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "alloc::borrow::ToOwned",
                                    B,
                                    [],
                                    "to_owned",
                                    []
                                  |),
                                  [ M.read (| borrowed |) ]
                                |)
                              ]
                          |) in
                        M.alloc (|
                          M.read (|
                            M.match_operator (|
                              M.read (| self |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let _ :=
                                      M.is_struct_tuple (| γ, "alloc::borrow::Cow::Borrowed" |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic", [] |),
                                          [
                                            M.read (|
                                              Value.String
                                                "internal error: entered unreachable code"
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "alloc::borrow::Cow::Owned",
                                        0
                                      |) in
                                    let owned := M.alloc (| γ0_0 |) in
                                    M.alloc (| M.read (| owned |) |)))
                              ]
                            |)
                          |)
                        |)
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "alloc::borrow::Cow::Owned", 0 |) in
                    let owned := M.alloc (| γ0_0 |) in
                    M.alloc (| M.read (| owned |) |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_mut :
      forall (B : Ty.t),
      M.IsAssociatedFunction (Self B) "to_mut" (to_mut B).
    
    (*
        pub fn into_owned(self) -> <B as ToOwned>::Owned {
            match self {
                Borrowed(borrowed) => borrowed.to_owned(),
                Owned(owned) => owned,
            }
        }
    *)
    Definition into_owned (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "alloc::borrow::Cow::Borrowed",
                        0
                      |) in
                    let borrowed := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "alloc::borrow::ToOwned", B, [], "to_owned", [] |),
                        [ M.read (| borrowed |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "alloc::borrow::Cow::Owned", 0 |) in
                    let owned := M.copy (| γ0_0 |) in
                    owned))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_owned :
      forall (B : Ty.t),
      M.IsAssociatedFunction (Self B) "into_owned" (into_owned B).
  End Impl_alloc_borrow_Cow_B.
  
  Module Impl_core_ops_deref_Deref_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_where_core_borrow_Borrow_associated_type_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*     type Target = B; *)
    Definition _Target (B : Ty.t) : Ty.t := B.
    
    (*
        fn deref(&self) -> &B {
            match *self {
                Borrowed(borrowed) => borrowed,
                Owned(ref owned) => owned.borrow(),
            }
        }
    *)
    Definition deref (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.read (| self |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "alloc::borrow::Cow::Borrowed",
                        0
                      |) in
                    let borrowed := M.copy (| γ0_0 |) in
                    M.alloc (| M.read (| borrowed |) |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "alloc::borrow::Cow::Owned", 0 |) in
                    let owned := M.alloc (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::borrow::Borrow",
                          Ty.associated,
                          [ B ],
                          "borrow",
                          []
                        |),
                        [ M.read (| owned |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::Deref"
        (Self B)
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("Target", InstanceField.Ty (_Target B)); ("deref", InstanceField.Method (deref B)) ].
  End Impl_core_ops_deref_Deref_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_where_core_borrow_Borrow_associated_type_B_for_alloc_borrow_Cow_B.
  
  Module Impl_core_ops_deref_DerefPure_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_where_core_borrow_Borrow_associated_type_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::DerefPure"
        (Self B)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_ops_deref_DerefPure_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_where_core_borrow_Borrow_associated_type_B_for_alloc_borrow_Cow_B.
  
  Module Impl_core_cmp_Eq_where_core_marker_Sized_B_where_core_cmp_Eq_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance "core::cmp::Eq" (Self B) (* Trait polymorphic types *) [] (* Instance *) [].
  End Impl_core_cmp_Eq_where_core_marker_Sized_B_where_core_cmp_Eq_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
  
  Module Impl_core_cmp_Ord_where_core_marker_Sized_B_where_core_cmp_Ord_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*
        fn cmp(&self, other: &Self) -> Ordering {
            Ord::cmp(&**self, &**other)
        }
    *)
    Definition cmp (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self 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::Ord", B, [], "cmp", [] |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance
        "core::cmp::Ord"
        (Self B)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method (cmp B)) ].
  End Impl_core_cmp_Ord_where_core_marker_Sized_B_where_core_cmp_Ord_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
  
  Module Impl_core_cmp_PartialEq_where_core_marker_Sized_B_where_core_marker_Sized_C_where_core_cmp_PartialEq_B_C_where_alloc_borrow_ToOwned_B_where_alloc_borrow_ToOwned_C_alloc_borrow_Cow_C_for_alloc_borrow_Cow_B.
    Definition Self (B C : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*
        fn eq(&self, other: &Cow<'b, C>) -> bool {
            PartialEq::eq(&**self, &**other)
        }
    *)
    Definition eq (B C : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B C 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", B, [ C ], "eq", [] |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "alloc::borrow::Cow") [] [ C ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (B C : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self B C)
        (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "alloc::borrow::Cow") [] [ C ] ]
        (* Instance *) [ ("eq", InstanceField.Method (eq B C)) ].
  End Impl_core_cmp_PartialEq_where_core_marker_Sized_B_where_core_marker_Sized_C_where_core_cmp_PartialEq_B_C_where_alloc_borrow_ToOwned_B_where_alloc_borrow_ToOwned_C_alloc_borrow_Cow_C_for_alloc_borrow_Cow_B.
  
  Module Impl_core_cmp_PartialOrd_where_core_marker_Sized_B_where_core_cmp_PartialOrd_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*
        fn partial_cmp(&self, other: &Cow<'a, B>) -> Option<Ordering> {
            PartialOrd::partial_cmp(&**self, &**other)
        }
    *)
    Definition partial_cmp (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self 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", B, [ B ], "partial_cmp", [] |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| other |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        (Self B)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method (partial_cmp B)) ].
  End Impl_core_cmp_PartialOrd_where_core_marker_Sized_B_where_core_cmp_PartialOrd_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
  
  Module Impl_core_fmt_Debug_where_core_marker_Sized_B_where_core_fmt_Debug_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            match *self {
                Borrowed(ref b) => fmt::Debug::fmt(b, f),
                Owned(ref o) => fmt::Debug::fmt(o, f),
            }
        }
    *)
    Definition fmt (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              M.read (| self |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "alloc::borrow::Cow::Borrowed",
                        0
                      |) in
                    let b := M.alloc (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::fmt::Debug",
                          Ty.apply (Ty.path "&") [] [ B ],
                          [],
                          "fmt",
                          []
                        |),
                        [ M.read (| b |); M.read (| f |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "alloc::borrow::Cow::Owned", 0 |) in
                    let o := M.alloc (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::fmt::Debug", Ty.associated, [], "fmt", [] |),
                        [ M.read (| o |); M.read (| f |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self B)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt B)) ].
  End Impl_core_fmt_Debug_where_core_marker_Sized_B_where_core_fmt_Debug_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
  
  Module Impl_core_fmt_Display_where_core_marker_Sized_B_where_core_fmt_Display_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            match *self {
                Borrowed(ref b) => fmt::Display::fmt(b, f),
                Owned(ref o) => fmt::Display::fmt(o, f),
            }
        }
    *)
    Definition fmt (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              M.read (| self |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "alloc::borrow::Cow::Borrowed",
                        0
                      |) in
                    let b := M.alloc (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::fmt::Display",
                          Ty.apply (Ty.path "&") [] [ B ],
                          [],
                          "fmt",
                          []
                        |),
                        [ M.read (| b |); M.read (| f |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "alloc::borrow::Cow::Owned", 0 |) in
                    let o := M.alloc (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::fmt::Display", Ty.associated, [], "fmt", [] |),
                        [ M.read (| o |); M.read (| f |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance
        "core::fmt::Display"
        (Self B)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt B)) ].
  End Impl_core_fmt_Display_where_core_marker_Sized_B_where_core_fmt_Display_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
  
  Module Impl_core_default_Default_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*
        fn default() -> Self {
            Owned(<B as ToOwned>::Owned::default())
        }
    *)
    Definition default (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructTuple
            "alloc::borrow::Cow::Owned"
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", Ty.associated, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self B)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default B)) ].
  End Impl_core_default_Default_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
  
  Module Impl_core_hash_Hash_where_core_marker_Sized_B_where_core_hash_Hash_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
    Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
    
    (*
        fn hash<H: Hasher>(&self, state: &mut H) {
            Hash::hash(&**self, state)
        }
    *)
    Definition hash (B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self B 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", B, [], "hash", [ H ] |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.read (| state |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (B : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self B)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash B)) ].
  End Impl_core_hash_Hash_where_core_marker_Sized_B_where_core_hash_Hash_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
  
  Module Impl_core_convert_AsRef_where_core_marker_Sized_T_where_alloc_borrow_ToOwned_T_T_for_alloc_borrow_Cow_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ T ].
    
    (*
        fn as_ref(&self) -> &T {
            self
        }
    *)
    Definition as_ref (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.call_closure (|
            M.get_trait_method (|
              "core::ops::deref::Deref",
              Ty.apply (Ty.path "alloc::borrow::Cow") [] [ T ],
              [],
              "deref",
              []
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::AsRef"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *) [ ("as_ref", InstanceField.Method (as_ref T)) ].
  End Impl_core_convert_AsRef_where_core_marker_Sized_T_where_alloc_borrow_ToOwned_T_T_for_alloc_borrow_Cow_T.
  
  Module Impl_core_ops_arith_Add_ref__str_for_alloc_borrow_Cow_str.
    Definition Self : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ].
    
    (*     type Output = Cow<'a, str>; *)
    Definition _Output : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ].
    
    (*
        fn add(mut self, rhs: &'a str) -> Self::Output {
            self += rhs;
            self
        }
    *)
    Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::AddAssign",
                    Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ],
                    [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ],
                    "add_assign",
                    []
                  |),
                  [ self; M.read (| rhs |) ]
                |)
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Add"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
  End Impl_core_ops_arith_Add_ref__str_for_alloc_borrow_Cow_str.
  
  Module Impl_core_ops_arith_Add_alloc_borrow_Cow_str_for_alloc_borrow_Cow_str.
    Definition Self : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ].
    
    (*     type Output = Cow<'a, str>; *)
    Definition _Output : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ].
    
    (*
        fn add(mut self, rhs: Cow<'a, str>) -> Self::Output {
            self += rhs;
            self
        }
    *)
    Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::AddAssign",
                    Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ],
                    [ Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ] ],
                    "add_assign",
                    []
                  |),
                  [ self; M.read (| rhs |) ]
                |)
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Add"
        Self
        (* Trait polymorphic types *)
        [ (* Rhs *) Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ] ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
  End Impl_core_ops_arith_Add_alloc_borrow_Cow_str_for_alloc_borrow_Cow_str.
  
  Module Impl_core_ops_arith_AddAssign_ref__str_for_alloc_borrow_Cow_str.
    Definition Self : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ].
    
    (*
        fn add_assign(&mut self, rhs: &'a str) {
            if self.is_empty() {
                *self = Cow::Borrowed(rhs)
            } else if !rhs.is_empty() {
                if let Cow::Borrowed(lhs) = *self {
                    let mut s = String::with_capacity(lhs.len() + rhs.len());
                    s.push_str(lhs);
                    *self = Cow::Owned(s);
                }
                self.to_mut().push_str(rhs);
            }
        }
    *)
    Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) 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 "str", "is_empty", [] |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ],
                                  [],
                                  "deref",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |)
                            ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.write (|
                      M.read (| self |),
                      Value.StructTuple "alloc::borrow::Cow::Borrowed" [ M.read (| rhs |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    M.call_closure (|
                                      M.get_associated_function (| Ty.path "str", "is_empty", [] |),
                                      [ M.read (| rhs |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ := M.read (| self |) in
                                      let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "alloc::borrow::Cow::Borrowed",
                                          0
                                        |) in
                                      let lhs := M.copy (| γ0_0 |) in
                                      let~ s :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "alloc::string::String",
                                              "with_capacity",
                                              []
                                            |),
                                            [
                                              BinOp.Wrap.add (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "str",
                                                    "len",
                                                    []
                                                  |),
                                                  [ M.read (| lhs |) ]
                                                |),
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "str",
                                                    "len",
                                                    []
                                                  |),
                                                  [ M.read (| rhs |) ]
                                                |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "alloc::string::String",
                                              "push_str",
                                              []
                                            |),
                                            [ s; M.read (| lhs |) ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          M.read (| self |),
                                          Value.StructTuple
                                            "alloc::borrow::Cow::Owned"
                                            [ M.read (| s |) ]
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "alloc::string::String",
                                    "push_str",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::borrow::Cow")
                                          []
                                          [ Ty.path "str" ],
                                        "to_mut",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |);
                                    M.read (| rhs |)
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::AddAssign"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
        (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
  End Impl_core_ops_arith_AddAssign_ref__str_for_alloc_borrow_Cow_str.
  
  Module Impl_core_ops_arith_AddAssign_alloc_borrow_Cow_str_for_alloc_borrow_Cow_str.
    Definition Self : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ].
    
    (*
        fn add_assign(&mut self, rhs: Cow<'a, str>) {
            if self.is_empty() {
                *self = rhs
            } else if !rhs.is_empty() {
                if let Cow::Borrowed(lhs) = *self {
                    let mut s = String::with_capacity(lhs.len() + rhs.len());
                    s.push_str(lhs);
                    *self = Cow::Owned(s);
                }
                self.to_mut().push_str(&rhs);
            }
        }
    *)
    Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) 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 "str", "is_empty", [] |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ],
                                  [],
                                  "deref",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |)
                            ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.write (| M.read (| self |), M.read (| rhs |) |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    M.call_closure (|
                                      M.get_associated_function (| Ty.path "str", "is_empty", [] |),
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::deref::Deref",
                                            Ty.apply
                                              (Ty.path "alloc::borrow::Cow")
                                              []
                                              [ Ty.path "str" ],
                                            [],
                                            "deref",
                                            []
                                          |),
                                          [ rhs ]
                                        |)
                                      ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ := M.read (| self |) in
                                      let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "alloc::borrow::Cow::Borrowed",
                                          0
                                        |) in
                                      let lhs := M.copy (| γ0_0 |) in
                                      let~ s :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "alloc::string::String",
                                              "with_capacity",
                                              []
                                            |),
                                            [
                                              BinOp.Wrap.add (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "str",
                                                    "len",
                                                    []
                                                  |),
                                                  [ M.read (| lhs |) ]
                                                |),
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "str",
                                                    "len",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::ops::deref::Deref",
                                                        Ty.apply
                                                          (Ty.path "alloc::borrow::Cow")
                                                          []
                                                          [ Ty.path "str" ],
                                                        [],
                                                        "deref",
                                                        []
                                                      |),
                                                      [ rhs ]
                                                    |)
                                                  ]
                                                |)
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "alloc::string::String",
                                              "push_str",
                                              []
                                            |),
                                            [ s; M.read (| lhs |) ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          M.read (| self |),
                                          Value.StructTuple
                                            "alloc::borrow::Cow::Owned"
                                            [ M.read (| s |) ]
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "alloc::string::String",
                                    "push_str",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::borrow::Cow")
                                          []
                                          [ Ty.path "str" ],
                                        "to_mut",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |);
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.apply
                                          (Ty.path "alloc::borrow::Cow")
                                          []
                                          [ Ty.path "str" ],
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [ rhs ]
                                    |)
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::AddAssign"
        Self
        (* Trait polymorphic types *)
        [ (* Rhs *) Ty.apply (Ty.path "alloc::borrow::Cow") [] [ Ty.path "str" ] ]
        (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
  End Impl_core_ops_arith_AddAssign_alloc_borrow_Cow_str_for_alloc_borrow_Cow_str.
End borrow.
