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 := ()]} |} = ∅

theories/gmap.v

@@ -237,6 +237,7 @@ Definition gset K `{Countable K} := mapset (gmap K).
 
 Section gset.
   Context `{Countable K}.
+  (* Lift instances of operational TCs from [mapset] and mark them [simpl never]. *)
   Global Instance gset_elem_of: ElemOf K (gset K) := _.
   Global Instance gset_empty : Empty (gset K) := _.
   Global Instance gset_singleton : Singleton K (gset K) := _.
@@ -244,10 +245,6 @@ Section gset.
   Global Instance gset_intersection: Intersection (gset K) := _.
   Global Instance gset_difference: Difference (gset K) := _.
   Global Instance gset_elements: Elements K (gset K) := _.
-  Global Instance gset_leibniz : LeibnizEquiv (gset K) := _.
-  Global Instance gset_semi_set : SemiSet K (gset K) | 1 := _.
-  Global Instance gset_set : Set_ K (gset K) | 1 := _.
-  Global Instance gset_fin_set : FinSet K (gset K) := _.
   Global Instance gset_eq_dec : EqDecision (gset K) := _.
   Global Instance gset_countable : Countable (gset K) := _.
   Global Instance gset_equiv_dec : RelDecision (≡@{gset K}) | 1 := _.
@@ -255,6 +252,27 @@ Section gset.
   Global Instance gset_disjoint_dec : RelDecision (##@{gset K}) := _.
   Global Instance gset_subseteq_dec : RelDecision (⊆@{gset K}) := _.
   Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
+
+  Global Arguments gset_elem_of : simpl never.
+  Global Arguments gset_empty : simpl never.
+  Global Arguments gset_singleton : simpl never.
+  Global Arguments gset_union : simpl never.
+  Global Arguments gset_intersection : simpl never.
+  Global Arguments gset_difference : simpl never.
+  Global Arguments gset_elements : simpl never.
+  Global Arguments gset_eq_dec : simpl never.
+  Global Arguments gset_countable : simpl never.
+  Global Arguments gset_equiv_dec : simpl never.
+  Global Arguments gset_elem_of_dec : simpl never.
+  Global Arguments gset_disjoint_dec : simpl never.
+  Global Arguments gset_subseteq_dec : simpl never.
+  Global Arguments gset_dom : simpl never.
+
+  (* Lift instances of other TCs. *)
+  Global Instance gset_leibniz : LeibnizEquiv (gset K) := _.
+  Global Instance gset_semi_set : SemiSet K (gset K) | 1 := _.
+  Global Instance gset_set : Set_ K (gset K) | 1 := _.
+  Global Instance gset_fin_set : FinSet K (gset K) := _.
   Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
   (** If you are looking for a lemma showing that [gset] is extensional, see