∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k) (x : List ((a : α) × β a)),
  Std.Internal.List.replaceEntry k v x =
    match x with
    | [] => []
    | ⟨k', v'⟩ :: l => bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: Std.Internal.List.replaceEntry k v l