For most map operations we have a lemma lookup_foo that always applies -- except, ironically, for insert.
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...