∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.containsKey k toInsert = false →
    Std.Internal.List.getValueD k (Std.Internal.List.insertList l toInsert) fallback =
      Std.Internal.List.getValueD k l fallback