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

Module collections.
  Module btree.
    Module remove.
      Module Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_LeafOrInternal_alloc_collections_btree_node_marker_KV.
        Definition Self (K V : Ty.t) : Ty.t :=
          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"
            ].
        
        (*
            pub fn remove_kv_tracking<F: FnOnce(), A: Allocator + Clone>(
                self,
                handle_emptied_internal_root: F,
                alloc: A,
            ) -> ((K, V), Handle<NodeRef<marker::Mut<'a>, K, V, marker::Leaf>, marker::Edge>) {
                match self.force() {
                    Leaf(node) => node.remove_leaf_kv(handle_emptied_internal_root, alloc),
                    Internal(node) => node.remove_internal_kv(handle_emptied_internal_root, alloc),
                }
            }
        *)
        Definition remove_kv_tracking
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ F; A ], [ self; handle_emptied_internal_root; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let handle_emptied_internal_root := M.alloc (| handle_emptied_internal_root |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                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"
                          ],
                        "force",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "alloc::collections::btree::node::ForceResult::Leaf",
                            0
                          |) in
                        let node := M.copy (| γ0_0 |) in
                        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"
                                ],
                              "remove_leaf_kv",
                              [ F; A ]
                            |),
                            [
                              M.read (| node |);
                              M.read (| handle_emptied_internal_root |);
                              M.read (| alloc |)
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "alloc::collections::btree::node::ForceResult::Internal",
                            0
                          |) in
                        let node := M.copy (| γ0_0 |) in
                        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::Internal"
                                    ];
                                  Ty.path "alloc::collections::btree::node::marker::KV"
                                ],
                              "remove_internal_kv",
                              [ F; A ]
                            |),
                            [
                              M.read (| node |);
                              M.read (| handle_emptied_internal_root |);
                              M.read (| alloc |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_remove_kv_tracking :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "remove_kv_tracking" (remove_kv_tracking K V).
      End Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_LeafOrInternal_alloc_collections_btree_node_marker_KV.
      
      Module Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_Leaf_alloc_collections_btree_node_marker_KV.
        Definition Self (K V : Ty.t) : Ty.t :=
          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"
            ].
        
        (*
            fn remove_leaf_kv<F: FnOnce(), A: Allocator + Clone>(
                self,
                handle_emptied_internal_root: F,
                alloc: A,
            ) -> ((K, V), Handle<NodeRef<marker::Mut<'a>, K, V, marker::Leaf>, marker::Edge>) {
                let (old_kv, mut pos) = self.remove();
                let len = pos.reborrow().into_node().len();
                if len < MIN_LEN {
                    let idx = pos.idx();
                    // We have to temporarily forget the child type, because there is no
                    // distinct node type for the immediate parents of a leaf.
                    let new_pos = match pos.into_node().forget_type().choose_parent_kv() {
                        Ok(Left(left_parent_kv)) => {
                            debug_assert!(left_parent_kv.right_child_len() == MIN_LEN - 1);
                            if left_parent_kv.can_merge() {
                                left_parent_kv.merge_tracking_child_edge(Right(idx), alloc.clone())
                            } else {
                                debug_assert!(left_parent_kv.left_child_len() > MIN_LEN);
                                left_parent_kv.steal_left(idx)
                            }
                        }
                        Ok(Right(right_parent_kv)) => {
                            debug_assert!(right_parent_kv.left_child_len() == MIN_LEN - 1);
                            if right_parent_kv.can_merge() {
                                right_parent_kv.merge_tracking_child_edge(Left(idx), alloc.clone())
                            } else {
                                debug_assert!(right_parent_kv.right_child_len() > MIN_LEN);
                                right_parent_kv.steal_right(idx)
                            }
                        }
                        Err(pos) => unsafe { Handle::new_edge(pos, idx) },
                    };
                    // SAFETY: `new_pos` is the leaf we started from or a sibling.
                    pos = unsafe { new_pos.cast_to_leaf_unchecked() };
        
                    // Only if we merged, the parent (if any) has shrunk, but skipping
                    // the following step otherwise does not pay off in benchmarks.
                    //
                    // SAFETY: We won't destroy or rearrange the leaf where `pos` is at
                    // by handling its parent recursively; at worst we will destroy or
                    // rearrange the parent through the grandparent, thus change the
                    // link to the parent inside the leaf.
                    if let Ok(parent) = unsafe { pos.reborrow_mut() }.into_node().ascend() {
                        if !parent.into_node().forget_type().fix_node_and_affected_ancestors(alloc) {
                            handle_emptied_internal_root();
                        }
                    }
                }
                (old_kv, pos)
            }
        *)
        Definition remove_leaf_kv
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ F; A ], [ self; handle_emptied_internal_root; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let handle_emptied_internal_root := M.alloc (| handle_emptied_internal_root |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                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::Leaf"
                              ];
                            Ty.path "alloc::collections::btree::node::marker::KV"
                          ],
                        "remove",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |),
                  [
                    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 pos := M.copy (| γ0_1 |) in
                        let~ len :=
                          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::Immut";
                                    K;
                                    V;
                                    Ty.path "alloc::collections::btree::node::marker::Leaf"
                                  ],
                                "len",
                                []
                              |),
                              [
                                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::Leaf"
                                            ];
                                          Ty.path "alloc::collections::btree::node::marker::Edge"
                                        ],
                                      "into_node",
                                      []
                                    |),
                                    [
                                      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"
                                            ],
                                          "reborrow",
                                          []
                                        |),
                                        [ pos ]
                                      |)
                                    ]
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.lt (|
                                          M.read (| len |),
                                          M.read (|
                                            M.get_constant (|
                                              "alloc::collections::btree::map::MIN_LEN"
                                            |)
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ idx :=
                                    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"
                                            ],
                                          "idx",
                                          []
                                        |),
                                        [ pos ]
                                      |)
                                    |) in
                                  let~ new_pos :=
                                    M.copy (|
                                      M.match_operator (|
                                        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::LeafOrInternal"
                                                ],
                                              "choose_parent_kv",
                                              []
                                            |),
                                            [
                                              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"
                                                    ],
                                                  "forget_type",
                                                  []
                                                |),
                                                [
                                                  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"
                                                        ],
                                                      "into_node",
                                                      []
                                                    |),
                                                    [ M.read (| pos |) ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::result::Result::Ok",
                                                  0
                                                |) in
                                              let γ1_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ0_0,
                                                  "alloc::collections::btree::node::LeftOrRight::Left",
                                                  0
                                                |) in
                                              let left_parent_kv := M.copy (| γ1_0 |) in
                                              let~ _ :=
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.use (M.alloc (| Value.Bool true |)) in
                                                        let _ :=
                                                          M.is_constant_or_break_match (|
                                                            M.read (| γ |),
                                                            Value.Bool true
                                                          |) in
                                                        let~ _ :=
                                                          M.match_operator (|
                                                            M.alloc (| Value.Tuple [] |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ :=
                                                                    M.use
                                                                      (M.alloc (|
                                                                        UnOp.not (|
                                                                          BinOp.eq (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "alloc::collections::btree::node::BalancingContext")
                                                                                  []
                                                                                  [ K; V ],
                                                                                "right_child_len",
                                                                                []
                                                                              |),
                                                                              [ left_parent_kv ]
                                                                            |),
                                                                            BinOp.Wrap.sub (|
                                                                              M.read (|
                                                                                M.get_constant (|
                                                                                  "alloc::collections::btree::map::MIN_LEN"
                                                                                |)
                                                                              |),
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                1
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |)) in
                                                                  let _ :=
                                                                    M.is_constant_or_break_match (|
                                                                      M.read (| γ |),
                                                                      Value.Bool true
                                                                    |) in
                                                                  M.alloc (|
                                                                    M.never_to_any (|
                                                                      M.call_closure (|
                                                                        M.get_function (|
                                                                          "core::panicking::panic",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            Value.String
                                                                              "assertion failed: left_parent_kv.right_child_len() == MIN_LEN - 1"
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |)
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (| Value.Tuple [] |)))
                                                            ]
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |) in
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "alloc::collections::btree::node::BalancingContext")
                                                                  []
                                                                  [ K; V ],
                                                                "can_merge",
                                                                []
                                                              |),
                                                              [ left_parent_kv ]
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path
                                                                "alloc::collections::btree::node::BalancingContext")
                                                              []
                                                              [ K; V ],
                                                            "merge_tracking_child_edge",
                                                            [ A ]
                                                          |),
                                                          [
                                                            M.read (| left_parent_kv |);
                                                            Value.StructTuple
                                                              "alloc::collections::btree::node::LeftOrRight::Right"
                                                              [ M.read (| idx |) ];
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::clone::Clone",
                                                                A,
                                                                [],
                                                                "clone",
                                                                []
                                                              |),
                                                              [ alloc ]
                                                            |)
                                                          ]
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let~ _ :=
                                                        M.match_operator (|
                                                          M.alloc (| Value.Tuple [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      Value.Bool true
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                let~ _ :=
                                                                  M.match_operator (|
                                                                    M.alloc (| Value.Tuple [] |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let γ :=
                                                                            M.use
                                                                              (M.alloc (|
                                                                                UnOp.not (|
                                                                                  BinOp.gt (|
                                                                                    M.call_closure (|
                                                                                      M.get_associated_function (|
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "alloc::collections::btree::node::BalancingContext")
                                                                                          []
                                                                                          [ K; V ],
                                                                                        "left_child_len",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        left_parent_kv
                                                                                      ]
                                                                                    |),
                                                                                    M.read (|
                                                                                      M.get_constant (|
                                                                                        "alloc::collections::btree::map::MIN_LEN"
                                                                                      |)
                                                                                    |)
                                                                                  |)
                                                                                |)
                                                                              |)) in
                                                                          let _ :=
                                                                            M.is_constant_or_break_match (|
                                                                              M.read (| γ |),
                                                                              Value.Bool true
                                                                            |) in
                                                                          M.alloc (|
                                                                            M.never_to_any (|
                                                                              M.call_closure (|
                                                                                M.get_function (|
                                                                                  "core::panicking::panic",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (|
                                                                                    Value.String
                                                                                      "assertion failed: left_parent_kv.left_child_len() > MIN_LEN"
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            |)
                                                                          |)));
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (M.alloc (|
                                                                            Value.Tuple []
                                                                          |)))
                                                                    ]
                                                                  |) in
                                                                M.alloc (| Value.Tuple [] |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) in
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path
                                                                "alloc::collections::btree::node::BalancingContext")
                                                              []
                                                              [ K; V ],
                                                            "steal_left",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| left_parent_kv |);
                                                            M.read (| idx |)
                                                          ]
                                                        |)
                                                      |)))
                                                ]
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::result::Result::Ok",
                                                  0
                                                |) in
                                              let γ1_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ0_0,
                                                  "alloc::collections::btree::node::LeftOrRight::Right",
                                                  0
                                                |) in
                                              let right_parent_kv := M.copy (| γ1_0 |) in
                                              let~ _ :=
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.use (M.alloc (| Value.Bool true |)) in
                                                        let _ :=
                                                          M.is_constant_or_break_match (|
                                                            M.read (| γ |),
                                                            Value.Bool true
                                                          |) in
                                                        let~ _ :=
                                                          M.match_operator (|
                                                            M.alloc (| Value.Tuple [] |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ :=
                                                                    M.use
                                                                      (M.alloc (|
                                                                        UnOp.not (|
                                                                          BinOp.eq (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "alloc::collections::btree::node::BalancingContext")
                                                                                  []
                                                                                  [ K; V ],
                                                                                "left_child_len",
                                                                                []
                                                                              |),
                                                                              [ right_parent_kv ]
                                                                            |),
                                                                            BinOp.Wrap.sub (|
                                                                              M.read (|
                                                                                M.get_constant (|
                                                                                  "alloc::collections::btree::map::MIN_LEN"
                                                                                |)
                                                                              |),
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                1
                                                                            |)
                                                                          |)
                                                                        |)
                                                                      |)) in
                                                                  let _ :=
                                                                    M.is_constant_or_break_match (|
                                                                      M.read (| γ |),
                                                                      Value.Bool true
                                                                    |) in
                                                                  M.alloc (|
                                                                    M.never_to_any (|
                                                                      M.call_closure (|
                                                                        M.get_function (|
                                                                          "core::panicking::panic",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            Value.String
                                                                              "assertion failed: right_parent_kv.left_child_len() == MIN_LEN - 1"
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |)
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (| Value.Tuple [] |)))
                                                            ]
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |) in
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "alloc::collections::btree::node::BalancingContext")
                                                                  []
                                                                  [ K; V ],
                                                                "can_merge",
                                                                []
                                                              |),
                                                              [ right_parent_kv ]
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path
                                                                "alloc::collections::btree::node::BalancingContext")
                                                              []
                                                              [ K; V ],
                                                            "merge_tracking_child_edge",
                                                            [ A ]
                                                          |),
                                                          [
                                                            M.read (| right_parent_kv |);
                                                            Value.StructTuple
                                                              "alloc::collections::btree::node::LeftOrRight::Left"
                                                              [ M.read (| idx |) ];
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::clone::Clone",
                                                                A,
                                                                [],
                                                                "clone",
                                                                []
                                                              |),
                                                              [ alloc ]
                                                            |)
                                                          ]
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let~ _ :=
                                                        M.match_operator (|
                                                          M.alloc (| Value.Tuple [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      Value.Bool true
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                let~ _ :=
                                                                  M.match_operator (|
                                                                    M.alloc (| Value.Tuple [] |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let γ :=
                                                                            M.use
                                                                              (M.alloc (|
                                                                                UnOp.not (|
                                                                                  BinOp.gt (|
                                                                                    M.call_closure (|
                                                                                      M.get_associated_function (|
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "alloc::collections::btree::node::BalancingContext")
                                                                                          []
                                                                                          [ K; V ],
                                                                                        "right_child_len",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        right_parent_kv
                                                                                      ]
                                                                                    |),
                                                                                    M.read (|
                                                                                      M.get_constant (|
                                                                                        "alloc::collections::btree::map::MIN_LEN"
                                                                                      |)
                                                                                    |)
                                                                                  |)
                                                                                |)
                                                                              |)) in
                                                                          let _ :=
                                                                            M.is_constant_or_break_match (|
                                                                              M.read (| γ |),
                                                                              Value.Bool true
                                                                            |) in
                                                                          M.alloc (|
                                                                            M.never_to_any (|
                                                                              M.call_closure (|
                                                                                M.get_function (|
                                                                                  "core::panicking::panic",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (|
                                                                                    Value.String
                                                                                      "assertion failed: right_parent_kv.right_child_len() > MIN_LEN"
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            |)
                                                                          |)));
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (M.alloc (|
                                                                            Value.Tuple []
                                                                          |)))
                                                                    ]
                                                                  |) in
                                                                M.alloc (| Value.Tuple [] |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) in
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path
                                                                "alloc::collections::btree::node::BalancingContext")
                                                              []
                                                              [ K; V ],
                                                            "steal_right",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| right_parent_kv |);
                                                            M.read (| idx |)
                                                          ]
                                                        |)
                                                      |)))
                                                ]
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::result::Result::Err",
                                                  0
                                                |) in
                                              let pos := M.copy (| γ0_0 |) in
                                              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::Edge"
                                                      ],
                                                    "new_edge",
                                                    []
                                                  |),
                                                  [ M.read (| pos |); M.read (| idx |) ]
                                                |)
                                              |)))
                                        ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      pos,
                                      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::Edge"
                                            ],
                                          "cast_to_leaf_unchecked",
                                          []
                                        |),
                                        [ M.read (| new_pos |) ]
                                      |)
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (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::Mut";
                                                      K;
                                                      V;
                                                      Ty.path
                                                        "alloc::collections::btree::node::marker::Leaf"
                                                    ],
                                                  "ascend",
                                                  []
                                                |),
                                                [
                                                  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"
                                                        ],
                                                      "into_node",
                                                      []
                                                    |),
                                                    [
                                                      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"
                                                            ],
                                                          "reborrow_mut",
                                                          []
                                                        |),
                                                        [ pos ]
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::result::Result::Ok",
                                              0
                                            |) in
                                          let parent := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        UnOp.not (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.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"
                                                                ],
                                                              "fix_node_and_affected_ancestors",
                                                              [ A ]
                                                            |),
                                                            [
                                                              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"
                                                                    ],
                                                                  "forget_type",
                                                                  []
                                                                |),
                                                                [
                                                                  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::Internal"
                                                                            ];
                                                                          Ty.path
                                                                            "alloc::collections::btree::node::marker::Edge"
                                                                        ],
                                                                      "into_node",
                                                                      []
                                                                    |),
                                                                    [ M.read (| parent |) ]
                                                                  |)
                                                                ]
                                                              |);
                                                              M.read (| alloc |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  let~ _ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::function::FnOnce",
                                                          F,
                                                          [ Ty.tuple [] ],
                                                          "call_once",
                                                          []
                                                        |),
                                                        [
                                                          M.read (| handle_emptied_internal_root |);
                                                          Value.Tuple []
                                                        ]
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [ M.read (| old_kv |); M.read (| pos |) ] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_remove_leaf_kv :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "remove_leaf_kv" (remove_leaf_kv K V).
      End Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_Leaf_alloc_collections_btree_node_marker_KV.
      
      Module Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_Internal_alloc_collections_btree_node_marker_KV.
        Definition Self (K V : Ty.t) : Ty.t :=
          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::Internal"
                ];
              Ty.path "alloc::collections::btree::node::marker::KV"
            ].
        
        (*
            fn remove_internal_kv<F: FnOnce(), A: Allocator + Clone>(
                self,
                handle_emptied_internal_root: F,
                alloc: A,
            ) -> ((K, V), Handle<NodeRef<marker::Mut<'a>, K, V, marker::Leaf>, marker::Edge>) {
                // Remove an adjacent KV from its leaf and then put it back in place of
                // the element we were asked to remove. Prefer the left adjacent KV,
                // for the reasons listed in `choose_parent_kv`.
                let left_leaf_kv = self.left_edge().descend().last_leaf_edge().left_kv();
                let left_leaf_kv = unsafe { left_leaf_kv.ok().unwrap_unchecked() };
                let (left_kv, left_hole) = left_leaf_kv.remove_leaf_kv(handle_emptied_internal_root, alloc);
        
                // The internal node may have been stolen from or merged. Go back right
                // to find where the original KV ended up.
                let mut internal = unsafe { left_hole.next_kv().ok().unwrap_unchecked() };
                let old_kv = internal.replace_kv(left_kv.0, left_kv.1);
                let pos = internal.next_leaf_edge();
                (old_kv, pos)
            }
        *)
        Definition remove_internal_kv
            (K V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self K V in
          match ε, τ, α with
          | [], [ F; A ], [ self; handle_emptied_internal_root; alloc ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let handle_emptied_internal_root := M.alloc (| handle_emptied_internal_root |) in
              let alloc := M.alloc (| alloc |) in
              M.read (|
                let~ left_leaf_kv :=
                  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"
                          ],
                        "left_kv",
                        []
                      |),
                      [
                        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::LeafOrInternal"
                              ],
                            "last_leaf_edge",
                            []
                          |),
                          [
                            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::Internal"
                                      ];
                                    Ty.path "alloc::collections::btree::node::marker::Edge"
                                  ],
                                "descend",
                                []
                              |),
                              [
                                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::Internal"
                                          ];
                                        Ty.path "alloc::collections::btree::node::marker::KV"
                                      ],
                                    "left_edge",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ left_leaf_kv :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        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::KV"
                              ]
                          ],
                        "unwrap_unchecked",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                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"
                                  ];
                                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"
                                  ]
                              ],
                            "ok",
                            []
                          |),
                          [ M.read (| left_leaf_kv |) ]
                        |)
                      ]
                    |)
                  |) 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::Leaf"
                              ];
                            Ty.path "alloc::collections::btree::node::marker::KV"
                          ],
                        "remove_leaf_kv",
                        [ F; A ]
                      |),
                      [
                        M.read (| left_leaf_kv |);
                        M.read (| handle_emptied_internal_root |);
                        M.read (| 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 left_kv := M.copy (| γ0_0 |) in
                        let left_hole := M.copy (| γ0_1 |) in
                        let~ internal :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                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::LeafOrInternal"
                                          ];
                                        Ty.path "alloc::collections::btree::node::marker::KV"
                                      ]
                                  ],
                                "unwrap_unchecked",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [
                                        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"
                                          ];
                                        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"
                                          ]
                                      ],
                                    "ok",
                                    []
                                  |),
                                  [
                                    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"
                                          ],
                                        "next_kv",
                                        []
                                      |),
                                      [ M.read (| left_hole |) ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |) in
                        let~ old_kv :=
                          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"
                                  ],
                                "replace_kv",
                                []
                              |),
                              [
                                internal;
                                M.read (| M.SubPointer.get_tuple_field (| left_kv, 0 |) |);
                                M.read (| M.SubPointer.get_tuple_field (| left_kv, 1 |) |)
                              ]
                            |)
                          |) in
                        let~ pos :=
                          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"
                                  ],
                                "next_leaf_edge",
                                []
                              |),
                              [ M.read (| internal |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [ M.read (| old_kv |); M.read (| pos |) ] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_remove_internal_kv :
          forall (K V : Ty.t),
          M.IsAssociatedFunction (Self K V) "remove_internal_kv" (remove_internal_kv K V).
      End Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_alloc_collections_btree_node_marker_Mut_K_V_alloc_collections_btree_node_marker_Internal_alloc_collections_btree_node_marker_KV.
    End remove.
  End btree.
End collections.
