For most map operations we have a lemma
lookup_foo that always applies -- except, ironically, for
Unfortunately the lemma really should be called
lookup_insert, but that name is already taken, so I called it
lookup_insert_eq. Arguably that would be a good name for the
i = j case and nicely symmetric with
lookup_insert_ne (well, the really symmetric version would take
i = j as precondition, which can make it easier to rewrite with).
lookup_insert is used a lot so I feel renaming might be a bit too disruptive...