∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced)
  (hr : r.Balanced),
  Std.DTreeMap.Internal.Impl.link k v l r hl hr =
    match l, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl =>
      let d := Std.DTreeMap.Internal.Impl.insertMin k v r ⋯;
      { impl := d.impl, balanced_impl := ⋯, size_impl := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner szl k' v' l' r', hl =>
      match r, hr with
      | Std.DTreeMap.Internal.Impl.leaf, hr =>
        let d := Std.DTreeMap.Internal.Impl.insertMax k v (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r') ⋯;
        { impl := d.impl, balanced_impl := ⋯, size_impl := ⋯ }
      | Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'', hr =>
        if h₁ : Std.DTreeMap.Internal.delta * szl < szr then
          match Std.DTreeMap.Internal.Impl.link k v (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r') l'' ⋯ ⋯ with
          | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } =>
            { impl := Std.DTreeMap.Internal.Impl.balanceLErase k'' v'' ℓ r'' ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
        else
          if h₂ : Std.DTreeMap.Internal.delta * szr < szl then
            match Std.DTreeMap.Internal.Impl.link k v r' (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') ⋯ ⋯ with
            | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } =>
              { impl := Std.DTreeMap.Internal.Impl.balanceRErase k' v' l' ℓ ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
          else
            {
              impl :=
                Std.DTreeMap.Internal.Impl.inner (szl + 1 + szr) k v (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r')
                  (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r''),
              balanced_impl := ⋯, size_impl := ⋯ }