no goals
m : Type u_1 → Type u_2
δ : Type u_1
α : Type u_3
β : Type u_4
inst✝ : Monad m
f : δ → α → β → m δ
init : δ
l : AssocList α β
⊢ foldlM f init l =
    List.foldlM
      (fun d x =>
        match x with
        | (a, b) => f d a b)
      init (toList l)
induction l generalizing init <;> simp [*, foldlM]