∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {f : β → γ},
  (Std.Iter.map f it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => Std.PlausibleIterStep.yield (Std.Iter.map f it') (f out) ⋯
    | ⟨Std.IterStep.skip it', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.map f it') ⋯
    | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯