∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : LT α] [inst_3 : DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst : Std.PRange.InfinitelyUpwardEnumerable α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {lo hi : α},
  ((Std.PRange.succ lo)...Std.PRange.succ hi).toList = List.map Std.PRange.succ (lo...hi).toList