∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (motive : Std.DTreeMap.Internal.RxoIterator α β → Sort u_3)
  (upper : α) (h_1 : (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper })
  (h_2 :
    (k : α) →
      (v : β k) →
        (t : Std.DTreeMap.Internal.Impl α β) →
          (it : Std.DTreeMap.Internal.Zipper α β) →
            (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }),
  (match { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper } with
    | { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper } => h_1 upper
    | { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper } => h_2 k v t it upper) =
    h_1 upper