∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β)
  (x_2 : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false),
  (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minEntry x_2 = ⟨k, v⟩