∀ {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : α → δ) (a : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.mapKey f (Batteries.AssocList.cons a b es) =
    Batteries.AssocList.cons (f a) b (Batteries.AssocList.mapKey f es)