Workaround to avoid `injection` from unfolding equalities on `dom`

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.

changed title from Workaround to avoid [injection] from unfolding equalities on [dom] to Workaround to avoid {++}injection{++} from unfolding equalities on {++}dom{++}

changed the description

added 1 commit

• 5bb47351 - Tests.

Compare with previous version

resolved all threads

merged

mentioned in commit 56558ffb