rename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteq

This hopefully makes the lemmas easier to find.

theories/gmap.v

@@ -258,6 +258,10 @@ Section gset.
   Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
   Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
+  Lemma gset_eq (Y X : gset K) :
+    (forall x, x ∈ X ↔ x ∈ Y) → X = Y.
+  Proof. apply mapset_eq. Qed.
+
   Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
     (λ _, x) <$> mapset_car X.