∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.maxView! k v l r =
    match r with
    | Std.DTreeMap.Internal.Impl.leaf => { k := k, v := v, tree := l }
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' =>
      have d := Std.DTreeMap.Internal.Impl.maxView! k' v' l' r';
      { k := d.k, v := d.v, tree := Std.DTreeMap.Internal.Impl.balanceL! k v l d.tree }