no goals
α : Type u_1
β : Type u_2
δ : Type u_3
f : α → β → δ
l : AssocList α β
⊢ toList (mapVal f l) =
    List.map
      (fun x =>
        match x with
        | (a, b) => (a, f a b))
      (toList l)
induction l <;> simp [*]