{α : Type u_1} →
  {β : α → Type u_2} →
    (rs : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (motive :
                (l_1 : Std.DTreeMap.Internal.Impl α β) →
                  l_1.Balanced →
                    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l_1.size
                        (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
                      Sort u_3) →
              (l_1 : Std.DTreeMap.Internal.Impl α β) →
                (hlb : l_1.Balanced) →
                  (hlr :
                      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l_1.size
                        (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                    ((hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                        (hlr :
                            Std.DTreeMap.Internal.Impl.BalanceLErasePrecond Std.DTreeMap.Internal.Impl.leaf.size
                              (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                          motive Std.DTreeMap.Internal.Impl.leaf hlb hlr) →
                      ((ls : ℕ) →
                          (lk : α) →
                            (lv : β lk) →
                              (ll lr : Std.DTreeMap.Internal.Impl α β) →
                                (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced) →
                                  (hlr :
                                      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                                        (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                                        (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                                    motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hlb hlr) →
                        motive l_1 hlb hlr