no goals
ι : Type ?u.280076
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l : List α
⊢ foldrM f b l = foldr (fun a mb => mb >>= f a) (pure b) l
induction l <;> simp [*]