∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterators.Finite α m] {it : Std.IterM m β},
  it.ensureTermination.toListRev = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← it'.toListRev
        pure (__do_lift ++ [out])
      | Std.IterStep.skip it' => it'.toListRev
      | Std.IterStep.done => pure []