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

Module collections.
  Module btree.
    Module map.
      Module entry.
        (*
        Enum Entry
        {
          const_params := [];
          ty_params := [ "K"; "V"; "A" ];
          variants :=
            [
              {
                name := "Vacant";
                item :=
                  StructTuple
                    [
                      Ty.apply
                        (Ty.path "alloc::collections::btree::map::entry::VacantEntry")
                        []
                        [ K; V; A ]
                    ];
                discriminant := None;
              };
              {
                name := "Occupied";
                item :=
                  StructTuple
                    [
                      Ty.apply
                        (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                        []
                        [ K; V; A ]
                    ];
                discriminant := None;
              }
            ];
        }
        *)
        
        Module Impl_core_fmt_Debug_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_Entry_K_V_A.
          Definition Self (K V A : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "alloc::collections::btree::map::entry::Entry") [] [ K; V; A ].
          
          (*
              fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                  match *self {
                      Vacant(ref v) => f.debug_tuple("Entry").field(v).finish(),
                      Occupied(ref o) => f.debug_tuple("Entry").field(o).finish(),
                  }
              }
          *)
          Definition fmt (K V A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self; f ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let f := M.alloc (| f |) in
                M.read (|
                  M.match_operator (|
                    M.read (| self |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Vacant",
                              0
                            |) in
                          let v := M.alloc (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::builders::DebugTuple",
                                "finish",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::builders::DebugTuple",
                                    "field",
                                    []
                                  |),
                                  [
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::Formatter",
                                          "debug_tuple",
                                          []
                                        |),
                                        [ M.read (| f |); M.read (| Value.String "Entry" |) ]
                                      |)
                                    |);
                                    M.read (| v |)
                                  ]
                                |)
                              ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Occupied",
                              0
                            |) in
                          let o := M.alloc (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::builders::DebugTuple",
                                "finish",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::builders::DebugTuple",
                                    "field",
                                    []
                                  |),
                                  [
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::Formatter",
                                          "debug_tuple",
                                          []
                                        |),
                                        [ M.read (| f |); M.read (| Value.String "Entry" |) ]
                                      |)
                                    |);
                                    M.read (| o |)
                                  ]
                                |)
                              ]
                            |)
                          |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (K V A : Ty.t),
            M.IsTraitInstance
              "core::fmt::Debug"
              (Self K V A)
              (* Trait polymorphic types *) []
              (* Instance *) [ ("fmt", InstanceField.Method (fmt K V A)) ].
        End Impl_core_fmt_Debug_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_Entry_K_V_A.
        
        (* StructRecord
          {
            name := "VacantEntry";
            const_params := [];
            ty_params := [ "K"; "V"; "A" ];
            fields :=
              [
                ("key", K);
                ("handle",
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloc::collections::btree::node::Handle")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloc::collections::btree::node::NodeRef")
                            []
                            [
                              Ty.path "alloc::collections::btree::node::marker::Mut";
                              K;
                              V;
                              Ty.path "alloc::collections::btree::node::marker::Leaf"
                            ];
                          Ty.path "alloc::collections::btree::node::marker::Edge"
                        ]
                    ]);
                ("dormant_map",
                  Ty.apply
                    (Ty.path "alloc::collections::btree::borrow::DormantMutRef")
                    []
                    [ Ty.apply (Ty.path "alloc::collections::btree::map::BTreeMap") [] [ K; V; A ]
                    ]);
                ("alloc", A);
                ("_marker",
                  Ty.apply
                    (Ty.path "core::marker::PhantomData")
                    []
                    [ Ty.apply (Ty.path "&mut") [] [ Ty.tuple [ K; V ] ] ])
              ];
          } *)
        
        Module Impl_core_fmt_Debug_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_VacantEntry_K_V_A.
          Definition Self (K V A : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "alloc::collections::btree::map::entry::VacantEntry") [] [ K; V; A ].
          
          (*
              fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                  f.debug_tuple("VacantEntry").field(self.key()).finish()
              }
          *)
          Definition fmt (K V A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self; f ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let f := M.alloc (| f |) in
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugTuple",
                    "finish",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::builders::DebugTuple",
                        "field",
                        []
                      |),
                      [
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "debug_tuple",
                              []
                            |),
                            [ M.read (| f |); M.read (| Value.String "VacantEntry" |) ]
                          |)
                        |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::btree::map::entry::VacantEntry")
                              []
                              [ K; V; A ],
                            "key",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      ]
                    |)
                  ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (K V A : Ty.t),
            M.IsTraitInstance
              "core::fmt::Debug"
              (Self K V A)
              (* Trait polymorphic types *) []
              (* Instance *) [ ("fmt", InstanceField.Method (fmt K V A)) ].
        End Impl_core_fmt_Debug_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_VacantEntry_K_V_A.
        
        (* StructRecord
          {
            name := "OccupiedEntry";
            const_params := [];
            ty_params := [ "K"; "V"; "A" ];
            fields :=
              [
                ("handle",
                  Ty.apply
                    (Ty.path "alloc::collections::btree::node::Handle")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloc::collections::btree::node::NodeRef")
                        []
                        [
                          Ty.path "alloc::collections::btree::node::marker::Mut";
                          K;
                          V;
                          Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                        ];
                      Ty.path "alloc::collections::btree::node::marker::KV"
                    ]);
                ("dormant_map",
                  Ty.apply
                    (Ty.path "alloc::collections::btree::borrow::DormantMutRef")
                    []
                    [ Ty.apply (Ty.path "alloc::collections::btree::map::BTreeMap") [] [ K; V; A ]
                    ]);
                ("alloc", A);
                ("_marker",
                  Ty.apply
                    (Ty.path "core::marker::PhantomData")
                    []
                    [ Ty.apply (Ty.path "&mut") [] [ Ty.tuple [ K; V ] ] ])
              ];
          } *)
        
        Module Impl_core_fmt_Debug_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_OccupiedEntry_K_V_A.
          Definition Self (K V A : Ty.t) : Ty.t :=
            Ty.apply
              (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
              []
              [ K; V; A ].
          
          (*
              fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                  f.debug_struct("OccupiedEntry").field("key", self.key()).field("value", self.get()).finish()
              }
          *)
          Definition fmt (K V A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self; f ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let f := M.alloc (| f |) in
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugStruct",
                    "finish",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::builders::DebugStruct",
                        "field",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::builders::DebugStruct",
                            "field",
                            []
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Formatter",
                                  "debug_struct",
                                  []
                                |),
                                [ M.read (| f |); M.read (| Value.String "OccupiedEntry" |) ]
                              |)
                            |);
                            M.read (| Value.String "key" |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                                  []
                                  [ K; V; A ],
                                "key",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                        |);
                        M.read (| Value.String "value" |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                              []
                              [ K; V; A ],
                            "get",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      ]
                    |)
                  ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (K V A : Ty.t),
            M.IsTraitInstance
              "core::fmt::Debug"
              (Self K V A)
              (* Trait polymorphic types *) []
              (* Instance *) [ ("fmt", InstanceField.Method (fmt K V A)) ].
        End Impl_core_fmt_Debug_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_OccupiedEntry_K_V_A.
        
        (* StructRecord
          {
            name := "OccupiedError";
            const_params := [];
            ty_params := [ "K"; "V"; "A" ];
            fields :=
              [
                ("entry",
                  Ty.apply
                    (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                    []
                    [ K; V; A ]);
                ("value", V)
              ];
          } *)
        
        Module Impl_core_fmt_Debug_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_OccupiedError_K_V_A.
          Definition Self (K V A : Ty.t) : Ty.t :=
            Ty.apply
              (Ty.path "alloc::collections::btree::map::entry::OccupiedError")
              []
              [ K; V; A ].
          
          (*
              fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                  f.debug_struct("OccupiedError")
                      .field("key", self.entry.key())
                      .field("old_value", self.entry.get())
                      .field("new_value", &self.value)
                      .finish()
              }
          *)
          Definition fmt (K V A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self; f ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let f := M.alloc (| f |) in
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::fmt::builders::DebugStruct",
                    "finish",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::builders::DebugStruct",
                        "field",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::builders::DebugStruct",
                            "field",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::builders::DebugStruct",
                                "field",
                                []
                              |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::Formatter",
                                      "debug_struct",
                                      []
                                    |),
                                    [ M.read (| f |); M.read (| Value.String "OccupiedError" |) ]
                                  |)
                                |);
                                M.read (| Value.String "key" |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path
                                        "alloc::collections::btree::map::entry::OccupiedEntry")
                                      []
                                      [ K; V; A ],
                                    "key",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "alloc::collections::btree::map::entry::OccupiedError",
                                      "entry"
                                    |)
                                  ]
                                |)
                              ]
                            |);
                            M.read (| Value.String "old_value" |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                                  []
                                  [ K; V; A ],
                                "get",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "alloc::collections::btree::map::entry::OccupiedError",
                                  "entry"
                                |)
                              ]
                            |)
                          ]
                        |);
                        M.read (| Value.String "new_value" |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "alloc::collections::btree::map::entry::OccupiedError",
                          "value"
                        |)
                      ]
                    |)
                  ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (K V A : Ty.t),
            M.IsTraitInstance
              "core::fmt::Debug"
              (Self K V A)
              (* Trait polymorphic types *) []
              (* Instance *) [ ("fmt", InstanceField.Method (fmt K V A)) ].
        End Impl_core_fmt_Debug_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_OccupiedError_K_V_A.
        
        Module Impl_core_fmt_Display_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_OccupiedError_K_V_A.
          Definition Self (K V A : Ty.t) : Ty.t :=
            Ty.apply
              (Ty.path "alloc::collections::btree::map::entry::OccupiedError")
              []
              [ K; V; A ].
          
          (*
              fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
                  write!(
                      f,
                      "failed to insert {:?}, key {:?} already exists with value {:?}",
                      self.value,
                      self.entry.key(),
                      self.entry.get(),
                  )
              }
          *)
          Definition fmt (K V A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self; f ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let f := M.alloc (| f |) in
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_fmt", [] |),
                  [
                    M.read (| f |);
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                      [
                        M.alloc (|
                          Value.Array
                            [
                              M.read (| Value.String "failed to insert " |);
                              M.read (| Value.String ", key " |);
                              M.read (| Value.String " already exists with value " |)
                            ]
                        |);
                        M.alloc (|
                          Value.Array
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Argument",
                                  "new_debug",
                                  [ V ]
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "alloc::collections::btree::map::entry::OccupiedError",
                                    "value"
                                  |)
                                ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Argument",
                                  "new_debug",
                                  [ Ty.apply (Ty.path "&") [] [ K ] ]
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path
                                            "alloc::collections::btree::map::entry::OccupiedEntry")
                                          []
                                          [ K; V; A ],
                                        "key",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "alloc::collections::btree::map::entry::OccupiedError",
                                          "entry"
                                        |)
                                      ]
                                    |)
                                  |)
                                ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::Argument",
                                  "new_debug",
                                  [ Ty.apply (Ty.path "&") [] [ V ] ]
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path
                                            "alloc::collections::btree::map::entry::OccupiedEntry")
                                          []
                                          [ K; V; A ],
                                        "get",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "alloc::collections::btree::map::entry::OccupiedError",
                                          "entry"
                                        |)
                                      ]
                                    |)
                                  |)
                                ]
                              |)
                            ]
                        |)
                      ]
                    |)
                  ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (K V A : Ty.t),
            M.IsTraitInstance
              "core::fmt::Display"
              (Self K V A)
              (* Trait polymorphic types *) []
              (* Instance *) [ ("fmt", InstanceField.Method (fmt K V A)) ].
        End Impl_core_fmt_Display_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_OccupiedError_K_V_A.
        
        Module Impl_core_error_Error_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_for_alloc_collections_btree_map_entry_OccupiedError_K_V_alloc_alloc_Global.
          Definition Self (K V : Ty.t) : Ty.t :=
            Ty.apply
              (Ty.path "alloc::collections::btree::map::entry::OccupiedError")
              []
              [ K; V; Ty.path "alloc::alloc::Global" ].
          
          (*
              fn description(&self) -> &str {
                  "key already exists"
              }
          *)
          Definition description
              (K V : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (| Value.String "key already exists" |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (K V : Ty.t),
            M.IsTraitInstance
              "core::error::Error"
              (Self K V)
              (* Trait polymorphic types *) []
              (* Instance *) [ ("description", InstanceField.Method (description K V)) ].
        End Impl_core_error_Error_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_for_alloc_collections_btree_map_entry_OccupiedError_K_V_alloc_alloc_Global.
        
        Module Impl_alloc_collections_btree_map_entry_Entry_K_V_A.
          Definition Self (K V A : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "alloc::collections::btree::map::entry::Entry") [] [ K; V; A ].
          
          (*
              pub fn or_insert(self, default: V) -> &'a mut V {
                  match self {
                      Occupied(entry) => entry.into_mut(),
                      Vacant(entry) => entry.insert(default),
                  }
              }
          *)
          Definition or_insert
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self; default ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let default := M.alloc (| default |) in
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Occupied",
                              0
                            |) in
                          let entry := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                                  []
                                  [ K; V; A ],
                                "into_mut",
                                []
                              |),
                              [ M.read (| entry |) ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Vacant",
                              0
                            |) in
                          let entry := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::VacantEntry")
                                  []
                                  [ K; V; A ],
                                "insert",
                                []
                              |),
                              [ M.read (| entry |); M.read (| default |) ]
                            |)
                          |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_or_insert :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "or_insert" (or_insert K V A).
          
          (*
              pub fn or_insert_with<F: FnOnce() -> V>(self, default: F) -> &'a mut V {
                  match self {
                      Occupied(entry) => entry.into_mut(),
                      Vacant(entry) => entry.insert(default()),
                  }
              }
          *)
          Definition or_insert_with
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [ F ], [ self; default ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let default := M.alloc (| default |) in
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Occupied",
                              0
                            |) in
                          let entry := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                                  []
                                  [ K; V; A ],
                                "into_mut",
                                []
                              |),
                              [ M.read (| entry |) ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Vacant",
                              0
                            |) in
                          let entry := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::VacantEntry")
                                  []
                                  [ K; V; A ],
                                "insert",
                                []
                              |),
                              [
                                M.read (| entry |);
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::function::FnOnce",
                                    F,
                                    [ Ty.tuple [] ],
                                    "call_once",
                                    []
                                  |),
                                  [ M.read (| default |); Value.Tuple [] ]
                                |)
                              ]
                            |)
                          |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_or_insert_with :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "or_insert_with" (or_insert_with K V A).
          
          (*
              pub fn or_insert_with_key<F: FnOnce(&K) -> V>(self, default: F) -> &'a mut V {
                  match self {
                      Occupied(entry) => entry.into_mut(),
                      Vacant(entry) => {
                          let value = default(entry.key());
                          entry.insert(value)
                      }
                  }
              }
          *)
          Definition or_insert_with_key
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [ F ], [ self; default ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let default := M.alloc (| default |) in
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Occupied",
                              0
                            |) in
                          let entry := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                                  []
                                  [ K; V; A ],
                                "into_mut",
                                []
                              |),
                              [ M.read (| entry |) ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Vacant",
                              0
                            |) in
                          let entry := M.copy (| γ0_0 |) in
                          let~ value :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::function::FnOnce",
                                  F,
                                  [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ K ] ] ],
                                  "call_once",
                                  []
                                |),
                                [
                                  M.read (| default |);
                                  Value.Tuple
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path
                                              "alloc::collections::btree::map::entry::VacantEntry")
                                            []
                                            [ K; V; A ],
                                          "key",
                                          []
                                        |),
                                        [ entry ]
                                      |)
                                    ]
                                ]
                              |)
                            |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::VacantEntry")
                                  []
                                  [ K; V; A ],
                                "insert",
                                []
                              |),
                              [ M.read (| entry |); M.read (| value |) ]
                            |)
                          |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_or_insert_with_key :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "or_insert_with_key" (or_insert_with_key K V A).
          
          (*
              pub fn key(&self) -> &K {
                  match *self {
                      Occupied(ref entry) => entry.key(),
                      Vacant(ref entry) => entry.key(),
                  }
              }
          *)
          Definition key (K V A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (|
                  M.match_operator (|
                    M.read (| self |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Occupied",
                              0
                            |) in
                          let entry := M.alloc (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                                  []
                                  [ K; V; A ],
                                "key",
                                []
                              |),
                              [ M.read (| entry |) ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Vacant",
                              0
                            |) in
                          let entry := M.alloc (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::VacantEntry")
                                  []
                                  [ K; V; A ],
                                "key",
                                []
                              |),
                              [ M.read (| entry |) ]
                            |)
                          |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_key :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "key" (key K V A).
          
          (*
              pub fn and_modify<F>(self, f: F) -> Self
              where
                  F: FnOnce(&mut V),
              {
                  match self {
                      Occupied(mut entry) => {
                          f(entry.get_mut());
                          Occupied(entry)
                      }
                      Vacant(entry) => Vacant(entry),
                  }
              }
          *)
          Definition and_modify
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [ F ], [ self; f ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let f := M.alloc (| f |) in
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Occupied",
                              0
                            |) in
                          let entry := M.copy (| γ0_0 |) in
                          let~ _ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::function::FnOnce",
                                  F,
                                  [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ V ] ] ],
                                  "call_once",
                                  []
                                |),
                                [
                                  M.read (| f |);
                                  Value.Tuple
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path
                                              "alloc::collections::btree::map::entry::OccupiedEntry")
                                            []
                                            [ K; V; A ],
                                          "get_mut",
                                          []
                                        |),
                                        [ entry ]
                                      |)
                                    ]
                                ]
                              |)
                            |) in
                          M.alloc (|
                            Value.StructTuple
                              "alloc::collections::btree::map::entry::Entry::Occupied"
                              [ M.read (| entry |) ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Vacant",
                              0
                            |) in
                          let entry := M.copy (| γ0_0 |) in
                          M.alloc (|
                            Value.StructTuple
                              "alloc::collections::btree::map::entry::Entry::Vacant"
                              [ M.read (| entry |) ]
                          |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_and_modify :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "and_modify" (and_modify K V A).
          (*
              pub fn or_default(self) -> &'a mut V {
                  match self {
                      Occupied(entry) => entry.into_mut(),
                      Vacant(entry) => entry.insert(Default::default()),
                  }
              }
          *)
          Definition or_default
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Occupied",
                              0
                            |) in
                          let entry := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                                  []
                                  [ K; V; A ],
                                "into_mut",
                                []
                              |),
                              [ M.read (| entry |) ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "alloc::collections::btree::map::entry::Entry::Vacant",
                              0
                            |) in
                          let entry := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::entry::VacantEntry")
                                  []
                                  [ K; V; A ],
                                "insert",
                                []
                              |),
                              [
                                M.read (| entry |);
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::default::Default",
                                    V,
                                    [],
                                    "default",
                                    []
                                  |),
                                  []
                                |)
                              ]
                            |)
                          |)))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_or_default :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "or_default" (or_default K V A).
        End Impl_alloc_collections_btree_map_entry_Entry_K_V_A.
        
        
        Module Impl_alloc_collections_btree_map_entry_VacantEntry_K_V_A.
          Definition Self (K V A : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "alloc::collections::btree::map::entry::VacantEntry") [] [ K; V; A ].
          
          (*
              pub fn key(&self) -> &K {
                  &self.key
              }
          *)
          Definition key (K V A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "alloc::collections::btree::map::entry::VacantEntry",
                  "key"
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_key :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "key" (key K V A).
          
          (*
              pub fn into_key(self) -> K {
                  self.key
              }
          *)
          Definition into_key
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "alloc::collections::btree::map::entry::VacantEntry",
                    "key"
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_into_key :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "into_key" (into_key K V A).
          
          (*
              pub fn insert(mut self, value: V) -> &'a mut V {
                  let out_ptr = match self.handle {
                      None => {
                          // SAFETY: There is no tree yet so no reference to it exists.
                          let map = unsafe { self.dormant_map.awaken() };
                          let mut root = NodeRef::new_leaf(self.alloc.clone());
                          let val_ptr = root.borrow_mut().push(self.key, value);
                          map.root = Some(root.forget_type());
                          map.length = 1;
                          val_ptr
                      }
                      Some(handle) => {
                          let new_handle =
                              handle.insert_recursing(self.key, value, self.alloc.clone(), |ins| {
                                  drop(ins.left);
                                  // SAFETY: Pushing a new root node doesn't invalidate
                                  // handles to existing nodes.
                                  let map = unsafe { self.dormant_map.reborrow() };
                                  let root = map.root.as_mut().unwrap(); // same as ins.left
                                  root.push_internal_level(self.alloc).push(ins.kv.0, ins.kv.1, ins.right)
                              });
          
                          // Get the pointer to the value
                          let val_ptr = new_handle.into_val_mut();
          
                          // SAFETY: We have consumed self.handle.
                          let map = unsafe { self.dormant_map.awaken() };
                          map.length += 1;
                          val_ptr
                      }
                  };
          
                  // Now that we have finished growing the tree using borrowed references,
                  // dereference the pointer to a part of it, that we picked up along the way.
                  unsafe { &mut *out_ptr }
              }
          *)
          Definition insert
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self; value ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let value := M.alloc (| value |) in
                M.read (|
                  let~ out_ptr :=
                    M.copy (|
                      M.match_operator (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "alloc::collections::btree::map::entry::VacantEntry",
                          "handle"
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                              let~ map :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::collections::btree::borrow::DormantMutRef")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "alloc::collections::btree::map::BTreeMap")
                                            []
                                            [ K; V; A ]
                                        ],
                                      "awaken",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "alloc::collections::btree::map::entry::VacantEntry",
                                          "dormant_map"
                                        |)
                                      |)
                                    ]
                                  |)
                                |) in
                              let~ root :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::collections::btree::node::NodeRef")
                                        []
                                        [
                                          Ty.path "alloc::collections::btree::node::marker::Owned";
                                          K;
                                          V;
                                          Ty.path "alloc::collections::btree::node::marker::Leaf"
                                        ],
                                      "new_leaf",
                                      [ A ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::clone::Clone",
                                          A,
                                          [],
                                          "clone",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            self,
                                            "alloc::collections::btree::map::entry::VacantEntry",
                                            "alloc"
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |) in
                              let~ val_ptr :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::collections::btree::node::NodeRef")
                                        []
                                        [
                                          Ty.path "alloc::collections::btree::node::marker::Mut";
                                          K;
                                          V;
                                          Ty.path "alloc::collections::btree::node::marker::Leaf"
                                        ],
                                      "push",
                                      []
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "alloc::collections::btree::node::NodeRef")
                                              []
                                              [
                                                Ty.path
                                                  "alloc::collections::btree::node::marker::Owned";
                                                K;
                                                V;
                                                Ty.path
                                                  "alloc::collections::btree::node::marker::Leaf"
                                              ],
                                            "borrow_mut",
                                            []
                                          |),
                                          [ root ]
                                        |)
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "alloc::collections::btree::map::entry::VacantEntry",
                                          "key"
                                        |)
                                      |);
                                      M.read (| value |)
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                M.write (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| map |),
                                    "alloc::collections::btree::map::BTreeMap",
                                    "root"
                                  |),
                                  Value.StructTuple
                                    "core::option::Option::Some"
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::collections::btree::node::NodeRef")
                                            []
                                            [
                                              Ty.path
                                                "alloc::collections::btree::node::marker::Owned";
                                              K;
                                              V;
                                              Ty.path
                                                "alloc::collections::btree::node::marker::Leaf"
                                            ],
                                          "forget_type",
                                          []
                                        |),
                                        [ M.read (| root |) ]
                                      |)
                                    ]
                                |) in
                              let~ _ :=
                                M.write (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| map |),
                                    "alloc::collections::btree::map::BTreeMap",
                                    "length"
                                  |),
                                  Value.Integer IntegerKind.Usize 1
                                |) in
                              val_ptr));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let handle := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.read (|
                                  let~ new_handle :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::collections::btree::node::Handle")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "alloc::collections::btree::node::NodeRef")
                                                []
                                                [
                                                  Ty.path
                                                    "alloc::collections::btree::node::marker::Mut";
                                                  K;
                                                  V;
                                                  Ty.path
                                                    "alloc::collections::btree::node::marker::Leaf"
                                                ];
                                              Ty.path
                                                "alloc::collections::btree::node::marker::Edge"
                                            ],
                                          "insert_recursing",
                                          [
                                            A;
                                            Ty.function
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.apply
                                                      (Ty.path
                                                        "alloc::collections::btree::node::SplitResult")
                                                      []
                                                      [
                                                        K;
                                                        V;
                                                        Ty.path
                                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                                      ]
                                                  ]
                                              ]
                                              (Ty.tuple [])
                                          ]
                                        |),
                                        [
                                          M.read (| handle |);
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              self,
                                              "alloc::collections::btree::map::entry::VacantEntry",
                                              "key"
                                            |)
                                          |);
                                          M.read (| value |);
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::clone::Clone",
                                              A,
                                              [],
                                              "clone",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "alloc::collections::btree::map::entry::VacantEntry",
                                                "alloc"
                                              |)
                                            ]
                                          |);
                                          M.closure
                                            (fun γ =>
                                              ltac:(M.monadic
                                                match γ with
                                                | [ α0 ] =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      M.alloc (| α0 |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let ins := M.copy (| γ |) in
                                                            M.read (|
                                                              let~ _ :=
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_function (|
                                                                      "core::mem::drop",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::collections::btree::node::NodeRef")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "alloc::collections::btree::node::marker::Mut";
                                                                            K;
                                                                            V;
                                                                            Ty.path
                                                                              "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                          ]
                                                                      ]
                                                                    |),
                                                                    [
                                                                      M.read (|
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          ins,
                                                                          "alloc::collections::btree::node::SplitResult",
                                                                          "left"
                                                                        |)
                                                                      |)
                                                                    ]
                                                                  |)
                                                                |) in
                                                              let~ map :=
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "alloc::collections::btree::borrow::DormantMutRef")
                                                                        []
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "alloc::collections::btree::map::BTreeMap")
                                                                            []
                                                                            [ K; V; A ]
                                                                        ],
                                                                      "reborrow",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        self,
                                                                        "alloc::collections::btree::map::entry::VacantEntry",
                                                                        "dormant_map"
                                                                      |)
                                                                    ]
                                                                  |)
                                                                |) in
                                                              let~ root :=
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::option::Option")
                                                                        []
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "&mut")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "alloc::collections::btree::node::NodeRef")
                                                                                []
                                                                                [
                                                                                  Ty.path
                                                                                    "alloc::collections::btree::node::marker::Owned";
                                                                                  K;
                                                                                  V;
                                                                                  Ty.path
                                                                                    "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                                ]
                                                                            ]
                                                                        ],
                                                                      "unwrap",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "core::option::Option")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "alloc::collections::btree::node::NodeRef")
                                                                                []
                                                                                [
                                                                                  Ty.path
                                                                                    "alloc::collections::btree::node::marker::Owned";
                                                                                  K;
                                                                                  V;
                                                                                  Ty.path
                                                                                    "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                                ]
                                                                            ],
                                                                          "as_mut",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.SubPointer.get_struct_record_field (|
                                                                            M.read (| map |),
                                                                            "alloc::collections::btree::map::BTreeMap",
                                                                            "root"
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    ]
                                                                  |)
                                                                |) in
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "alloc::collections::btree::node::NodeRef")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "alloc::collections::btree::node::marker::Mut";
                                                                        K;
                                                                        V;
                                                                        Ty.path
                                                                          "alloc::collections::btree::node::marker::Internal"
                                                                      ],
                                                                    "push",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "alloc::collections::btree::node::NodeRef")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "alloc::collections::btree::node::marker::Owned";
                                                                              K;
                                                                              V;
                                                                              Ty.path
                                                                                "alloc::collections::btree::node::marker::LeafOrInternal"
                                                                            ],
                                                                          "push_internal_level",
                                                                          [ A ]
                                                                        |),
                                                                        [
                                                                          M.read (| root |);
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              self,
                                                                              "alloc::collections::btree::map::entry::VacantEntry",
                                                                              "alloc"
                                                                            |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |);
                                                                    M.read (|
                                                                      M.SubPointer.get_tuple_field (|
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          ins,
                                                                          "alloc::collections::btree::node::SplitResult",
                                                                          "kv"
                                                                        |),
                                                                        0
                                                                      |)
                                                                    |);
                                                                    M.read (|
                                                                      M.SubPointer.get_tuple_field (|
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          ins,
                                                                          "alloc::collections::btree::node::SplitResult",
                                                                          "kv"
                                                                        |),
                                                                        1
                                                                      |)
                                                                    |);
                                                                    M.read (|
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        ins,
                                                                        "alloc::collections::btree::node::SplitResult",
                                                                        "right"
                                                                      |)
                                                                    |)
                                                                  ]
                                                                |)
                                                              |)
                                                            |)))
                                                      ]
                                                    |)))
                                                | _ => M.impossible "wrong number of arguments"
                                                end))
                                        ]
                                      |)
                                    |) in
                                  let~ val_ptr :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::collections::btree::node::Handle")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "alloc::collections::btree::node::NodeRef")
                                                []
                                                [
                                                  Ty.path
                                                    "alloc::collections::btree::node::marker::Mut";
                                                  K;
                                                  V;
                                                  Ty.path
                                                    "alloc::collections::btree::node::marker::Leaf"
                                                ];
                                              Ty.path "alloc::collections::btree::node::marker::KV"
                                            ],
                                          "into_val_mut",
                                          []
                                        |),
                                        [ M.read (| new_handle |) ]
                                      |)
                                    |) in
                                  let~ map :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path
                                              "alloc::collections::btree::borrow::DormantMutRef")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "alloc::collections::btree::map::BTreeMap")
                                                []
                                                [ K; V; A ]
                                            ],
                                          "awaken",
                                          []
                                        |),
                                        [
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              self,
                                              "alloc::collections::btree::map::entry::VacantEntry",
                                              "dormant_map"
                                            |)
                                          |)
                                        ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    let β :=
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| map |),
                                        "alloc::collections::btree::map::BTreeMap",
                                        "length"
                                      |) in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.add (|
                                        M.read (| β |),
                                        Value.Integer IntegerKind.Usize 1
                                      |)
                                    |) in
                                  val_ptr
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  M.alloc (| M.read (| out_ptr |) |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_insert :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "insert" (insert K V A).
        End Impl_alloc_collections_btree_map_entry_VacantEntry_K_V_A.
        
        Module Impl_alloc_collections_btree_map_entry_OccupiedEntry_K_V_A.
          Definition Self (K V A : Ty.t) : Ty.t :=
            Ty.apply
              (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
              []
              [ K; V; A ].
          
          (*
              pub fn key(&self) -> &K {
                  self.handle.reborrow().into_kv().0
              }
          *)
          Definition key (K V A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (|
                  M.SubPointer.get_tuple_field (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::collections::btree::node::Handle")
                            []
                            [
                              Ty.apply
                                (Ty.path "alloc::collections::btree::node::NodeRef")
                                []
                                [
                                  Ty.path "alloc::collections::btree::node::marker::Immut";
                                  K;
                                  V;
                                  Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                                ];
                              Ty.path "alloc::collections::btree::node::marker::KV"
                            ],
                          "into_kv",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::btree::node::Handle")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::node::NodeRef")
                                    []
                                    [
                                      Ty.path "alloc::collections::btree::node::marker::Mut";
                                      K;
                                      V;
                                      Ty.path
                                        "alloc::collections::btree::node::marker::LeafOrInternal"
                                    ];
                                  Ty.path "alloc::collections::btree::node::marker::KV"
                                ],
                              "reborrow",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::btree::map::entry::OccupiedEntry",
                                "handle"
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    0
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_key :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "key" (key K V A).
          
          (*
              pub fn remove_entry(self) -> (K, V) {
                  self.remove_kv()
              }
          *)
          Definition remove_entry
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                      []
                      [ K; V; A ],
                    "remove_kv",
                    []
                  |),
                  [ M.read (| self |) ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_remove_entry :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "remove_entry" (remove_entry K V A).
          
          (*
              pub fn get(&self) -> &V {
                  self.handle.reborrow().into_kv().1
              }
          *)
          Definition get (K V A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (|
                  M.SubPointer.get_tuple_field (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::collections::btree::node::Handle")
                            []
                            [
                              Ty.apply
                                (Ty.path "alloc::collections::btree::node::NodeRef")
                                []
                                [
                                  Ty.path "alloc::collections::btree::node::marker::Immut";
                                  K;
                                  V;
                                  Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                                ];
                              Ty.path "alloc::collections::btree::node::marker::KV"
                            ],
                          "into_kv",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::btree::node::Handle")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::node::NodeRef")
                                    []
                                    [
                                      Ty.path "alloc::collections::btree::node::marker::Mut";
                                      K;
                                      V;
                                      Ty.path
                                        "alloc::collections::btree::node::marker::LeafOrInternal"
                                    ];
                                  Ty.path "alloc::collections::btree::node::marker::KV"
                                ],
                              "reborrow",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "alloc::collections::btree::map::entry::OccupiedEntry",
                                "handle"
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    1
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_get :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "get" (get K V A).
          
          (*
              pub fn get_mut(&mut self) -> &mut V {
                  self.handle.kv_mut().1
              }
          *)
          Definition get_mut
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (|
                  M.SubPointer.get_tuple_field (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::collections::btree::node::Handle")
                            []
                            [
                              Ty.apply
                                (Ty.path "alloc::collections::btree::node::NodeRef")
                                []
                                [
                                  Ty.path "alloc::collections::btree::node::marker::Mut";
                                  K;
                                  V;
                                  Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                                ];
                              Ty.path "alloc::collections::btree::node::marker::KV"
                            ],
                          "kv_mut",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "alloc::collections::btree::map::entry::OccupiedEntry",
                            "handle"
                          |)
                        ]
                      |)
                    |),
                    1
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_get_mut :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "get_mut" (get_mut K V A).
          
          (*
              pub fn into_mut(self) -> &'a mut V {
                  self.handle.into_val_mut()
              }
          *)
          Definition into_mut
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::node::Handle")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloc::collections::btree::node::NodeRef")
                          []
                          [
                            Ty.path "alloc::collections::btree::node::marker::Mut";
                            K;
                            V;
                            Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                          ];
                        Ty.path "alloc::collections::btree::node::marker::KV"
                      ],
                    "into_val_mut",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "alloc::collections::btree::map::entry::OccupiedEntry",
                        "handle"
                      |)
                    |)
                  ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_into_mut :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "into_mut" (into_mut K V A).
          
          (*
              pub fn insert(&mut self, value: V) -> V {
                  mem::replace(self.get_mut(), value)
              }
          *)
          Definition insert
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self; value ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let value := M.alloc (| value |) in
                M.call_closure (|
                  M.get_function (| "core::mem::replace", [ V ] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                          []
                          [ K; V; A ],
                        "get_mut",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| value |)
                  ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_insert :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "insert" (insert K V A).
          
          (*
              pub fn remove(self) -> V {
                  self.remove_kv().1
              }
          *)
          Definition remove
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (|
                  M.SubPointer.get_tuple_field (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::collections::btree::map::entry::OccupiedEntry")
                            []
                            [ K; V; A ],
                          "remove_kv",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |),
                    1
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_remove :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "remove" (remove K V A).
          
          (*
              pub(super) fn remove_kv(self) -> (K, V) {
                  let mut emptied_internal_root = false;
                  let (old_kv, _) =
                      self.handle.remove_kv_tracking(|| emptied_internal_root = true, self.alloc.clone());
                  // SAFETY: we consumed the intermediate root borrow, `self.handle`.
                  let map = unsafe { self.dormant_map.awaken() };
                  map.length -= 1;
                  if emptied_internal_root {
                      let root = map.root.as_mut().unwrap();
                      root.pop_internal_level(self.alloc);
                  }
                  old_kv
              }
          *)
          Definition remove_kv
              (K V A : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self K V A in
            match ε, τ, α with
            | [], [], [ self ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                M.read (|
                  let~ emptied_internal_root := M.alloc (| Value.Bool false |) in
                  M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::collections::btree::node::Handle")
                            []
                            [
                              Ty.apply
                                (Ty.path "alloc::collections::btree::node::NodeRef")
                                []
                                [
                                  Ty.path "alloc::collections::btree::node::marker::Mut";
                                  K;
                                  V;
                                  Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                                ];
                              Ty.path "alloc::collections::btree::node::marker::KV"
                            ],
                          "remove_kv_tracking",
                          [ Ty.function [ Ty.tuple [] ] (Ty.tuple []); A ]
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "alloc::collections::btree::map::entry::OccupiedEntry",
                              "handle"
                            |)
                          |);
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [ α0 ] =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      M.alloc (| α0 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.read (|
                                              M.write (| emptied_internal_root, Value.Bool true |)
                                            |)))
                                      ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end));
                          M.call_closure (|
                            M.get_trait_method (| "core::clone::Clone", A, [], "clone", [] |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                self,
                                "alloc::collections::btree::map::entry::OccupiedEntry",
                                "alloc"
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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 old_kv := M.copy (| γ0_0 |) in
                          let~ map :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::borrow::DormantMutRef")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::collections::btree::map::BTreeMap")
                                        []
                                        [ K; V; A ]
                                    ],
                                  "awaken",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "alloc::collections::btree::map::entry::OccupiedEntry",
                                      "dormant_map"
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            let β :=
                              M.SubPointer.get_struct_record_field (|
                                M.read (| map |),
                                "alloc::collections::btree::map::BTreeMap",
                                "length"
                              |) in
                            M.write (|
                              β,
                              BinOp.Wrap.sub (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.use emptied_internal_root in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ root :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "&mut")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path
                                                        "alloc::collections::btree::node::NodeRef")
                                                      []
                                                      [
                                                        Ty.path
                                                          "alloc::collections::btree::node::marker::Owned";
                                                        K;
                                                        V;
                                                        Ty.path
                                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                                      ]
                                                  ]
                                              ],
                                            "unwrap",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path
                                                        "alloc::collections::btree::node::NodeRef")
                                                      []
                                                      [
                                                        Ty.path
                                                          "alloc::collections::btree::node::marker::Owned";
                                                        K;
                                                        V;
                                                        Ty.path
                                                          "alloc::collections::btree::node::marker::LeafOrInternal"
                                                      ]
                                                  ],
                                                "as_mut",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| map |),
                                                  "alloc::collections::btree::map::BTreeMap",
                                                  "root"
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "alloc::collections::btree::node::NodeRef")
                                              []
                                              [
                                                Ty.path
                                                  "alloc::collections::btree::node::marker::Owned";
                                                K;
                                                V;
                                                Ty.path
                                                  "alloc::collections::btree::node::marker::LeafOrInternal"
                                              ],
                                            "pop_internal_level",
                                            [ A ]
                                          |),
                                          [
                                            M.read (| root |);
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                self,
                                                "alloc::collections::btree::map::entry::OccupiedEntry",
                                                "alloc"
                                              |)
                                            |)
                                          ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          old_kv))
                    ]
                  |)
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom AssociatedFunction_remove_kv :
            forall (K V A : Ty.t),
            M.IsAssociatedFunction (Self K V A) "remove_kv" (remove_kv K V A).
        End Impl_alloc_collections_btree_map_entry_OccupiedEntry_K_V_A.
      End entry.
    End map.
  End btree.
End collections.
