no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
s : ForInStep β
a : α
l : List α
⊢ bindList f (a :: l) s = do
    let x ← ForInStep.bind s (f a)
    bindList f l x
simp