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.

Doesn't lookup_insert_is_Some' already give this?

I guess it kind of does, even though one has to do an extra right afterwards.
I'm now somewhat unconvinced by the usefulness of the new lemma myself, so I guess I'll close the MR. (the new lemma is more direct, but also has a longer name, so...)

Sorry for the noise!

closed

If you think it's useful, we can add _1 and _2 (or _21 and _22 to also get rid of the disjuntion) variants of the already existing lemmas. Such lemmas could be useful for auto and friends.