∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] {r : Std.Rci α} {i : ℕ}, r.toList[i]? = Std.PRange.succMany? i r.lower