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