∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toListRev =
    match ↑it.step with
    | Std.IterStep.yield it' out => it'.toListRev ++ [out]
    | Std.IterStep.skip it' => it'.toListRev
    | Std.IterStep.done => []