∀ {α : Type u_1} {β : α → Type u_2} (sz : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner sz k v l' r').Balanced →
    ∀ (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β),
      (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').Balanced → r''.Balanced