theorem Std.Iter.uLift_eq_toIter_uLift_toIterM {α β : Type u} {it : Iter β} : it.uLift = (it.toIterM.uLift Id).toIter

theorem Std.Iter.step_uLift {α β : Type u} [Iterator α Id β] {it : Iter β} : it.uLift.step = match it.step with | ⟨IterStep.yield it' out, h⟩ => PlausibleIterStep.yield it'.uLift { down := out } ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip it'.uLift ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

@[simp]

theorem Std.Iter.toList_uLift {α β : Type u} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] : it.uLift.toList = List.map ULift.up it.toList

@[simp]

theorem Std.Iter.toListRev_uLift {α β : Type u} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] : it.uLift.toListRev = List.map ULift.up it.toListRev

@[simp]

theorem Std.Iter.toArray_uLift {α β : Type u} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] : it.uLift.toArray = Array.map ULift.up it.toArray

@[simp]

theorem Std.Iter.count_uLift {α β : Type u} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] : it.uLift.count = it.count