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