A stronger version of `big_sepM_insert_override_{1,2}`.

This implements

  Lemma big_sepM_insert_wand_overwrite Φ m i x x' :
    m !! i = Some x →
    ([∗ map] k↦y ∈ m, Φ k y) ⊢
      Φ i x ∗ (Φ i x' -∗ ([∗ map] k↦y ∈ <[i:=x']> m, Φ k y)).

Which is stronger than big_sepM_insert_override_1 and big_sepM_insert_override_2, and is nicer than ``big_sepM_insert_override` because it is stated completely inside the logic (modulo the lookup part, of course). I think this lemma is useful for a general user. For instance, it allows you to do incremental updates to the map which holds some resources that can be updated by symbolic execution.

There are some questions that are worth considering tho:

1. Naming. I called this lemma "overwrite" because it writes over the location i in the map. I was told that the other lemmas are "override" lemmas because the user sort of takes control for a bit. There is also some discussion about those terms on stackoverflow

2. Old lemmas. Should they still be kept in?