simplify_map_eq sometimes fails to rewrite with `lookup_singleton_ne`
This came up in iris!959 (merged), see the FIXMEs in gmap_view.v. This is probably related to old unification; rewrite ->lookup_singleton_ne
fails but rewrite lookup_singleton_ne
succeeds. So something similar to !497 (merged) could help.