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