∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)}
  {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false)
  {h : Std.Internal.List.containsKey k (Std.Internal.List.insertListConst l toInsert) = true},
  Std.Internal.List.getKey k (Std.Internal.List.insertListConst l toInsert) h = Std.Internal.List.getKey k l ⋯