Skip to content

Add a weakening lemma for goals: "is_Some (<[i:=x]>m !! j)"

Armaël Guéneau requested to merge Armael/stdpp:is_Some_lookup_weaken into master

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.

Merge request reports