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

Module cell.
  (* StructRecord
    {
      name := "Cell";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ ("value", Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ]) ];
    } *)
  
  Module Impl_core_marker_Send_where_core_marker_Sized_T_where_core_marker_Send_T_for_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Send"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Send_where_core_marker_Sized_T_where_core_marker_Send_T_for_core_cell_Cell_T.
  
  Module Impl_core_marker_Sync_where_core_marker_Sized_T_for_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Sync"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Sync_where_core_marker_Sized_T_for_core_cell_Cell_T.
  
  Module Impl_core_clone_Clone_where_core_marker_Copy_T_for_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    (*
        fn clone(&self) -> Cell<T> {
            Cell::new(self.get())
        }
    *)
    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
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
              "new",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                  "get",
                  []
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => 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)) ].
  End Impl_core_clone_Clone_where_core_marker_Copy_T_for_core_cell_Cell_T.
  
  Module Impl_core_default_Default_where_core_default_Default_T_for_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    (*
        fn default() -> Cell<T> {
            Cell::new(Default::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
          (M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
              "new",
              []
            |),
            [
              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_cell_Cell_T.
  
  Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_where_core_marker_Copy_T_for_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    (*
        fn eq(&self, other: &Cell<T>) -> bool {
            self.get() == other.get()
        }
    *)
    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.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| other |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_where_core_marker_Copy_T_for_core_cell_Cell_T.
  
  Module Impl_core_cmp_Eq_where_core_cmp_Eq_T_where_core_marker_Copy_T_for_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance "core::cmp::Eq" (Self T) (* Trait polymorphic types *) [] (* Instance *) [].
  End Impl_core_cmp_Eq_where_core_cmp_Eq_T_where_core_marker_Copy_T_for_core_cell_Cell_T.
  
  Module Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_where_core_marker_Copy_T_for_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    (*
        fn partial_cmp(&self, other: &Cell<T>) -> Option<Ordering> {
            self.get().partial_cmp(&other.get())
        }
    *)
    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.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| other |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn lt(&self, other: &Cell<T>) -> bool {
            self.get() < other.get()
        }
    *)
    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.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| other |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn le(&self, other: &Cell<T>) -> bool {
            self.get() <= other.get()
        }
    *)
    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.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| other |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn gt(&self, other: &Cell<T>) -> bool {
            self.get() > other.get()
        }
    *)
    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.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| other |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn ge(&self, other: &Cell<T>) -> bool {
            self.get() >= other.get()
        }
    *)
    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.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| other |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_where_core_marker_Copy_T_for_core_cell_Cell_T.
  
  Module Impl_core_cmp_Ord_where_core_cmp_Ord_T_where_core_marker_Copy_T_for_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    (*
        fn cmp(&self, other: &Cell<T>) -> Ordering {
            self.get().cmp(&other.get())
        }
    *)
    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.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| other |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_where_core_marker_Copy_T_for_core_cell_Cell_T.
  
  Module Impl_core_convert_From_T_for_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    (*
        fn from(t: T) -> Cell<T> {
            Cell::new(t)
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ t ] =>
        ltac:(M.monadic
          (let t := M.alloc (| t |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
              "new",
              []
            |),
            [ M.read (| t |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_T_for_core_cell_Cell_T.
  
  Module Impl_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    (*
        pub const fn new(value: T) -> Cell<T> {
            Cell { value: UnsafeCell::new(value) }
        }
    *)
    Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          Value.StructRecord
            "core::cell::Cell"
            [
              ("value",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
                    "new",
                    []
                  |),
                  [ M.read (| value |) ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "new" (new T).
    
    (*
        pub fn set(&self, val: T) {
            self.replace(val);
        }
    *)
    Definition set (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; val ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let val := M.alloc (| val |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "replace",
                    []
                  |),
                  [ M.read (| self |); M.read (| val |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_set : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "set" (set T).
    
    (*
        pub fn swap(&self, other: &Self) {
            // This function documents that it *will* panic, and intrinsics::is_nonoverlapping doesn't
            // do the check in const, so trying to use it here would be inviting unnecessary fragility.
            fn is_nonoverlapping<T>(src: *const T, dst: *const T) -> bool {
                let src_usize = src.addr();
                let dst_usize = dst.addr();
                let diff = src_usize.abs_diff(dst_usize);
                diff >= size_of::<T>()
            }
    
            if ptr::eq(self, other) {
                // Swapping wouldn't change anything.
                return;
            }
            if !is_nonoverlapping(self, other) {
                // See <https://github.com/rust-lang/rust/issues/80778> for why we need to stop here.
                panic!("`Cell::swap` on overlapping non-identical `Cell`s");
            }
            // SAFETY: This can be risky if called from separate threads, but `Cell`
            // is `!Sync` so this won't happen. This also won't invalidate any
            // pointers since `Cell` makes sure nothing else will be pointing into
            // either of these `Cell`s. We also excluded shenanigans like partially overlapping `Cell`s,
            // so `swap` will just properly copy two full values of type `T` back and forth.
            unsafe {
                mem::swap(&mut *self.value.get(), &mut *other.value.get());
            }
        }
    *)
    Definition swap (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.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_function (|
                                    "core::ptr::eq",
                                    [ Ty.apply (Ty.path "core::cell::Cell") [] [ T ] ]
                                  |),
                                  [ M.read (| self |); M.read (| other |) ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (| M.read (| M.return_ (| Value.Tuple [] |) |) |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  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 (|
                                      Self,
                                      "is_nonoverlapping.swap",
                                      []
                                    |),
                                    [ M.read (| self |); M.read (| other |) ]
                                  |)
                                |)
                              |)) 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_fmt", [] |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::Arguments",
                                      "new_const",
                                      []
                                    |),
                                    [
                                      M.alloc (|
                                        Value.Array
                                          [
                                            M.read (|
                                              Value.String
                                                "`Cell::swap` on overlapping non-identical `Cell`s"
                                            |)
                                          ]
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "core::mem::swap", [ T ] |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
                            "get",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "core::cell::Cell",
                              "value"
                            |)
                          ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
                            "get",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "core::cell::Cell",
                              "value"
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_swap :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "swap" (swap T).
    
    (*
        pub fn replace(&self, val: T) -> T {
            // SAFETY: This can cause data races if called from a separate thread,
            // but `Cell` is `!Sync` so this won't happen.
            mem::replace(unsafe { &mut *self.value.get() }, val)
        }
    *)
    Definition replace (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; val ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let val := M.alloc (| val |) in
          M.call_closure (|
            M.get_function (| "core::mem::replace", [ T ] |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
                  "get",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::cell::Cell",
                    "value"
                  |)
                ]
              |);
              M.read (| val |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_replace :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "replace" (replace T).
    
    (*
        pub const fn into_inner(self) -> T {
            self.value.into_inner()
        }
    *)
    Definition into_inner (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_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "into_inner",
              []
            |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (| self, "core::cell::Cell", "value" |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_inner :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "into_inner" (into_inner T).
    (*
        pub fn get(&self) -> T {
            // SAFETY: This can cause data races if called from a separate thread,
            // but `Cell` is `!Sync` so this won't happen.
            unsafe { *self.value.get() }
        }
    *)
    Definition get (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.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
                "get",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::cell::Cell",
                  "value"
                |)
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "get" (get T).
    
    (*
        pub fn update<F>(&self, f: F) -> T
        where
            F: FnOnce(T) -> T,
        {
            let old = self.get();
            let new = f(old);
            self.set(new);
            new
        }
    *)
    Definition update (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ old :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "get",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ new :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::function::FnOnce",
                    F,
                    [ Ty.tuple [ T ] ],
                    "call_once",
                    []
                  |),
                  [ M.read (| f |); Value.Tuple [ M.read (| old |) ] ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
                    "set",
                    []
                  |),
                  [ M.read (| self |); M.read (| new |) ]
                |)
              |) in
            new
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_update :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "update" (update T).
    (*
        pub const fn as_ptr(&self) -> *mut T {
            self.value.get()
        }
    *)
    Definition as_ptr (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_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "get",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::cell::Cell",
                "value"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_ptr :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_ptr" (as_ptr T).
    
    (*
        pub fn get_mut(&mut self) -> &mut T {
            self.value.get_mut()
        }
    *)
    Definition get_mut (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_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "get_mut",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::cell::Cell",
                "value"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "get_mut" (get_mut T).
    
    (*
        pub fn from_mut(t: &mut T) -> &Cell<T> {
            // SAFETY: `&mut` ensures unique access.
            unsafe { &*(t as *mut T as *const Cell<T>) }
        }
    *)
    Definition from_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ t ] =>
        ltac:(M.monadic
          (let t := M.alloc (| t |) in
          M.rust_cast (M.read (| M.use (M.alloc (| M.read (| t |) |)) |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "from_mut" (from_mut T).
    (*
        pub fn take(&self) -> T {
            self.replace(Default::default())
        }
    *)
    Definition take (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_associated_function (|
              Ty.apply (Ty.path "core::cell::Cell") [] [ T ],
              "replace",
              []
            |),
            [
              M.read (| self |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_take :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "take" (take T).
  End Impl_core_cell_Cell_T.
  
  
  
  
  Module Impl_core_ops_unsize_CoerceUnsized_where_core_ops_unsize_CoerceUnsized_T_U_core_cell_Cell_U_for_core_cell_Cell_T.
    Definition Self (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    Axiom Implements :
      forall (T U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::CoerceUnsized"
        (Self T U)
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "core::cell::Cell") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_CoerceUnsized_where_core_ops_unsize_CoerceUnsized_T_U_core_cell_Cell_U_for_core_cell_Cell_T.
  
  Module Impl_core_ops_unsize_DispatchFromDyn_where_core_ops_unsize_DispatchFromDyn_T_U_core_cell_Cell_U_for_core_cell_Cell_T.
    Definition Self (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    Axiom Implements :
      forall (T U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::DispatchFromDyn"
        (Self T U)
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "core::cell::Cell") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_DispatchFromDyn_where_core_ops_unsize_DispatchFromDyn_T_U_core_cell_Cell_U_for_core_cell_Cell_T.
  
  Module Impl_core_cell_Cell_slice_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.apply (Ty.path "slice") [] [ T ] ].
    
    (*
        pub fn as_slice_of_cells(&self) -> &[Cell<T>] {
            // SAFETY: `Cell<T>` has the same memory layout as `T`.
            unsafe { &*(self as *const Cell<[T]> as *const [Cell<T>]) }
        }
    *)
    Definition as_slice_of_cells
        (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.rust_cast (M.read (| M.use (M.alloc (| M.read (| self |) |)) |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_slice_of_cells :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_slice_of_cells" (as_slice_of_cells T).
  End Impl_core_cell_Cell_slice_T.
  
  Module Impl_core_cell_Cell_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ].
    
    (*
        pub fn as_array_of_cells(&self) -> &[Cell<T>; N] {
            // SAFETY: `Cell<T>` has the same memory layout as `T`.
            unsafe { &*(self as *const Cell<[T; N]> as *const [Cell<T>; N]) }
        }
    *)
    Definition as_array_of_cells
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.rust_cast (M.read (| M.use (M.alloc (| M.read (| self |) |)) |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_array_of_cells :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "as_array_of_cells" (as_array_of_cells N T).
  End Impl_core_cell_Cell_array_N_T.
  
  (* StructRecord
    {
      name := "RefCell";
      const_params := [];
      ty_params := [ "T" ];
      fields :=
        [
          ("borrow", Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ]);
          ("value", Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ])
        ];
    } *)
  
  (* StructTuple
    {
      name := "BorrowError";
      const_params := [];
      ty_params := [];
      fields := [];
    } *)
  
  Module Impl_core_fmt_Debug_for_core_cell_BorrowError.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            let mut builder = f.debug_struct("BorrowError");
    
            #[cfg(feature = "debug_refcell")]
            builder.field("location", self.location);
    
            builder.finish()
        }
    *)
    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.read (|
            let~ builder :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::Formatter",
                    "debug_struct",
                    []
                  |),
                  [ M.read (| f |); M.read (| Value.String "BorrowError" |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::builders::DebugStruct",
                  "finish",
                  []
                |),
                [ builder ]
              |)
            |)
          |)))
      | _, _, _ => 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_cell_BorrowError.
  
  Module Impl_core_fmt_Display_for_core_cell_BorrowError.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            Display::fmt("already mutably borrowed", f)
        }
    *)
    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_trait_method (| "core::fmt::Display", Ty.path "str", [], "fmt", [] |),
            [ M.read (| Value.String "already mutably borrowed" |); M.read (| f |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_core_cell_BorrowError.
  
  (* StructTuple
    {
      name := "BorrowMutError";
      const_params := [];
      ty_params := [];
      fields := [];
    } *)
  
  Module Impl_core_fmt_Debug_for_core_cell_BorrowMutError.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowMutError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            let mut builder = f.debug_struct("BorrowMutError");
    
            #[cfg(feature = "debug_refcell")]
            builder.field("location", self.location);
    
            builder.finish()
        }
    *)
    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.read (|
            let~ builder :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::Formatter",
                    "debug_struct",
                    []
                  |),
                  [ M.read (| f |); M.read (| Value.String "BorrowMutError" |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::builders::DebugStruct",
                  "finish",
                  []
                |),
                [ builder ]
              |)
            |)
          |)))
      | _, _, _ => 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_cell_BorrowMutError.
  
  Module Impl_core_fmt_Display_for_core_cell_BorrowMutError.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowMutError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            Display::fmt("already borrowed", f)
        }
    *)
    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_trait_method (| "core::fmt::Display", Ty.path "str", [], "fmt", [] |),
            [ M.read (| Value.String "already borrowed" |); M.read (| f |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_core_cell_BorrowMutError.
  
  (*
  fn panic_already_borrowed(err: BorrowMutError) -> ! {
      panic!("already borrowed: {:?}", err)
  }
  *)
  Definition panic_already_borrowed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ err ] =>
      ltac:(M.monadic
        (let err := M.alloc (| err |) in
        M.call_closure (|
          M.get_function (| "core::panicking::panic_fmt", [] |),
          [
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
              [
                M.alloc (| Value.Array [ M.read (| Value.String "already borrowed: " |) ] |);
                M.alloc (|
                  Value.Array
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::rt::Argument",
                          "new_debug",
                          [ Ty.path "core::cell::BorrowMutError" ]
                        |),
                        [ err ]
                      |)
                    ]
                |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_panic_already_borrowed :
    M.IsFunction "core::cell::panic_already_borrowed" panic_already_borrowed.
  
  (*
  fn panic_already_mutably_borrowed(err: BorrowError) -> ! {
      panic!("already mutably borrowed: {:?}", err)
  }
  *)
  Definition panic_already_mutably_borrowed
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ err ] =>
      ltac:(M.monadic
        (let err := M.alloc (| err |) in
        M.call_closure (|
          M.get_function (| "core::panicking::panic_fmt", [] |),
          [
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
              [
                M.alloc (|
                  Value.Array [ M.read (| Value.String "already mutably borrowed: " |) ]
                |);
                M.alloc (|
                  Value.Array
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::rt::Argument",
                          "new_debug",
                          [ Ty.path "core::cell::BorrowError" ]
                        |),
                        [ err ]
                      |)
                    ]
                |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_panic_already_mutably_borrowed :
    M.IsFunction "core::cell::panic_already_mutably_borrowed" panic_already_mutably_borrowed.
  
  Axiom BorrowFlag : (Ty.path "core::cell::BorrowFlag") = (Ty.path "isize").
  
  Definition value_UNUSED : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Isize 0 |))).
  
  (*
  fn is_writing(x: BorrowFlag) -> bool {
      x < UNUSED
  }
  *)
  Definition is_writing (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ x ] =>
      ltac:(M.monadic
        (let x := M.alloc (| x |) in
        BinOp.lt (| M.read (| x |), M.read (| M.get_constant (| "core::cell::UNUSED" |) |) |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_is_writing : M.IsFunction "core::cell::is_writing" is_writing.
  
  (*
  fn is_reading(x: BorrowFlag) -> bool {
      x > UNUSED
  }
  *)
  Definition is_reading (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ x ] =>
      ltac:(M.monadic
        (let x := M.alloc (| x |) in
        BinOp.gt (| M.read (| x |), M.read (| M.get_constant (| "core::cell::UNUSED" |) |) |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_is_reading : M.IsFunction "core::cell::is_reading" is_reading.
  
  Module Impl_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    (*
        pub const fn new(value: T) -> RefCell<T> {
            RefCell {
                value: UnsafeCell::new(value),
                borrow: Cell::new(UNUSED),
                #[cfg(feature = "debug_refcell")]
                borrowed_at: Cell::new(None),
            }
        }
    *)
    Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          Value.StructRecord
            "core::cell::RefCell"
            [
              ("value",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
                    "new",
                    []
                  |),
                  [ M.read (| value |) ]
                |));
              ("borrow",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "new",
                    []
                  |),
                  [ M.read (| M.get_constant (| "core::cell::UNUSED" |) |) ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "new" (new T).
    
    (*
        pub const fn into_inner(self) -> T {
            // Since this function takes `self` (the `RefCell`) by value, the
            // compiler statically verifies that it is not currently borrowed.
            self.value.into_inner()
        }
    *)
    Definition into_inner (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_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "into_inner",
              []
            |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (| self, "core::cell::RefCell", "value" |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_inner :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "into_inner" (into_inner T).
    
    (*
        pub fn replace(&self, t: T) -> T {
            mem::replace(&mut *self.borrow_mut(), t)
        }
    *)
    Definition replace (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; t ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let t := M.alloc (| t |) in
          M.call_closure (|
            M.get_function (| "core::mem::replace", [ T ] |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::DerefMut",
                  Ty.apply (Ty.path "core::cell::RefMut") [] [ T ],
                  [],
                  "deref_mut",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow_mut",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |);
              M.read (| t |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_replace :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "replace" (replace T).
    
    (*
        pub fn replace_with<F: FnOnce(&mut T) -> T>(&self, f: F) -> T {
            let mut_borrow = &mut *self.borrow_mut();
            let replacement = f(mut_borrow);
            mem::replace(mut_borrow, replacement)
        }
    *)
    Definition replace_with (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ mut_borrow :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::deref::DerefMut",
                    Ty.apply (Ty.path "core::cell::RefMut") [] [ T ],
                    [],
                    "deref_mut",
                    []
                  |),
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                          "borrow_mut",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |)
                  ]
                |)
              |) in
            let~ replacement :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::function::FnOnce",
                    F,
                    [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ] ],
                    "call_once",
                    []
                  |),
                  [ M.read (| f |); Value.Tuple [ M.read (| mut_borrow |) ] ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::mem::replace", [ T ] |),
                [ M.read (| mut_borrow |); M.read (| replacement |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_replace_with :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "replace_with" (replace_with T).
    
    (*
        pub fn swap(&self, other: &Self) {
            mem::swap(&mut *self.borrow_mut(), &mut *other.borrow_mut())
        }
    *)
    Definition swap (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_function (| "core::mem::swap", [ T ] |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::DerefMut",
                  Ty.apply (Ty.path "core::cell::RefMut") [] [ T ],
                  [],
                  "deref_mut",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow_mut",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::DerefMut",
                  Ty.apply (Ty.path "core::cell::RefMut") [] [ T ],
                  [],
                  "deref_mut",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow_mut",
                        []
                      |),
                      [ M.read (| other |) ]
                    |)
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_swap :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "swap" (swap T).
    (*
        pub fn borrow(&self) -> Ref<'_, T> {
            match self.try_borrow() {
                Ok(b) => b,
                Err(err) => panic_already_mutably_borrowed(err),
            }
        }
    *)
    Definition borrow (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 (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                    "try_borrow",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let b := M.copy (| γ0_0 |) in
                    b));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let err := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::cell::panic_already_mutably_borrowed", [] |),
                          [ M.read (| err |) ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_borrow :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "borrow" (borrow T).
    
    (*
        pub fn try_borrow(&self) -> Result<Ref<'_, T>, BorrowError> {
            match BorrowRef::new(&self.borrow) {
                Some(b) => {
                    #[cfg(feature = "debug_refcell")]
                    {
                        // `borrowed_at` is always the *first* active borrow
                        if b.borrow.get() == 1 {
                            self.borrowed_at.set(Some(crate::panic::Location::caller()));
                        }
                    }
    
                    // SAFETY: `BorrowRef` ensures that there is only immutable access
                    // to the value while borrowed.
                    let value = unsafe { NonNull::new_unchecked(self.value.get()) };
                    Ok(Ref { value, borrow: b })
                }
                None => Err(BorrowError {
                    // If a borrow occurred, then we must already have an outstanding borrow,
                    // so `borrowed_at` will be `Some`
                    #[cfg(feature = "debug_refcell")]
                    location: self.borrowed_at.get().unwrap(),
                }),
            }
        }
    *)
    Definition try_borrow (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 (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::cell::BorrowRef", "new", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::cell::RefCell",
                      "borrow"
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let b := M.copy (| γ0_0 |) in
                    let~ value :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            "new_unchecked",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
                                "get",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::cell::RefCell",
                                  "value"
                                |)
                              ]
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructRecord
                            "core::cell::Ref"
                            [ ("value", M.read (| value |)); ("borrow", M.read (| b |)) ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [ Value.StructTuple "core::cell::BorrowError" [] ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_try_borrow :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "try_borrow" (try_borrow T).
    
    (*
        pub fn borrow_mut(&self) -> RefMut<'_, T> {
            match self.try_borrow_mut() {
                Ok(b) => b,
                Err(err) => panic_already_borrowed(err),
            }
        }
    *)
    Definition borrow_mut (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 (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                    "try_borrow_mut",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let b := M.copy (| γ0_0 |) in
                    b));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    let err := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::cell::panic_already_borrowed", [] |),
                          [ M.read (| err |) ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_borrow_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "borrow_mut" (borrow_mut T).
    
    (*
        pub fn try_borrow_mut(&self) -> Result<RefMut<'_, T>, BorrowMutError> {
            match BorrowRefMut::new(&self.borrow) {
                Some(b) => {
                    #[cfg(feature = "debug_refcell")]
                    {
                        self.borrowed_at.set(Some(crate::panic::Location::caller()));
                    }
    
                    // SAFETY: `BorrowRefMut` guarantees unique access.
                    let value = unsafe { NonNull::new_unchecked(self.value.get()) };
                    Ok(RefMut { value, borrow: b, marker: PhantomData })
                }
                None => Err(BorrowMutError {
                    // If a borrow occurred, then we must already have an outstanding borrow,
                    // so `borrowed_at` will be `Some`
                    #[cfg(feature = "debug_refcell")]
                    location: self.borrowed_at.get().unwrap(),
                }),
            }
        }
    *)
    Definition try_borrow_mut
        (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 (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::cell::BorrowRefMut", "new", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::cell::RefCell",
                      "borrow"
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let b := M.copy (| γ0_0 |) in
                    let~ value :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                            "new_unchecked",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
                                "get",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "core::cell::RefCell",
                                  "value"
                                |)
                              ]
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructRecord
                            "core::cell::RefMut"
                            [
                              ("value", M.read (| value |));
                              ("borrow", M.read (| b |));
                              ("marker", Value.StructTuple "core::marker::PhantomData" [])
                            ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [ Value.StructTuple "core::cell::BorrowMutError" [] ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_try_borrow_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "try_borrow_mut" (try_borrow_mut T).
    
    (*
        pub fn as_ptr(&self) -> *mut T {
            self.value.get()
        }
    *)
    Definition as_ptr (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_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "get",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::cell::RefCell",
                "value"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_ptr :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_ptr" (as_ptr T).
    
    (*
        pub fn get_mut(&mut self) -> &mut T {
            self.value.get_mut()
        }
    *)
    Definition get_mut (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_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "get_mut",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::cell::RefCell",
                "value"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "get_mut" (get_mut T).
    
    (*
        pub fn undo_leak(&mut self) -> &mut T {
            *self.borrow.get_mut() = UNUSED;
            self.get_mut()
        }
    *)
    Definition undo_leak (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 (|
            let~ _ :=
              M.write (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "get_mut",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::cell::RefCell",
                      "borrow"
                    |)
                  ]
                |),
                M.read (| M.get_constant (| "core::cell::UNUSED" |) |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                  "get_mut",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_undo_leak :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "undo_leak" (undo_leak T).
    
    (*
        pub unsafe fn try_borrow_unguarded(&self) -> Result<&T, BorrowError> {
            if !is_writing(self.borrow.get()) {
                // SAFETY: We check that nobody is actively writing now, but it is
                // the caller's responsibility to ensure that nobody writes until
                // the returned reference is no longer in use.
                // Also, `self.value.get()` refers to the value owned by `self`
                // and is thus guaranteed to be valid for the lifetime of `self`.
                Ok(unsafe { &*self.value.get() })
            } else {
                Err(BorrowError {
                    // If a borrow occurred, then we must already have an outstanding borrow,
                    // so `borrowed_at` will be `Some`
                    #[cfg(feature = "debug_refcell")]
                    location: self.borrowed_at.get().unwrap(),
                })
            }
        }
    *)
    Definition try_borrow_unguarded
        (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 (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            M.call_closure (|
                              M.get_function (| "core::cell::is_writing", [] |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                                    "get",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::cell::RefCell",
                                      "borrow"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
                              "get",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::cell::RefCell",
                                "value"
                              |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [ Value.StructTuple "core::cell::BorrowError" [] ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_try_borrow_unguarded :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "try_borrow_unguarded" (try_borrow_unguarded T).
    (*
        pub fn take(&self) -> T {
            self.replace(Default::default())
        }
    *)
    Definition take (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_associated_function (|
              Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
              "replace",
              []
            |),
            [
              M.read (| self |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_take :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "take" (take T).
  End Impl_core_cell_RefCell_T.
  
  
  
  Module Impl_core_marker_Send_where_core_marker_Sized_T_where_core_marker_Send_T_for_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Send"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Send_where_core_marker_Sized_T_where_core_marker_Send_T_for_core_cell_RefCell_T.
  
  Module Impl_core_marker_Sync_where_core_marker_Sized_T_for_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Sync"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Sync_where_core_marker_Sized_T_for_core_cell_RefCell_T.
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    (*
        fn clone(&self) -> RefCell<T> {
            RefCell::new(self.borrow().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
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
              "new",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                            "borrow",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn clone_from(&mut self, source: &Self) {
            self.get_mut().clone_from(&source.borrow())
        }
    *)
    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.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                  "get_mut",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| source |) ]
                    |)
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => 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_cell_RefCell_T.
  
  Module Impl_core_default_Default_where_core_default_Default_T_for_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    (*
        fn default() -> RefCell<T> {
            RefCell::new(Default::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
          (M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
              "new",
              []
            |),
            [
              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_cell_RefCell_T.
  
  Module Impl_core_cmp_PartialEq_where_core_marker_Sized_T_where_core_cmp_PartialEq_T_for_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    (*
        fn eq(&self, other: &RefCell<T>) -> bool {
            *self.borrow() == *other.borrow()
        }
    *)
    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.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| other |) ]
                    |)
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => 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_marker_Sized_T_where_core_cmp_PartialEq_T_for_core_cell_RefCell_T.
  
  Module Impl_core_cmp_Eq_where_core_marker_Sized_T_where_core_cmp_Eq_T_for_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance "core::cmp::Eq" (Self T) (* Trait polymorphic types *) [] (* Instance *) [].
  End Impl_core_cmp_Eq_where_core_marker_Sized_T_where_core_cmp_Eq_T_for_core_cell_RefCell_T.
  
  Module Impl_core_cmp_PartialOrd_where_core_marker_Sized_T_where_core_cmp_PartialOrd_T_for_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    (*
        fn partial_cmp(&self, other: &RefCell<T>) -> Option<Ordering> {
            self.borrow().partial_cmp(&*other.borrow())
        }
    *)
    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.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| other |) ]
                    |)
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn lt(&self, other: &RefCell<T>) -> bool {
            *self.borrow() < *other.borrow()
        }
    *)
    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.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| other |) ]
                    |)
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn le(&self, other: &RefCell<T>) -> bool {
            *self.borrow() <= *other.borrow()
        }
    *)
    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.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| other |) ]
                    |)
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn gt(&self, other: &RefCell<T>) -> bool {
            *self.borrow() > *other.borrow()
        }
    *)
    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.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| other |) ]
                    |)
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn ge(&self, other: &RefCell<T>) -> bool {
            *self.borrow() >= *other.borrow()
        }
    *)
    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.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| other |) ]
                    |)
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => 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_marker_Sized_T_where_core_cmp_PartialOrd_T_for_core_cell_RefCell_T.
  
  Module Impl_core_cmp_Ord_where_core_marker_Sized_T_where_core_cmp_Ord_T_for_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    (*
        fn cmp(&self, other: &RefCell<T>) -> Ordering {
            self.borrow().cmp(&*other.borrow())
        }
    *)
    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.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
                        "borrow",
                        []
                      |),
                      [ M.read (| other |) ]
                    |)
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => 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_marker_Sized_T_where_core_cmp_Ord_T_for_core_cell_RefCell_T.
  
  Module Impl_core_convert_From_T_for_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    (*
        fn from(t: T) -> RefCell<T> {
            RefCell::new(t)
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ t ] =>
        ltac:(M.monadic
          (let t := M.alloc (| t |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::cell::RefCell") [] [ T ],
              "new",
              []
            |),
            [ M.read (| t |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_T_for_core_cell_RefCell_T.
  
  Module Impl_core_ops_unsize_CoerceUnsized_where_core_ops_unsize_CoerceUnsized_T_U_core_cell_RefCell_U_for_core_cell_RefCell_T.
    Definition Self (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    Axiom Implements :
      forall (T U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::CoerceUnsized"
        (Self T U)
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "core::cell::RefCell") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_CoerceUnsized_where_core_ops_unsize_CoerceUnsized_T_U_core_cell_RefCell_U_for_core_cell_RefCell_T.
  
  (* StructRecord
    {
      name := "BorrowRef";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("borrow",
            Ty.apply
              (Ty.path "&")
              []
              [ Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ] ])
        ];
    } *)
  
  Module Impl_core_cell_BorrowRef.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowRef".
    
    (*
        fn new(borrow: &'b Cell<BorrowFlag>) -> Option<BorrowRef<'b>> {
            let b = borrow.get().wrapping_add(1);
            if !is_reading(b) {
                // Incrementing borrow can result in a non-reading value (<= 0) in these cases:
                // 1. It was < 0, i.e. there are writing borrows, so we can't allow a read borrow
                //    due to Rust's reference aliasing rules
                // 2. It was isize::MAX (the max amount of reading borrows) and it overflowed
                //    into isize::MIN (the max amount of writing borrows) so we can't allow
                //    an additional read borrow because isize can't represent so many read borrows
                //    (this can only happen if you mem::forget more than a small constant amount of
                //    `Ref`s, which is not good practice)
                None
            } else {
                // Incrementing borrow can result in a reading value (> 0) in these cases:
                // 1. It was = 0, i.e. it wasn't borrowed, and we are taking the first read borrow
                // 2. It was > 0 and < isize::MAX, i.e. there were read borrows, and isize
                //    is large enough to represent having one more read borrow
                borrow.set(b);
                Some(BorrowRef { borrow })
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ borrow ] =>
        ltac:(M.monadic
          (let borrow := M.alloc (| borrow |) in
          M.read (|
            let~ b :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "isize", "wrapping_add", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                        "get",
                        []
                      |),
                      [ M.read (| borrow |) ]
                    |);
                    Value.Integer IntegerKind.Isize 1
                  ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            M.call_closure (|
                              M.get_function (| "core::cell::is_reading", [] |),
                              [ M.read (| b |) ]
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                            "set",
                            []
                          |),
                          [ M.read (| borrow |); M.read (| b |) ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          Value.StructRecord
                            "core::cell::BorrowRef"
                            [ ("borrow", M.read (| borrow |)) ]
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  End Impl_core_cell_BorrowRef.
  
  Module Impl_core_ops_drop_Drop_for_core_cell_BorrowRef.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowRef".
    
    (*
        fn drop(&mut self) {
            let borrow = self.borrow.get();
            debug_assert!(is_reading(borrow));
            self.borrow.set(borrow - 1);
        }
    *)
    Definition drop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ borrow :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "get",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::cell::BorrowRef",
                        "borrow"
                      |)
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use (M.alloc (| Value.Bool true |)) 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.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_function (| "core::cell::is_reading", [] |),
                                          [ M.read (| borrow |) ]
                                        |)
                                      |)
                                    |)) 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: is_reading(borrow)"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) 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.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "set",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::cell::BorrowRef",
                        "borrow"
                      |)
                    |);
                    BinOp.Wrap.sub (| M.read (| borrow |), Value.Integer IntegerKind.Isize 1 |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::drop::Drop"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("drop", InstanceField.Method drop) ].
  End Impl_core_ops_drop_Drop_for_core_cell_BorrowRef.
  
  Module Impl_core_clone_Clone_for_core_cell_BorrowRef.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowRef".
    
    (*
        fn clone(&self) -> Self {
            // Since this Ref exists, we know the borrow flag
            // is a reading borrow.
            let borrow = self.borrow.get();
            debug_assert!(is_reading(borrow));
            // Prevent the borrow counter from overflowing into
            // a writing borrow.
            assert!(borrow != BorrowFlag::MAX);
            self.borrow.set(borrow + 1);
            BorrowRef { borrow: self.borrow }
        }
    *)
    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 (|
            let~ borrow :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "get",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::cell::BorrowRef",
                        "borrow"
                      |)
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use (M.alloc (| Value.Bool true |)) 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.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_function (| "core::cell::is_reading", [] |),
                                          [ M.read (| borrow |) ]
                                        |)
                                      |)
                                    |)) 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: is_reading(borrow)"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              BinOp.ne (|
                                M.read (| borrow |),
                                M.read (| M.get_constant (| "core::num::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: borrow != BorrowFlag::MAX"
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "set",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::cell::BorrowRef",
                        "borrow"
                      |)
                    |);
                    BinOp.Wrap.add (| M.read (| borrow |), Value.Integer IntegerKind.Isize 1 |)
                  ]
                |)
              |) in
            M.alloc (|
              Value.StructRecord
                "core::cell::BorrowRef"
                [
                  ("borrow",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::cell::BorrowRef",
                        "borrow"
                      |)
                    |))
                ]
            |)
          |)))
      | _, _, _ => 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_cell_BorrowRef.
  
  (* StructRecord
    {
      name := "Ref";
      const_params := [];
      ty_params := [ "T" ];
      fields :=
        [
          ("value", Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]);
          ("borrow", Ty.path "core::cell::BorrowRef")
        ];
    } *)
  
  Module Impl_core_ops_deref_Deref_where_core_marker_Sized_T_for_core_cell_Ref_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Ref") [] [ T ].
    
    (*     type Target = T; *)
    Definition _Target (T : Ty.t) : Ty.t := T.
    
    (*
        fn deref(&self) -> &T {
            // SAFETY: the value is accessible as long as we hold our borrow.
            unsafe { self.value.as_ref() }
        }
    *)
    Definition deref (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_associated_function (|
              Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
              "as_ref",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::cell::Ref",
                "value"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::Deref"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("Target", InstanceField.Ty (_Target T)); ("deref", InstanceField.Method (deref T)) ].
  End Impl_core_ops_deref_Deref_where_core_marker_Sized_T_for_core_cell_Ref_T.
  
  Module Impl_core_ops_deref_DerefPure_where_core_marker_Sized_T_for_core_cell_Ref_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Ref") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::DerefPure"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_ops_deref_DerefPure_where_core_marker_Sized_T_for_core_cell_Ref_T.
  
  Module Impl_core_cell_Ref_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Ref") [] [ T ].
    
    (*
        pub fn clone(orig: &Ref<'b, T>) -> Ref<'b, T> {
            Ref { value: orig.value, borrow: orig.borrow.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
      | [], [], [ orig ] =>
        ltac:(M.monadic
          (let orig := M.alloc (| orig |) in
          Value.StructRecord
            "core::cell::Ref"
            [
              ("value",
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| orig |),
                    "core::cell::Ref",
                    "value"
                  |)
                |));
              ("borrow",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "core::cell::BorrowRef",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| orig |),
                      "core::cell::Ref",
                      "borrow"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_clone :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "clone" (clone T).
    
    (*
        pub fn map<U: ?Sized, F>(orig: Ref<'b, T>, f: F) -> Ref<'b, U>
        where
            F: FnOnce(&T) -> &U,
        {
            Ref { value: NonNull::from(f(&*orig)), borrow: orig.borrow }
        }
    *)
    Definition map (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; F ], [ orig; f ] =>
        ltac:(M.monadic
          (let orig := M.alloc (| orig |) in
          let f := M.alloc (| f |) in
          Value.StructRecord
            "core::cell::Ref"
            [
              ("value",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ U ],
                    [ Ty.apply (Ty.path "&") [] [ U ] ],
                    "from",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::function::FnOnce",
                        F,
                        [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                        "call_once",
                        []
                      |),
                      [
                        M.read (| f |);
                        Value.Tuple
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::Deref",
                                Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                                [],
                                "deref",
                                []
                              |),
                              [ orig ]
                            |)
                          ]
                      ]
                    |)
                  ]
                |));
              ("borrow",
                M.read (|
                  M.SubPointer.get_struct_record_field (| orig, "core::cell::Ref", "borrow" |)
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "map" (map T).
    
    (*
        pub fn filter_map<U: ?Sized, F>(orig: Ref<'b, T>, f: F) -> Result<Ref<'b, U>, Self>
        where
            F: FnOnce(&T) -> Option<&U>,
        {
            match f(&*orig) {
                Some(value) => Ok(Ref { value: NonNull::from(value), borrow: orig.borrow }),
                None => Err(orig),
            }
        }
    *)
    Definition filter_map (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; F ], [ orig; f ] =>
        ltac:(M.monadic
          (let orig := M.alloc (| orig |) in
          let f := M.alloc (| f |) 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 ] ] ],
                    "call_once",
                    []
                  |),
                  [
                    M.read (| f |);
                    Value.Tuple
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                            [],
                            "deref",
                            []
                          |),
                          [ orig ]
                        |)
                      ]
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let value := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructRecord
                            "core::cell::Ref"
                            [
                              ("value",
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ U ],
                                    [ Ty.apply (Ty.path "&") [] [ U ] ],
                                    "from",
                                    []
                                  |),
                                  [ M.read (| value |) ]
                                |));
                              ("borrow",
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    orig,
                                    "core::cell::Ref",
                                    "borrow"
                                  |)
                                |))
                            ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.StructTuple "core::result::Result::Err" [ M.read (| orig |) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_filter_map :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "filter_map" (filter_map T).
    
    (*
        pub fn map_split<U: ?Sized, V: ?Sized, F>(orig: Ref<'b, T>, f: F) -> (Ref<'b, U>, Ref<'b, V>)
        where
            F: FnOnce(&T) -> (&U, &V),
        {
            let (a, b) = f(&*orig);
            let borrow = orig.borrow.clone();
            (Ref { value: NonNull::from(a), borrow }, Ref {
                value: NonNull::from(b),
                borrow: orig.borrow,
            })
        }
    *)
    Definition map_split (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; V; F ], [ orig; f ] =>
        ltac:(M.monadic
          (let orig := M.alloc (| orig |) in
          let f := M.alloc (| f |) 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 ] ] ],
                    "call_once",
                    []
                  |),
                  [
                    M.read (| f |);
                    Value.Tuple
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                            [],
                            "deref",
                            []
                          |),
                          [ orig ]
                        |)
                      ]
                  ]
                |)
              |),
              [
                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 a := M.copy (| γ0_0 |) in
                    let b := M.copy (| γ0_1 |) in
                    let~ borrow :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::clone::Clone",
                            Ty.path "core::cell::BorrowRef",
                            [],
                            "clone",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              orig,
                              "core::cell::Ref",
                              "borrow"
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.Tuple
                        [
                          Value.StructRecord
                            "core::cell::Ref"
                            [
                              ("value",
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ U ],
                                    [ Ty.apply (Ty.path "&") [] [ U ] ],
                                    "from",
                                    []
                                  |),
                                  [ M.read (| a |) ]
                                |));
                              ("borrow", M.read (| borrow |))
                            ];
                          Value.StructRecord
                            "core::cell::Ref"
                            [
                              ("value",
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ V ],
                                    [ Ty.apply (Ty.path "&") [] [ V ] ],
                                    "from",
                                    []
                                  |),
                                  [ M.read (| b |) ]
                                |));
                              ("borrow",
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    orig,
                                    "core::cell::Ref",
                                    "borrow"
                                  |)
                                |))
                            ]
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map_split :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "map_split" (map_split T).
    
    (*
        pub fn leak(orig: Ref<'b, T>) -> &'b T {
            // By forgetting this Ref we ensure that the borrow counter in the RefCell can't go back to
            // UNUSED within the lifetime `'b`. Resetting the reference tracking state would require a
            // unique reference to the borrowed RefCell. No further mutable references can be created
            // from the original cell.
            mem::forget(orig.borrow);
            // SAFETY: after forgetting, we can form a reference for the rest of lifetime `'b`.
            unsafe { orig.value.as_ref() }
        }
    *)
    Definition leak (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ orig ] =>
        ltac:(M.monadic
          (let orig := M.alloc (| orig |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::mem::forget", [ Ty.path "core::cell::BorrowRef" ] |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (| orig, "core::cell::Ref", "borrow" |)
                    |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                  "as_ref",
                  []
                |),
                [ M.SubPointer.get_struct_record_field (| orig, "core::cell::Ref", "value" |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_leak :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "leak" (leak T).
  End Impl_core_cell_Ref_T.
  
  Module Impl_core_ops_unsize_CoerceUnsized_where_core_marker_Sized_T_where_core_marker_Unsize_T_U_where_core_marker_Sized_U_core_cell_Ref_U_for_core_cell_Ref_T.
    Definition Self (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Ref") [] [ T ].
    
    Axiom Implements :
      forall (T U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::CoerceUnsized"
        (Self T U)
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "core::cell::Ref") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_CoerceUnsized_where_core_marker_Sized_T_where_core_marker_Unsize_T_U_where_core_marker_Sized_U_core_cell_Ref_U_for_core_cell_Ref_T.
  
  Module Impl_core_fmt_Display_where_core_marker_Sized_T_where_core_fmt_Display_T_for_core_cell_Ref_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Ref") [] [ T ].
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            ( **self).fmt(f)
        }
    *)
    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_trait_method (| "core::fmt::Display", T, [], "fmt", [] |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::Ref") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::fmt::Display"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
  End Impl_core_fmt_Display_where_core_marker_Sized_T_where_core_fmt_Display_T_for_core_cell_Ref_T.
  
  Module Impl_core_cell_RefMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefMut") [] [ T ].
    
    (*
        pub fn map<U: ?Sized, F>(mut orig: RefMut<'b, T>, f: F) -> RefMut<'b, U>
        where
            F: FnOnce(&mut T) -> &mut U,
        {
            let value = NonNull::from(f(&mut *orig));
            RefMut { value, borrow: orig.borrow, marker: PhantomData }
        }
    *)
    Definition map (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; F ], [ orig; f ] =>
        ltac:(M.monadic
          (let orig := M.alloc (| orig |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ value :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ U ],
                    [ Ty.apply (Ty.path "&mut") [] [ U ] ],
                    "from",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::function::FnOnce",
                        F,
                        [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ] ],
                        "call_once",
                        []
                      |),
                      [
                        M.read (| f |);
                        Value.Tuple
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::DerefMut",
                                Ty.apply (Ty.path "core::cell::RefMut") [] [ T ],
                                [],
                                "deref_mut",
                                []
                              |),
                              [ orig ]
                            |)
                          ]
                      ]
                    |)
                  ]
                |)
              |) in
            M.alloc (|
              Value.StructRecord
                "core::cell::RefMut"
                [
                  ("value", M.read (| value |));
                  ("borrow",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        orig,
                        "core::cell::RefMut",
                        "borrow"
                      |)
                    |));
                  ("marker", Value.StructTuple "core::marker::PhantomData" [])
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "map" (map T).
    
    (*
        pub fn filter_map<U: ?Sized, F>(mut orig: RefMut<'b, T>, f: F) -> Result<RefMut<'b, U>, Self>
        where
            F: FnOnce(&mut T) -> Option<&mut U>,
        {
            // SAFETY: function holds onto an exclusive reference for the duration
            // of its call through `orig`, and the pointer is only de-referenced
            // inside of the function call never allowing the exclusive reference to
            // escape.
            match f(&mut *orig) {
                Some(value) => {
                    Ok(RefMut { value: NonNull::from(value), borrow: orig.borrow, marker: PhantomData })
                }
                None => Err(orig),
            }
        }
    *)
    Definition filter_map (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; F ], [ orig; f ] =>
        ltac:(M.monadic
          (let orig := M.alloc (| orig |) in
          let f := M.alloc (| f |) 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 "&mut") [] [ T ] ] ],
                    "call_once",
                    []
                  |),
                  [
                    M.read (| f |);
                    Value.Tuple
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::DerefMut",
                            Ty.apply (Ty.path "core::cell::RefMut") [] [ T ],
                            [],
                            "deref_mut",
                            []
                          |),
                          [ orig ]
                        |)
                      ]
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let value := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          Value.StructRecord
                            "core::cell::RefMut"
                            [
                              ("value",
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ U ],
                                    [ Ty.apply (Ty.path "&mut") [] [ U ] ],
                                    "from",
                                    []
                                  |),
                                  [ M.read (| value |) ]
                                |));
                              ("borrow",
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    orig,
                                    "core::cell::RefMut",
                                    "borrow"
                                  |)
                                |));
                              ("marker", Value.StructTuple "core::marker::PhantomData" [])
                            ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.StructTuple "core::result::Result::Err" [ M.read (| orig |) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_filter_map :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "filter_map" (filter_map T).
    
    (*
        pub fn map_split<U: ?Sized, V: ?Sized, F>(
            mut orig: RefMut<'b, T>,
            f: F,
        ) -> (RefMut<'b, U>, RefMut<'b, V>)
        where
            F: FnOnce(&mut T) -> (&mut U, &mut V),
        {
            let borrow = orig.borrow.clone();
            let (a, b) = f(&mut *orig);
            (RefMut { value: NonNull::from(a), borrow, marker: PhantomData }, RefMut {
                value: NonNull::from(b),
                borrow: orig.borrow,
                marker: PhantomData,
            })
        }
    *)
    Definition map_split (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; V; F ], [ orig; f ] =>
        ltac:(M.monadic
          (let orig := M.alloc (| orig |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ borrow :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::cell::BorrowRefMut", "clone", [] |),
                  [ M.SubPointer.get_struct_record_field (| orig, "core::cell::RefMut", "borrow" |)
                  ]
                |)
              |) in
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::function::FnOnce",
                    F,
                    [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ] ],
                    "call_once",
                    []
                  |),
                  [
                    M.read (| f |);
                    Value.Tuple
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::DerefMut",
                            Ty.apply (Ty.path "core::cell::RefMut") [] [ T ],
                            [],
                            "deref_mut",
                            []
                          |),
                          [ orig ]
                        |)
                      ]
                  ]
                |)
              |),
              [
                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 a := M.copy (| γ0_0 |) in
                    let b := M.copy (| γ0_1 |) in
                    M.alloc (|
                      Value.Tuple
                        [
                          Value.StructRecord
                            "core::cell::RefMut"
                            [
                              ("value",
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ U ],
                                    [ Ty.apply (Ty.path "&mut") [] [ U ] ],
                                    "from",
                                    []
                                  |),
                                  [ M.read (| a |) ]
                                |));
                              ("borrow", M.read (| borrow |));
                              ("marker", Value.StructTuple "core::marker::PhantomData" [])
                            ];
                          Value.StructRecord
                            "core::cell::RefMut"
                            [
                              ("value",
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ V ],
                                    [ Ty.apply (Ty.path "&mut") [] [ V ] ],
                                    "from",
                                    []
                                  |),
                                  [ M.read (| b |) ]
                                |));
                              ("borrow",
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    orig,
                                    "core::cell::RefMut",
                                    "borrow"
                                  |)
                                |));
                              ("marker", Value.StructTuple "core::marker::PhantomData" [])
                            ]
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map_split :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "map_split" (map_split T).
    
    (*
        pub fn leak(mut orig: RefMut<'b, T>) -> &'b mut T {
            // By forgetting this BorrowRefMut we ensure that the borrow counter in the RefCell can't
            // go back to UNUSED within the lifetime `'b`. Resetting the reference tracking state would
            // require a unique reference to the borrowed RefCell. No further references can be created
            // from the original cell within that lifetime, making the current borrow the only
            // reference for the remaining lifetime.
            mem::forget(orig.borrow);
            // SAFETY: after forgetting, we can form a reference for the rest of lifetime `'b`.
            unsafe { orig.value.as_mut() }
        }
    *)
    Definition leak (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ orig ] =>
        ltac:(M.monadic
          (let orig := M.alloc (| orig |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::mem::forget", [ Ty.path "core::cell::BorrowRefMut" ] |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        orig,
                        "core::cell::RefMut",
                        "borrow"
                      |)
                    |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
                  "as_mut",
                  []
                |),
                [ M.SubPointer.get_struct_record_field (| orig, "core::cell::RefMut", "value" |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_leak :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "leak" (leak T).
  End Impl_core_cell_RefMut_T.
  
  (* StructRecord
    {
      name := "BorrowRefMut";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("borrow",
            Ty.apply
              (Ty.path "&")
              []
              [ Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ] ])
        ];
    } *)
  
  Module Impl_core_ops_drop_Drop_for_core_cell_BorrowRefMut.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowRefMut".
    
    (*
        fn drop(&mut self) {
            let borrow = self.borrow.get();
            debug_assert!(is_writing(borrow));
            self.borrow.set(borrow + 1);
        }
    *)
    Definition drop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ borrow :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "get",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::cell::BorrowRefMut",
                        "borrow"
                      |)
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use (M.alloc (| Value.Bool true |)) 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.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_function (| "core::cell::is_writing", [] |),
                                          [ M.read (| borrow |) ]
                                        |)
                                      |)
                                    |)) 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: is_writing(borrow)"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) 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.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "set",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::cell::BorrowRefMut",
                        "borrow"
                      |)
                    |);
                    BinOp.Wrap.add (| M.read (| borrow |), Value.Integer IntegerKind.Isize 1 |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::drop::Drop"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("drop", InstanceField.Method drop) ].
  End Impl_core_ops_drop_Drop_for_core_cell_BorrowRefMut.
  
  Module Impl_core_cell_BorrowRefMut.
    Definition Self : Ty.t := Ty.path "core::cell::BorrowRefMut".
    
    (*
        fn new(borrow: &'b Cell<BorrowFlag>) -> Option<BorrowRefMut<'b>> {
            // NOTE: Unlike BorrowRefMut::clone, new is called to create the initial
            // mutable reference, and so there must currently be no existing
            // references. Thus, while clone increments the mutable refcount, here
            // we explicitly only allow going from UNUSED to UNUSED - 1.
            match borrow.get() {
                UNUSED => {
                    borrow.set(UNUSED - 1);
                    Some(BorrowRefMut { borrow })
                }
                _ => None,
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ borrow ] =>
        ltac:(M.monadic
          (let borrow := M.alloc (| borrow |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "get",
                    []
                  |),
                  [ M.read (| borrow |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_constant_or_break_match (|
                        M.read (| γ |),
                        Value.Integer IntegerKind.Isize 0
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                            "set",
                            []
                          |),
                          [
                            M.read (| borrow |);
                            BinOp.Wrap.sub (|
                              M.read (| M.get_constant (| "core::cell::UNUSED" |) |),
                              Value.Integer IntegerKind.Isize 1
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          Value.StructRecord
                            "core::cell::BorrowRefMut"
                            [ ("borrow", M.read (| borrow |)) ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        fn clone(&self) -> BorrowRefMut<'b> {
            let borrow = self.borrow.get();
            debug_assert!(is_writing(borrow));
            // Prevent the borrow counter from underflowing.
            assert!(borrow != BorrowFlag::MIN);
            self.borrow.set(borrow - 1);
            BorrowRefMut { borrow: self.borrow }
        }
    *)
    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 (|
            let~ borrow :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "get",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::cell::BorrowRefMut",
                        "borrow"
                      |)
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use (M.alloc (| Value.Bool true |)) 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.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_function (| "core::cell::is_writing", [] |),
                                          [ M.read (| borrow |) ]
                                        |)
                                      |)
                                    |)) 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: is_writing(borrow)"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              BinOp.ne (|
                                M.read (| borrow |),
                                M.read (| M.get_constant (| "core::num::MIN" |) |)
                              |)
                            |)
                          |)) 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: borrow != BorrowFlag::MIN"
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::cell::Cell") [] [ Ty.path "isize" ],
                    "set",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::cell::BorrowRefMut",
                        "borrow"
                      |)
                    |);
                    BinOp.Wrap.sub (| M.read (| borrow |), Value.Integer IntegerKind.Isize 1 |)
                  ]
                |)
              |) in
            M.alloc (|
              Value.StructRecord
                "core::cell::BorrowRefMut"
                [
                  ("borrow",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::cell::BorrowRefMut",
                        "borrow"
                      |)
                    |))
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_clone : M.IsAssociatedFunction Self "clone" clone.
  End Impl_core_cell_BorrowRefMut.
  
  (* StructRecord
    {
      name := "RefMut";
      const_params := [];
      ty_params := [ "T" ];
      fields :=
        [
          ("value", Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ]);
          ("borrow", Ty.path "core::cell::BorrowRefMut");
          ("marker",
            Ty.apply
              (Ty.path "core::marker::PhantomData")
              []
              [ Ty.apply (Ty.path "&mut") [] [ T ] ])
        ];
    } *)
  
  Module Impl_core_ops_deref_Deref_where_core_marker_Sized_T_for_core_cell_RefMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefMut") [] [ T ].
    
    (*     type Target = T; *)
    Definition _Target (T : Ty.t) : Ty.t := T.
    
    (*
        fn deref(&self) -> &T {
            // SAFETY: the value is accessible as long as we hold our borrow.
            unsafe { self.value.as_ref() }
        }
    *)
    Definition deref (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_associated_function (|
              Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
              "as_ref",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::cell::RefMut",
                "value"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::Deref"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("Target", InstanceField.Ty (_Target T)); ("deref", InstanceField.Method (deref T)) ].
  End Impl_core_ops_deref_Deref_where_core_marker_Sized_T_for_core_cell_RefMut_T.
  
  Module Impl_core_ops_deref_DerefMut_where_core_marker_Sized_T_for_core_cell_RefMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefMut") [] [ T ].
    
    (*
        fn deref_mut(&mut self) -> &mut T {
            // SAFETY: the value is accessible as long as we hold our borrow.
            unsafe { self.value.as_mut() }
        }
    *)
    Definition deref_mut (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_associated_function (|
              Ty.apply (Ty.path "core::ptr::non_null::NonNull") [] [ T ],
              "as_mut",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::cell::RefMut",
                "value"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::DerefMut"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("deref_mut", InstanceField.Method (deref_mut T)) ].
  End Impl_core_ops_deref_DerefMut_where_core_marker_Sized_T_for_core_cell_RefMut_T.
  
  Module Impl_core_ops_deref_DerefPure_where_core_marker_Sized_T_for_core_cell_RefMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefMut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::deref::DerefPure"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_ops_deref_DerefPure_where_core_marker_Sized_T_for_core_cell_RefMut_T.
  
  Module Impl_core_ops_unsize_CoerceUnsized_where_core_marker_Sized_T_where_core_marker_Unsize_T_U_where_core_marker_Sized_U_core_cell_RefMut_U_for_core_cell_RefMut_T.
    Definition Self (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefMut") [] [ T ].
    
    Axiom Implements :
      forall (T U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::CoerceUnsized"
        (Self T U)
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "core::cell::RefMut") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_CoerceUnsized_where_core_marker_Sized_T_where_core_marker_Unsize_T_U_where_core_marker_Sized_U_core_cell_RefMut_U_for_core_cell_RefMut_T.
  
  Module Impl_core_fmt_Display_where_core_marker_Sized_T_where_core_fmt_Display_T_for_core_cell_RefMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefMut") [] [ T ].
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            ( **self).fmt(f)
        }
    *)
    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_trait_method (| "core::fmt::Display", T, [], "fmt", [] |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::deref::Deref",
                  Ty.apply (Ty.path "core::cell::RefMut") [] [ T ],
                  [],
                  "deref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::fmt::Display"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
  End Impl_core_fmt_Display_where_core_marker_Sized_T_where_core_fmt_Display_T_for_core_cell_RefMut_T.
  
  (* StructRecord
    {
      name := "UnsafeCell";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ ("value", T) ];
    } *)
  
  Module Impl_core_marker_Sync_where_core_marker_Sized_T_for_core_cell_UnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Sync"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Sync_where_core_marker_Sized_T_for_core_cell_UnsafeCell_T.
  
  Module Impl_core_cell_UnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ].
    
    (*
        pub const fn new(value: T) -> UnsafeCell<T> {
            UnsafeCell { value }
        }
    *)
    Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          Value.StructRecord "core::cell::UnsafeCell" [ ("value", M.read (| value |)) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "new" (new T).
    
    (*
        pub const fn into_inner(self) -> T {
            self.value
        }
    *)
    Definition into_inner (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.SubPointer.get_struct_record_field (| self, "core::cell::UnsafeCell", "value" |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_inner :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "into_inner" (into_inner T).
    (*
        pub const fn from_mut(value: &mut T) -> &mut UnsafeCell<T> {
            // SAFETY: `UnsafeCell<T>` has the same memory layout as `T` due to #[repr(transparent)].
            unsafe { &mut *(value as *mut T as *mut UnsafeCell<T>) }
        }
    *)
    Definition from_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          M.rust_cast (M.read (| M.use (M.alloc (| M.read (| value |) |)) |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "from_mut" (from_mut T).
    
    (*
        pub const fn get(&self) -> *mut T {
            // We can just cast the pointer from `UnsafeCell<T>` to `T` because of
            // #[repr(transparent)]. This exploits std's special status, there is
            // no guarantee for user code that this will work in future versions of the compiler!
            self as *const UnsafeCell<T> as *const T as *mut T
        }
    *)
    Definition get (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.rust_cast (M.rust_cast (M.read (| M.use (M.alloc (| M.read (| self |) |)) |)))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "get" (get T).
    
    (*
        pub const fn get_mut(&mut self) -> &mut T {
            &mut self.value
        }
    *)
    Definition get_mut (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.SubPointer.get_struct_record_field (|
            M.read (| self |),
            "core::cell::UnsafeCell",
            "value"
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "get_mut" (get_mut T).
    
    (*
        pub const fn raw_get(this: *const Self) -> *mut T {
            // We can just cast the pointer from `UnsafeCell<T>` to `T` because of
            // #[repr(transparent)]. This exploits std's special status, there is
            // no guarantee for user code that this will work in future versions of the compiler!
            this as *const T as *mut T
        }
    *)
    Definition raw_get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ this ] =>
        ltac:(M.monadic
          (let this := M.alloc (| this |) in
          M.rust_cast (M.rust_cast (M.read (| this |)))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_raw_get :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "raw_get" (raw_get T).
  End Impl_core_cell_UnsafeCell_T.
  
  
  Module Impl_core_default_Default_where_core_default_Default_T_for_core_cell_UnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ].
    
    (*
        fn default() -> UnsafeCell<T> {
            UnsafeCell::new(Default::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
          (M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "new",
              []
            |),
            [
              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_cell_UnsafeCell_T.
  
  Module Impl_core_convert_From_T_for_core_cell_UnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ].
    
    (*
        fn from(t: T) -> UnsafeCell<T> {
            UnsafeCell::new(t)
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ t ] =>
        ltac:(M.monadic
          (let t := M.alloc (| t |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "new",
              []
            |),
            [ M.read (| t |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_T_for_core_cell_UnsafeCell_T.
  
  Module Impl_core_ops_unsize_CoerceUnsized_where_core_ops_unsize_CoerceUnsized_T_U_core_cell_UnsafeCell_U_for_core_cell_UnsafeCell_T.
    Definition Self (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ].
    
    Axiom Implements :
      forall (T U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::CoerceUnsized"
        (Self T U)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_CoerceUnsized_where_core_ops_unsize_CoerceUnsized_T_U_core_cell_UnsafeCell_U_for_core_cell_UnsafeCell_T.
  
  Module Impl_core_ops_unsize_DispatchFromDyn_where_core_ops_unsize_DispatchFromDyn_T_U_core_cell_UnsafeCell_U_for_core_cell_UnsafeCell_T.
    Definition Self (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ].
    
    Axiom Implements :
      forall (T U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::DispatchFromDyn"
        (Self T U)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_DispatchFromDyn_where_core_ops_unsize_DispatchFromDyn_T_U_core_cell_UnsafeCell_U_for_core_cell_UnsafeCell_T.
  
  (* StructRecord
    {
      name := "SyncUnsafeCell";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ ("value", Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ]) ];
    } *)
  
  Module Impl_core_marker_Sync_where_core_marker_Sized_T_where_core_marker_Sync_T_for_core_cell_SyncUnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Sync"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Sync_where_core_marker_Sized_T_where_core_marker_Sync_T_for_core_cell_SyncUnsafeCell_T.
  
  Module Impl_core_cell_SyncUnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ T ].
    
    (*
        pub const fn new(value: T) -> Self {
            Self { value: UnsafeCell { value } }
        }
    *)
    Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          Value.StructRecord
            "core::cell::SyncUnsafeCell"
            [
              ("value",
                Value.StructRecord "core::cell::UnsafeCell" [ ("value", M.read (| value |)) ])
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "new" (new T).
    
    (*
        pub const fn into_inner(self) -> T {
            self.value.into_inner()
        }
    *)
    Definition into_inner (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_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "into_inner",
              []
            |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  self,
                  "core::cell::SyncUnsafeCell",
                  "value"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_inner :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "into_inner" (into_inner T).
    (*
        pub const fn get(&self) -> *mut T {
            self.value.get()
        }
    *)
    Definition get (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_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "get",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::cell::SyncUnsafeCell",
                "value"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "get" (get T).
    
    (*
        pub const fn get_mut(&mut self) -> &mut T {
            self.value.get_mut()
        }
    *)
    Definition get_mut (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_associated_function (|
              Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ],
              "get_mut",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::cell::SyncUnsafeCell",
                "value"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "get_mut" (get_mut T).
    
    (*
        pub const fn raw_get(this: *const Self) -> *mut T {
            // We can just cast the pointer from `SyncUnsafeCell<T>` to `T` because
            // of #[repr(transparent)] on both SyncUnsafeCell and UnsafeCell.
            // See UnsafeCell::raw_get.
            this as *const T as *mut T
        }
    *)
    Definition raw_get (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ this ] =>
        ltac:(M.monadic
          (let this := M.alloc (| this |) in
          M.rust_cast (M.rust_cast (M.read (| this |)))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_raw_get :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "raw_get" (raw_get T).
  End Impl_core_cell_SyncUnsafeCell_T.
  
  
  Module Impl_core_default_Default_where_core_default_Default_T_for_core_cell_SyncUnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ T ].
    
    (*
        fn default() -> SyncUnsafeCell<T> {
            SyncUnsafeCell::new(Default::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
          (M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ T ],
              "new",
              []
            |),
            [
              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_cell_SyncUnsafeCell_T.
  
  Module Impl_core_convert_From_T_for_core_cell_SyncUnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ T ].
    
    (*
        fn from(t: T) -> SyncUnsafeCell<T> {
            SyncUnsafeCell::new(t)
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ t ] =>
        ltac:(M.monadic
          (let t := M.alloc (| t |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ T ],
              "new",
              []
            |),
            [ M.read (| t |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_T_for_core_cell_SyncUnsafeCell_T.
  
  Module Impl_core_ops_unsize_CoerceUnsized_where_core_ops_unsize_CoerceUnsized_T_U_core_cell_SyncUnsafeCell_U_for_core_cell_SyncUnsafeCell_T.
    Definition Self (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ T ].
    
    Axiom Implements :
      forall (T U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::CoerceUnsized"
        (Self T U)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_CoerceUnsized_where_core_ops_unsize_CoerceUnsized_T_U_core_cell_SyncUnsafeCell_U_for_core_cell_SyncUnsafeCell_T.
  
  Module Impl_core_ops_unsize_DispatchFromDyn_where_core_ops_unsize_DispatchFromDyn_T_U_core_cell_SyncUnsafeCell_U_for_core_cell_SyncUnsafeCell_T.
    Definition Self (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ T ].
    
    Axiom Implements :
      forall (T U : Ty.t),
      M.IsTraitInstance
        "core::ops::unsize::DispatchFromDyn"
        (Self T U)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ U ] ]
        (* Instance *) [].
  End Impl_core_ops_unsize_DispatchFromDyn_where_core_ops_unsize_DispatchFromDyn_T_U_core_cell_SyncUnsafeCell_U_for_core_cell_SyncUnsafeCell_T.
  
  (*
  fn assert_coerce_unsized(
      a: UnsafeCell<&i32>,
      b: SyncUnsafeCell<&i32>,
      c: Cell<&i32>,
      d: RefCell<&i32>,
  ) {
      let _: UnsafeCell<&dyn Send> = a;
      let _: SyncUnsafeCell<&dyn Send> = b;
      let _: Cell<&dyn Send> = c;
      let _: RefCell<&dyn Send> = d;
  }
  *)
  Definition assert_coerce_unsized (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ a; b; c; d ] =>
      ltac:(M.monadic
        (let a := M.alloc (| a |) in
        let b := M.alloc (| b |) in
        let c := M.alloc (| c |) in
        let d := M.alloc (| d |) in
        M.read (|
          M.match_operator (|
            M.alloc (| M.read (| a |) |),
            [
              fun γ =>
                ltac:(M.monadic
                  (M.match_operator (|
                    M.alloc (| M.read (| b |) |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| M.read (| c |) |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| M.read (| d |) |),
                                    [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                                  |)))
                            ]
                          |)))
                    ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_assert_coerce_unsized :
    M.IsFunction "core::cell::assert_coerce_unsized" assert_coerce_unsized.
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_UnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::UnsafeCell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_UnsafeCell_T.
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_SyncUnsafeCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::SyncUnsafeCell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_SyncUnsafeCell_T.
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_Cell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Cell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_Cell_T.
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_RefCell_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefCell") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_RefCell_T.
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_Ref_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::Ref") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_Ref_T.
  
  Module Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_RefMut_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::cell::RefMut") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::pin::PinCoerceUnsized"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_pin_PinCoerceUnsized_where_core_marker_Sized_T_for_core_cell_RefMut_T.
End cell.
