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