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