∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size → Sort u_3)
  (rs : ℕ) (k : α) (v : β k) (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).size)
  (h_1 :
    (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hrb hlr)
  (h_2 :
    (rs : ℕ) →
      (k : α) →
        (v : β k) →
          (l_2 r : Std.DTreeMap.Internal.Impl α β) →
            (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_2 r).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l_2 r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner rs k v l_2 r) hrb hlr),
  (match Std.DTreeMap.Internal.Impl.inner rs k v l_1 r, hrb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr => h_1 hrb hlr
    | Std.DTreeMap.Internal.Impl.inner rs k v l_2 r, hrb, hlr => h_2 rs k v l_2 r hrb hlr) =
    h_2 rs k v l_1 r hrb hlr