{α : Type u_1} →
  {β : α → Type u_2} →
    (motive :
        (l : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced →
            Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size Std.DTreeMap.Internal.Impl.leaf.size → Sort u_3) →
      (l : Std.DTreeMap.Internal.Impl α β) →
        (hlb : l.Balanced) →
          (hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size Std.DTreeMap.Internal.Impl.leaf.size) →
            ((hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                (hlr :
                    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond Std.DTreeMap.Internal.Impl.leaf.size
                      Std.DTreeMap.Internal.Impl.leaf.size) →
                  motive Std.DTreeMap.Internal.Impl.leaf hlb hlr) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (hlb :
                          (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf
                              Std.DTreeMap.Internal.Impl.leaf).Balanced) →
                        (hlr :
                            Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                              (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf
                                  Std.DTreeMap.Internal.Impl.leaf).size
                              Std.DTreeMap.Internal.Impl.leaf.size) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf
                              Std.DTreeMap.Internal.Impl.leaf)
                            hlb hlr) →
                ((size : ℕ) →
                    (lk : α) →
                      (lv : β lk) →
                        (size_1 : ℕ) →
                          (lrk : α) →
                            (lrv : β lrk) →
                              (l r : Std.DTreeMap.Internal.Impl α β) →
                                (hlb :
                                    (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                                        (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r)).Balanced) →
                                  (hlr :
                                      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                                        (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                                            (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r)).size
                                        Std.DTreeMap.Internal.Impl.leaf.size) →
                                    motive
                                      (Std.DTreeMap.Internal.Impl.inner size lk lv Std.DTreeMap.Internal.Impl.leaf
                                        (Std.DTreeMap.Internal.Impl.inner size_1 lrk lrv l r))
                                      hlb hlr) →
                  ((size : ℕ) →
                      (lk : α) →
                        (lv : β lk) →
                          (ll : Std.DTreeMap.Internal.Impl α β) →
                            (size_1 : ℕ) →
                              (k : α) →
                                (v : β k) →
                                  (l r : Std.DTreeMap.Internal.Impl α β) →
                                    (h : ll = Std.DTreeMap.Internal.Impl.inner size_1 k v l r) →
                                      (hlb :
                                          (Std.DTreeMap.Internal.Impl.inner size lk lv
                                              (namedPattern ll (Std.DTreeMap.Internal.Impl.inner size_1 k v l r) h)
                                              Std.DTreeMap.Internal.Impl.leaf).Balanced) →
                                        (hlr :
                                            Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                                              (Std.DTreeMap.Internal.Impl.inner size lk lv
                                                  (namedPattern ll (Std.DTreeMap.Internal.Impl.inner size_1 k v l r) h)
                                                  Std.DTreeMap.Internal.Impl.leaf).size
                                              Std.DTreeMap.Internal.Impl.leaf.size) →
                                          motive
                                            (Std.DTreeMap.Internal.Impl.inner size lk lv
                                              (namedPattern ll (Std.DTreeMap.Internal.Impl.inner size_1 k v l r) h)
                                              Std.DTreeMap.Internal.Impl.leaf)
                                            hlb hlr) →
                    ((ls : ℕ) →
                        (lk : α) →
                          (lv : β lk) →
                            (ll : Std.DTreeMap.Internal.Impl α β) →
                              (lls : ℕ) →
                                (k : α) →
                                  (v : β k) →
                                    (l r : Std.DTreeMap.Internal.Impl α β) →
                                      (h : ll = Std.DTreeMap.Internal.Impl.inner lls k v l r) →
                                        (lr : Std.DTreeMap.Internal.Impl α β) →
                                          (lrs : ℕ) →
                                            (lrk : α) →
                                              (lrv : β lrk) →
                                                (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                                                  (h_5 : lr = Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr) →
                                                    (hlb :
                                                        (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                                            (namedPattern ll
                                                              (Std.DTreeMap.Internal.Impl.inner lls k v l r) h)
                                                            (namedPattern lr
                                                              (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)
                                                              h_5)).Balanced) →
                                                      (hlr :
                                                          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                                                            (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                                                (namedPattern ll
                                                                  (Std.DTreeMap.Internal.Impl.inner lls k v l r) h)
                                                                (namedPattern lr
                                                                  (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)
                                                                  h_5)).size
                                                            Std.DTreeMap.Internal.Impl.leaf.size) →
                                                        motive
                                                          (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                                            (namedPattern ll
                                                              (Std.DTreeMap.Internal.Impl.inner lls k v l r) h)
                                                            (namedPattern lr
                                                              (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)
                                                              h_5))
                                                          hlb hlr) →
                      motive l hlb hlr