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