∀ {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : δ → α → β → m δ) (x : δ)
  (a : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.foldlM f x (Batteries.AssocList.cons a b es) = do
    let __do_lift ← f x a b
    Batteries.AssocList.foldlM f __do_lift es