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