∀ {α : Type u} {β : α → Type v} {size : ℕ} {impl : Std.DTreeMap.Internal.Impl α β} {balanced_impl : impl.Balanced}
  {size_impl : impl.size = size} {impl_1 : Std.DTreeMap.Internal.Impl α β} {balanced_impl_1 : impl_1.Balanced}
  {size_impl_1 : impl_1.size = size},
  { impl := impl, balanced_impl := balanced_impl, size_impl := size_impl } =
      { impl := impl_1, balanced_impl := balanced_impl_1, size_impl := size_impl_1 } →
    impl = impl_1