no goals
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l l' : List α
⊢ List.foldlM f b (l ++ l') = do
    let init ← List.foldlM f b l
    List.foldlM f init l'
induction l generalizing b <;> simp [*]