Mark gset methods as simpl never to stop `cbn` from unfolding them
This clarifies what's meant to happen anyway, and is apparently needed for cbn. (I haven't yet tried doing this at the mapset level).
Example of the problem: without this change, cbn mangles the goal in the following:
Goal {[1; 2; 3]} =@{gset nat} ∅.
Fail progress simpl.
progress cbn. Show.I'd want progress cbn to fail, instead the above gives:
The command has indeed failed with message:
Failed to progress.
1 subgoal
============================
{| mapset_car := {[1 := ()]} ∪ {[2 := ()]} ∪ {[3 := ()]} |} = ∅