Skip to content

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.