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