∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  {it : Std.Iter α},
  it.toList =
    match it.internalState.next with
    | none => []
    | some a =>
      if a < it.internalState.upperBound then
        a :: { internalState := { next := Std.PRange.succ? a, upperBound := it.internalState.upperBound } }.toList
      else []