∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} {n : Type u_1 → Type u_3} {γ : Type u_1}
  [inst : Std.Iterator α m β] [inst_1 : Monad m] [inst_2 : Monad n] [inst_3 : MonadLiftT m n] [LawfulMonad m]
  [LawfulMonad n] [LawfulMonadLiftT m n] {it : Std.IterM m β}
  {f : (step : Std.IterStep (Std.IterM m β) β) → (Std.Iterators.HetT.liftInner n it.stepAsHetT).Property step → n γ},
  (Std.Iterators.HetT.liftInner n it.stepAsHetT).prun f = do
    let step ← liftM it.step
    f ↑step.inflate ⋯