∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  {it : Std.DTreeMap.Internal.Zipper α β} [inst : Ord α] {upper : α} {h : (compare k upper).isLT = true},
  { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }.step =
    Std.IterStep.yield { internalState := { iter := Std.DTreeMap.Internal.Zipper.prependMap t it, upper := upper } }
      ⟨k, v⟩