∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxEntry? = some ⟨k, v⟩