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