theorem Std.Iterators.ListIterator.stepAsHetT_iterM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {l : List β} : (l.iterM m).stepAsHetT = match l with | [] => pure IterStep.done | x :: xs => pure (IterStep.yield (xs.iterM m) x)