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