∀ {α : Type u_1} {β : α → Type u_2} (k : α) (v : β k) (szl : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β) (szr : ℕ) (k'' : α) (v'' : β k'') (l'' r'' : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner (szl + 1 + szr) k v (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r')
        (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'')).size =
    (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 +
      (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size