no goals
δ : Type u_1
α : Type u_2
β : Type u_3
f : δ → α → β → δ
init : δ
l : AssocList α β
⊢ foldl f init l =
    List.foldl
      (fun d x =>
        match x with
        | (a, b) => f d a b)
      init (toList l)
simp [List.foldl_eq_foldlM, foldl, Id.run]