theorem Std.Slice.Array.internalIter_eq {α : Type u} {s : Subarray α} : Internal.iter s = Iterators.Iter.map (fun (x : ULift { out : Nat // out < s.array.size }) => match x with | { down := i } => s.array[i.val]) ((PRange.Internal.iter { lower := s.start, upper := s.stop }).attachWith (fun (x : Nat) => x < s.array.size) ⋯).uLift

theorem Std.Slice.Array.toList_internalIter {α : Type u} {s : Subarray α} : (Internal.iter s).toList = List.map (fun (i : { x : Nat // x < s.array.size }) => s.array[i.val]) ({ lower := s.start, upper := s.stop }.toList.attachWith (fun (x : Nat) => x < s.array.size) ⋯)