∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k' (Std.Internal.List.modifyKey k f l) =
      if (k == k') = true then if Std.Internal.List.containsKey k l = true then some k else none
      else Std.Internal.List.getKey? k' l