Add a weakening lemma for goals: "is_Some (<[i:=x]>m !! j)"
I found this lemma to be quite useful in situations where one just wants to eliminate an insert that only updates a value that we know was already in the map.
I found this lemma to be quite useful in situations where one just wants to eliminate an insert that only updates a value that we know was already in the map.