∀ {α : Type u} {β : α → Type v} (k : α) (v : β k)
  (motive :
    (l r : Std.DTreeMap.Internal.Impl α β) →
      l.Balanced →
        r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size → Std.DTreeMap.Internal.Impl α β → Prop),
  (∀ (hrb hrb_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced)
      (hlr :
        Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
          Std.DTreeMap.Internal.Impl.leaf.size),
      Std.DTreeMap.Internal.Impl.leaf.Balanced →
        Std.DTreeMap.Internal.Impl.leaf.Balanced →
          Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
              Std.DTreeMap.Internal.Impl.leaf.size →
            Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
                Std.DTreeMap.Internal.Impl.leaf.size →
              motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf hrb hrb_1 hlr
                (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf
                  Std.DTreeMap.Internal.Impl.leaf)) →
    (∀ (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) (size : ℕ) (k_1 : α) (v_1 : β k_1)
        (hrb_1 :
          (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
              Std.DTreeMap.Internal.Impl.leaf).Balanced)
        (hlr :
          Std.DTreeMap.Internal.Impl.BalanceLPrecond
            (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                Std.DTreeMap.Internal.Impl.leaf).size
            Std.DTreeMap.Internal.Impl.leaf.size),
        Std.DTreeMap.Internal.Impl.leaf.Balanced →
          (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                Std.DTreeMap.Internal.Impl.leaf).Balanced →
            Std.DTreeMap.Internal.Impl.BalanceLPrecond
                (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                    Std.DTreeMap.Internal.Impl.leaf).size
                Std.DTreeMap.Internal.Impl.leaf.size →
              Std.DTreeMap.Internal.Impl.BalanceLPrecond
                  (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                      Std.DTreeMap.Internal.Impl.leaf).size
                  Std.DTreeMap.Internal.Impl.leaf.size →
                motive Std.DTreeMap.Internal.Impl.leaf
                  (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                    Std.DTreeMap.Internal.Impl.leaf)
                  hrb hrb_1 hlr
                  (Std.DTreeMap.Internal.Impl.inner 2 k v Std.DTreeMap.Internal.Impl.leaf
                    (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 Std.DTreeMap.Internal.Impl.leaf
                      Std.DTreeMap.Internal.Impl.leaf))) →
      (∀ (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) (size : ℕ) (rk : α) (rv : β rk) (size_1 : ℕ) (k_1 : α)
          (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
          (hrb_1 :
            (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)).Balanced)
          (hlr :
            Std.DTreeMap.Internal.Impl.BalanceLPrecond
              (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)).size
              Std.DTreeMap.Internal.Impl.leaf.size),
          Std.DTreeMap.Internal.Impl.leaf.Balanced →
            (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)).Balanced →
              Std.DTreeMap.Internal.Impl.BalanceLPrecond
                  (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)).size
                  Std.DTreeMap.Internal.Impl.leaf.size →
                Std.DTreeMap.Internal.Impl.BalanceLPrecond
                    (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                        (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)).size
                    Std.DTreeMap.Internal.Impl.leaf.size →
                  motive Std.DTreeMap.Internal.Impl.leaf
                    (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r))
                    hrb hrb_1 hlr
                    (Std.DTreeMap.Internal.Impl.inner 3 rk rv
                      (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf
                        Std.DTreeMap.Internal.Impl.leaf)
                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r))) →
        (∀ (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) (size : ℕ) (rk : α) (rv : β rk) (size_1 : ℕ) (rlk : α)
            (rlv : β rlk) (l r : Std.DTreeMap.Internal.Impl α β)
            (hrb_1 :
              (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                  Std.DTreeMap.Internal.Impl.leaf).Balanced)
            (hlr :
              Std.DTreeMap.Internal.Impl.BalanceLPrecond
                (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                    Std.DTreeMap.Internal.Impl.leaf).size
                Std.DTreeMap.Internal.Impl.leaf.size),
            Std.DTreeMap.Internal.Impl.leaf.Balanced →
              (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                    Std.DTreeMap.Internal.Impl.leaf).Balanced →
                Std.DTreeMap.Internal.Impl.BalanceLPrecond
                    (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                        Std.DTreeMap.Internal.Impl.leaf).size
                    Std.DTreeMap.Internal.Impl.leaf.size →
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond
                      (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                          Std.DTreeMap.Internal.Impl.leaf).size
                      Std.DTreeMap.Internal.Impl.leaf.size →
                    motive Std.DTreeMap.Internal.Impl.leaf
                      (Std.DTreeMap.Internal.Impl.inner size rk rv (Std.DTreeMap.Internal.Impl.inner size_1 rlk rlv l r)
                        Std.DTreeMap.Internal.Impl.leaf)
                      hrb hrb_1 hlr
                      (Std.DTreeMap.Internal.Impl.inner 3 rlk rlv
                        (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf
                          Std.DTreeMap.Internal.Impl.leaf)
                        (Std.DTreeMap.Internal.Impl.inner 1 rk rv Std.DTreeMap.Internal.Impl.leaf
                          Std.DTreeMap.Internal.Impl.leaf))) →
          (∀ (rs : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
              (hrb : (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced)
              (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced)
              (hlr :
                Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
                  (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size),
              (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced →
                Std.DTreeMap.Internal.Impl.leaf.Balanced →
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
                      (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                    Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
                        (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                      motive (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r) Std.DTreeMap.Internal.Impl.leaf hrb hlb
                        hlr
                        (Std.DTreeMap.Internal.Impl.inner (1 + rs) k v (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r)
                          Std.DTreeMap.Internal.Impl.leaf)) →
            (∀ (rs : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
                (hrb : (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced) (ls : ℕ) (lk : α) (lv : β lk),
                ls > Std.DTreeMap.Internal.delta * rs →
                  ∀ (lls : ℕ) (k_2 : α) (v_2 : β k_2) (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrk : α)
                    (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β)
                    (hlb :
                      (Std.DTreeMap.Internal.Impl.inner ls lk lv (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                          (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced)
                    (hlr :
                      Std.DTreeMap.Internal.Impl.BalanceLPrecond
                        (Std.DTreeMap.Internal.Impl.inner ls lk lv
                            (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                            (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                        (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size),
                    lls < Std.DTreeMap.Internal.ratio * lrs →
                      (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced →
                        (Std.DTreeMap.Internal.Impl.inner ls lk lv
                              (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                              (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced →
                          Std.DTreeMap.Internal.Impl.BalanceLPrecond
                              (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                  (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                  (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                              (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                            (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                  (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                  (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced →
                              Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                  (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                      (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                                  (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                                Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                    (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                        (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                        (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                                    (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                                  motive (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r)
                                    (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                      (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
                                    hrb hlb hlr
                                    (Std.DTreeMap.Internal.Impl.inner (1 + rs + ls) lk lv
                                      (Std.DTreeMap.Internal.Impl.inner (1 + rs + lls) k v
                                        (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r)
                                        (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1))
                                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))) →
              (∀ (rs : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
                  (hrb : (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced) (ls : ℕ) (lk : α) (lv : β lk),
                  ls > Std.DTreeMap.Internal.delta * rs →
                    ∀ (lls : ℕ) (k_2 : α) (v_2 : β k_2) (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrk : α)
                      (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β)
                      (hlb :
                        (Std.DTreeMap.Internal.Impl.inner ls lk lv
                            (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                            (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced)
                      (hlr :
                        Std.DTreeMap.Internal.Impl.BalanceLPrecond
                          (Std.DTreeMap.Internal.Impl.inner ls lk lv
                              (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                              (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                          (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size),
                      ¬lls < Std.DTreeMap.Internal.ratio * lrs →
                        (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced →
                          (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced →
                            Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                    (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                    (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                                (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                              (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                    (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                    (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).Balanced →
                                Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                    (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                        (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                        (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                                    (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                                  Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                      (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                          (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                          (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)).size
                                      (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                                    motive (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r)
                                      (Std.DTreeMap.Internal.Impl.inner ls lk lv
                                        (Std.DTreeMap.Internal.Impl.inner lls k_2 v_2 l_1 r_1)
                                        (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
                                      hrb hlb hlr
                                      (Std.DTreeMap.Internal.Impl.inner (1 + rs + ls) k_2 v_2
                                        (Std.DTreeMap.Internal.Impl.inner (1 + rs + l_1.size) k v
                                          (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r) l_1)
                                        (Std.DTreeMap.Internal.Impl.inner (1 + lrs + r_1.size) lk lv r_1
                                          (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr)))) →
                (∀ (rs : ℕ) (k_1 : α) (v_1 : β k_1) (l r : Std.DTreeMap.Internal.Impl α β)
                    (hrb : (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced) (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.BalanceLPrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                        (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size),
                    ¬ls > Std.DTreeMap.Internal.delta * rs →
                      (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).Balanced →
                        (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced →
                          Std.DTreeMap.Internal.Impl.BalanceLPrecond
                              (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                              (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                            Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                                (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r).size →
                              motive (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r)
                                (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hrb hlb hlr
                                (Std.DTreeMap.Internal.Impl.inner (1 + rs + ls) k v
                                  (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l r)
                                  (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr))) →
                  ∀ (l r : Std.DTreeMap.Internal.Impl α β) (hlb : l.Balanced) (hrb : r.Balanced)
                    (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size),
                    motive l r hlb hrb hlr (Std.DTreeMap.Internal.Impl.balanceR k v l r hlb hrb hlr)