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