∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {t : Std.DTreeMap.Internal.Impl α β}
  {it : Std.DTreeMap.Internal.Zipper α β},
  (Std.DTreeMap.Internal.Zipper.cons k v t it).step =
    Std.IterStep.yield { internalState := Std.DTreeMap.Internal.Zipper.prependMap t it } ⟨k, v⟩