∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.maxView! k v l (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    { k := (Std.DTreeMap.Internal.Impl.maxView! k' v' l' r').k,
      v := (Std.DTreeMap.Internal.Impl.maxView! k' v' l' r').v,
      tree := Std.DTreeMap.Internal.Impl.balanceL! k v l (Std.DTreeMap.Internal.Impl.maxView! k' v' l' r').tree }