∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] {α : Type uu} (as : List α) (init : β)
  (f : γ → α → β → m (ForInStep β)), Lean.Order.monotone f → Lean.Order.monotone fun x => forIn as init (f x)