∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → Bool},
  it.find? f =
    match ↑it.step with
    | Std.IterStep.yield it' out => if f out = true then some out else it'.find? f
    | Std.IterStep.skip it' => it'.find? f
    | Std.IterStep.done => none