∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)}
  {k : α},
  Std.Internal.List.containsKey k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = Std.Internal.List.containsKey k l