@[simp]
theorem
Std.PRange.toList_iter_eq_toList
{α : Type u_1}
{sl su : BoundShape}
[UpwardEnumerable α]
[BoundedUpwardEnumerable sl α]
[SupportsUpperBound su α]
[HasFiniteRanges su α]
[LawfulUpwardEnumerable α]
(r : PRange { lower := sl, upper := su } α)
: