∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (k : α) (v : β k)
  (l_1 : List ((a : α) × β a)),
  Std.Internal.List.insertListIfNew l (⟨k, v⟩ :: l_1) =
    Std.Internal.List.insertListIfNew (Std.Internal.List.insertEntryIfNew k v l) l_1