As reported by @vsiles and @msammler on Mattermost the tactics simplify_eq and injection accidentally unfold equalities dom (gset A) m1 = dom (gset A) m2 into merge ....
The culprit is that the definition of dom on gmap starts with a constructor MapSet. This MR tweaks the definition a bit, by inserting an eta expansion, to avoid that.