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