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