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