∀ {α : Type u_1} {β : α → Type u_2} (k' : α) (v' : β k'),
  (Std.DTreeMap.Internal.Impl.inner 1 k' v' Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf).size ≤
    Std.DTreeMap.Internal.Impl.leaf.size + 1