{α : Type u} →
  {β : α → Type v} →
    {lb ub : ℕ} →
      {P : Sort u_1} →
        {impl : Std.DTreeMap.Internal.Impl α β} →
          {balanced_impl : impl.Balanced} →
            {lb_le_size_impl : lb ≤ impl.size} →
              {size_impl_le_ub : impl.size ≤ ub} →
                {impl' : Std.DTreeMap.Internal.Impl α β} →
                  {balanced_impl' : impl'.Balanced} →
                    {lb_le_size_impl' : lb ≤ impl'.size} →
                      {size_impl_le_ub' : impl'.size ≤ ub} →
                        { impl := impl, balanced_impl := balanced_impl, lb_le_size_impl := lb_le_size_impl,
                              size_impl_le_ub := size_impl_le_ub } =
                            { impl := impl', balanced_impl := balanced_impl', lb_le_size_impl := lb_le_size_impl',
                              size_impl_le_ub := size_impl_le_ub' } →
                          (impl ≍ impl' → P) → P