diff --git a/opam b/opam
index 4c60499fd437cb6a2bc24dc539bb84db6beea266..362c0f85205c5eb5dfbdeb641a49c0e27cf73d1f 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
 depends: [
   "coq" { (>= "8.8.2" & < "8.10~") | (= "dev") }
-  "coq-iris" { (= "dev.2019-02-07.0.0655aa19") | (= "dev") }
+  "coq-iris" { (= "dev.2019-02-22.1.9c04e2b4") | (= "dev") }
 ]
diff --git a/theories/adequacy.v b/theories/adequacy.v
index d98eca8df86ffdaea620c398f93188acdb68179e..b6060e699b548c2f2acaf9e30962c60edfa54332 100644
--- a/theories/adequacy.v
+++ b/theories/adequacy.v
@@ -23,7 +23,7 @@ Proof. solve_inG. Qed.
 (* Definition to_view (σ : language.state ra_lang) : Views := (Excl <$> threads σ). *)
 Definition loc_sets (σ : language.state ra_lang) : gmap loc (gset message) :=
   let locs := {[ mloc m | m <- msgs (mem σ) ]} in
-  map_imap (λ l _, Some {[ m <- msgs (mem σ) | mloc m = l ]}) (to_gmap () locs).
+  map_imap (λ l _, Some {[ m <- msgs (mem σ) | mloc m = l ]}) (gset_to_gmap () locs).
 Definition to_hist (σ : language.state ra_lang) : Hists :=
   let maxsets := (λ M, {[ m <- M | set_Forall (λ m', mtime m' ⊑ mtime m) M ]} )  <$> loc_sets σ in
   let hists := map_vt <$> maxsets in
@@ -32,7 +32,7 @@ Definition to_hist (σ : language.state ra_lang) : Hists :=
 (* TODO: can we avoid this? *)
 (* Definition to_info (σ : language.state ra_lang) : Infos := *)
 (*   let locs := {[ mloc m | m <- msgs (mem σ) ]} in *)
-(*   let infos : gmap loc (frac.fracR * _) := to_gmap (1%Qp, to_agree 1%positive) locs in *)
+(*   let infos : gmap loc (frac.fracR * _) := gset_to_gmap (1%Qp, to_agree 1%positive) locs in *)
 (*   (infos). *)
 Definition to_info (σ : language.state ra_lang) : Infos :=
   (λ _, (1%Qp, to_agree 1%positive)) <$> to_hist σ.
@@ -56,7 +56,7 @@ Proof.
   rewrite /map_imap /dom /= /gset_dom /mapset_dom /= => x.
   rewrite !elem_of_mapset_dom_with.
   setoid_rewrite (_ : ∀ P, P ∧ true ↔ P); [|naive_solver|naive_solver].
-  setoid_rewrite <-(elem_of_map_of_list _ _ _ _); last first.
+  setoid_rewrite <-(elem_of_list_to_map _ _ _ _); last first.
   { apply NoDup_fmap_fst; last apply NoDup_omap; last apply NoDup_map_to_list.
     - intros ? ? ?. rewrite !elem_of_list_omap.
       assert (R : ∀ (a : K) (b : B) x, (pair (x.1) <$> curry (λ x y, Some (f x y)) x = Some (a, b)) ↔ (x.1 = a ∧ f (x.1) (x.2) = b)).
@@ -77,9 +77,9 @@ Proof.
   naive_solver.
 Qed.
 
-Lemma dom_to_gmap `{Countable K} {B} (g : gset K) (b:B) : dom (gset K) (to_gmap b g) ≡ g.
+Lemma dom_gset_to_gmap `{Countable K} {B} (g : gset K) (b:B) : dom (gset K) (gset_to_gmap b g) ≡ g.
 Proof.
-  rewrite /to_gmap dom_fmap => ?. rewrite elem_of_dom.
+  rewrite /gset_to_gmap dom_fmap => ?. rewrite elem_of_dom.
   split.
   - move => [[] ?]. by do !red.
   - eauto.
@@ -87,7 +87,7 @@ Qed.
 
 Lemma loc_sets_dom σ : dom _ (loc_sets σ) ≡ {[ mloc m | m <- mem σ ]}.
   rewrite /loc_sets.
-  by rewrite dom_map_imap dom_to_gmap.
+  by rewrite dom_map_imap dom_gset_to_gmap.
 Qed.
 
 (* Lemma elements_map_gset `{Countable T} `{Countable B} `{Equiv B} (f : T -> B) g : *)
@@ -96,7 +96,7 @@ Qed.
 (*   rewrite /map_gset. elim: (elements g) => [|? L IHL] /=. *)
 (*   - rewrite elements_empty. constructor. *)
 (*   - rewrite elements_union.  *)
-(*     by rewrite elem_of_elements elem_of_of_list. Qed. *)
+(*     by rewrite elem_of_elements elem_of_list_to_set. Qed. *)
 
 (* Instance foldl_proper `{Equiv T} `{Equiv B} (f : B -> list T -> B) : `(Proper ((≡) ==> (≡ₚ) ==> (≡)) f) -> Proper ((≡) ==> (≡ₚ) ==> (≡)) (foldl f). *)
 (* Proof. *)
@@ -114,7 +114,7 @@ Lemma loc_sets_lookup σ l h :
   (loc_sets σ) !! l = Some h ↔ l ∈ {[ mloc m | m <- mem σ ]} ∧ h = {[ m <- msgs (mem σ) | mloc m = l ]}.
 Proof.
   rewrite /loc_sets.
-  rewrite lookup_imap lookup_to_gmap /=.
+  rewrite lookup_imap lookup_gset_to_gmap /=.
   case: (decide (l ∈ {[ mloc m | m <- mem σ ]})) => ?.
   - rewrite option_guard_True // /=. naive_solver.
   - rewrite option_guard_False // /=. naive_solver.
diff --git a/theories/examples/hashtable.v b/theories/examples/hashtable.v
index 35217eef2f5e4b162f52bf012106eb6ed74ee68a..04871bfb0ad1a6b1d20c7f2db77fa05591fdb9e3 100644
--- a/theories/examples/hashtable.v
+++ b/theories/examples/hashtable.v
@@ -1694,7 +1694,7 @@ Section proof.
     Permutation (map_to_list (m1 ∪ m2)) (map_to_list m1 ++ map_to_list m2).
   Proof.
     intro Hdisj.
-    rewrite -(map_of_to_list m1) -foldr_insert_union.
+    rewrite -(list_to_map_to_list m1) -foldr_insert_union.
     pose proof (NoDup_fst_map_to_list m1) as HNoDup.
     remember (map_to_list m1) as l1.
     assert (Permutation (map_to_list m1) l1) as Hl1 by (rewrite Heql1; done).
@@ -1703,10 +1703,10 @@ Section proof.
     pose proof (map_to_list_insert_inv _ _ _ _ Hl1); subst; simpl.
     inversion HNoDup as [|??? HNoDup']; subst.
     apply map_disjoint_insert_l in Hdisj as [].
-    pose proof (not_elem_of_map_of_list_1 _ _ H1).
+    pose proof (not_elem_of_list_to_map_1 _ _ H1).
     rewrite !map_to_list_insert; auto.
-    constructor; apply (IHl1 HNoDup' (map_of_list l1)); try done.
-    { rewrite map_to_of_list; done. }
+    constructor; apply (IHl1 HNoDup' (list_to_map l1)); try done.
+    { rewrite map_to_list_to_map; done. }
     { rewrite foldr_insert_union lookup_union_None; auto. }
   Qed.
 
diff --git a/theories/examples/kvnode.v b/theories/examples/kvnode.v
index 251dd9037f54170e82655d119ef260211a8f6b75..bc0be50156ed659da1cee756feea8d0137785daf 100644
--- a/theories/examples/kvnode.v
+++ b/theories/examples/kvnode.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 From igps Require Export malloc repeat notation escrows.
 From igps Require Import persistor viewpred proofmode weakestpre protocols singlewriter logically_atomic
   invariants fork.
-From igps.gps Require Import shared plain recursive.
+From igps.gps Require Import shared plain.
 From igps.examples Require Import abs_hashtable snapshot hist_protocol repeat for_loop list_lemmas.
 Require Recdef.
 
@@ -186,7 +186,7 @@ Section proof.
 
   Set Default Proof Using "Type".
 
-  (* The collection of protocol assertions that describes a stable state of the node. *)
+  (* The set of protocol assertions that describes a stable state of the node. *)
   Definition node_state_R L v n g :=
     (⌜map_size L 8 /\ exists vs, log_latest L v vs⌝ ∗
      [XP (ZplusPos version n) in v | versionP n g]_R ∗ ⎡@own _ _ histG g (Snapshot L)⎤ ∗
@@ -468,7 +468,6 @@ Section proof.
   Proof.
     iIntros "(#kI & out & #node_state)" (Φ) "shift"; iDestruct "shift" as (P) "[HP #Hshift]".
     match goal with |-context[(▷ P ={_,_}=∗ ?R)%I] => set (Q := R) end.
-
     unfold read.
     unfold of_val.
     wp_rec'. wp_rec'.
@@ -848,7 +847,7 @@ Section proof.
   Lemma writer_spec n L v g N (HN : base_mask ## ↑N):
     {{{ ⎡PSCtx⎤ ∗ node_state_W L v n g ∗ inv N (∃ L, ⎡own g (Master (1/2) L)⎤) }}} writer #n
     {{{ RET #();
-        let L' := map_of_list (rev (map (fun i => ((v + (2 * (i + 1)))%nat, replicate 8 (i + 1))) (seq 0 3))) ∪ L in 
+        let L' := list_to_map (rev (map (fun i => ((v + (2 * (i + 1)))%nat, replicate 8 (i + 1))) (seq 0 3))) ∪ L in 
           node_state_W L' (v + 6) n g }}}.
   Proof.
     intros; iIntros "(#kI & node_state & #I) Hpost".
@@ -893,7 +892,7 @@ Section proof.
     iApply (wp_for_simple with "[] [node_state data]").
     - apply I.
     - instantiate (1 := (fun i => ⌜0 <= i <= 3⌝ ∗ ([∗ list] j ∈ seq 0 8, (ZplusPos (Z.of_nat j) l ↦ i)) ∗
-        let L' := map_of_list (rev (map (fun i => ((v + (2 * (i + 1)))%nat, replicate 8 (i + 1))) (seq 0 (Z.to_nat i))))
+        let L' := list_to_map (rev (map (fun i => ((v + (2 * (i + 1)))%nat, replicate 8 (i + 1))) (seq 0 (Z.to_nat i))))
         ∪ L in node_state_W L' (v + (2 * Z.to_nat i)) n g)%I).
       iIntros "!#" (i ?) "!# (% & % & data & node_state) Hpost".
       match goal with |-context[App (Rec _ ?b ?e) _] => assert (Closed (b :b: nil) e) as Hclosed by apply I end.
@@ -944,11 +943,10 @@ Section proof.
         iDestruct "H" as (?) "(% & ? & ?)"; subst.
         rewrite big_sepL_replicate; iFrame.
         rewrite Z2Nat.inj_add; try omega.
-        rewrite Nat.add_1_r seq_S List.map_app rev_app_distr; simpl.
-        rewrite Z2Nat.id; last omega.
+        rewrite Nat.add_1_r seq_S List.map_app rev_app_distr.
+        rewrite /= Z2Nat.id; last omega.
         by rewrite -(Nat.add_1_r (Z.to_nat i)) !Nat.mul_add_distr_l -!plus_assoc insert_union_l.
-    - simpl; change (seq 0 (Z.to_nat 0)) with (@nil nat); simpl.
-      rewrite left_id Nat.add_0_r; iFrame; auto.
+    - rewrite /= left_id Nat.add_0_r; iFrame; auto.
     - iNext; iIntros "H"; iDestruct "H" as (i) "(% & % & data & node_state)".
       assert (i = 3) by omega; subst.
       by iApply "Hpost".
diff --git a/theories/examples/kvnode2.v b/theories/examples/kvnode2.v
index df0b36ec7d7d743930f6d17ff02eddc40ba0c863..902d90abfefcc8a50a64a3106ecfbae5f8515efc 100644
--- a/theories/examples/kvnode2.v
+++ b/theories/examples/kvnode2.v
@@ -309,7 +309,7 @@ Section proof.
     - rewrite lookup_insert_ne; last done.
       rewrite Hin.
       split; intros []; split; auto; try omega.
-      destruct (decide (n' = n + 1)%nat); last omega.
+      destruct (decide (n' = n + 1)%nat); last lia.
       subst; rewrite Nat.even_add Heven in H; done.
   Qed.
 
@@ -320,11 +320,11 @@ Section proof.
       intros; destruct (decide (n' = O)).
       + subst; rewrite lookup_insert; split; eauto.
       + rewrite lookup_insert_ne; last done.
-        rewrite lookup_empty; split; intros []; [done | omega].
+        rewrite lookup_empty; split; intros []; [done | lia].
     - assert (n = (n - 2) + 2)%nat as Heq.
       { rewrite Nat.sub_add; first done.
         destruct n; first done.
-        destruct n; [done | omega]. }
+        destruct n; [done | lia]. }
       rewrite {1 3}Heq.
       eapply log_latest_insert, IHg.
       rewrite Heq Nat.even_add in H.
@@ -366,7 +366,7 @@ Section proof.
     destruct (decide (i < length l)); [rewrite app_nth1 | rewrite app_nth2]; try omega;
       destruct (decide _); auto; try omega.
     - subst; rewrite minus_diag; auto.
-    - rewrite !nth_overflow; auto; simpl; omega.
+    - rewrite !nth_overflow; auto; simpl; lia.
   Qed.
 
   Lemma map_nth_app {A} m1 n m2 i (d : A) (Hm1: map_size m1 n)
@@ -393,7 +393,7 @@ Section proof.
   Proof.
     intros; induction vals using rev_ind; simpl; iIntros "H".
     { iExists (make_log v nil); iFrame; iPureIntro.
-      split; last by (split; [apply make_log_latest | intros; omega]).
+      split; last by (split; [apply make_log_latest | intros; lia]).
       intros ???%make_log_lookup; subst; auto. }
     rewrite big_sepL_app; simpl.
     iDestruct "H" as "(H & Hi & _)".
@@ -419,7 +419,7 @@ Section proof.
         intros; erewrite map_nth_app; eauto.
         rewrite Nat.add_0_r in H4.
         destruct (decide _); first by subst.
-        apply H2; omega.
+        apply H2; lia.
     - rewrite big_sepL_app; simpl.
       erewrite Nat.add_0_r, map_nth_app; eauto.
       rewrite decide_True; last done; iFrame.
diff --git a/theories/examples/nat_tokens.v b/theories/examples/nat_tokens.v
index c3611e7898620cfd9a5e839341a090039c9c59c8..eb7a4109783ee578435e21d8fc096ee81fe02fea 100644
--- a/theories/examples/nat_tokens.v
+++ b/theories/examples/nat_tokens.v
@@ -8,24 +8,24 @@ From igps Require Import arith infrastructure.
 Definition Pos_upto_set (up: nat) : gset positive :=
   match up with
   | O => ∅
-  | S i => map_gset Pos.of_nat (seq_set 1 up)
+  | S i => map_gset Pos.of_nat (set_seq 1 up)
   end.
 
 Definition coPset_from_ex (i: nat): coPset
-  := ⊤ ∖  coPset.of_gset (Pos_upto_set i).
+  := ⊤ ∖  gset_to_coPset (Pos_upto_set i).
 
 Lemma coPset_from_ex_gt i p:
   p ∈ coPset_from_ex i ↔ (i < Pos.to_nat p)%nat.
 Proof.
-  rewrite elem_of_difference coPset.elem_of_of_gset.
+  rewrite elem_of_difference elem_of_gset_to_coPset.
   destruct i as [|i].
   - split; move => _; [by apply Pos2Nat.is_pos|done].
   - rewrite elem_of_map_gset. split.
     + move => [_ /= NIn].
       apply: not_ge => ?. apply: NIn.
-      exists (Pos.to_nat p). set_unfold; rewrite elem_of_seq_set. lia'.
+      exists (Pos.to_nat p). set_unfold. lia'.
     + move => Lt. split; first done.
-      move => [n [Eqn /elem_of_seq_set [Ge1 Lt2]]].
+      move => [n [Eqn /elem_of_set_seq [Ge1 Lt2]]].
       subst. lia'.
 Qed.
 
@@ -43,25 +43,25 @@ Qed.
 
 
 Lemma coPset_of_gset_union X Y :
-  coPset.of_gset (X ∪ Y) = coPset.of_gset X ∪ coPset.of_gset Y.
+  gset_to_coPset (X ∪ Y) = gset_to_coPset X ∪ gset_to_coPset Y.
 Proof.
   apply leibniz_equiv.
-  move => ?. by rewrite elem_of_union !coPset.elem_of_of_gset elem_of_union.
+  move => ?. by rewrite elem_of_union !elem_of_gset_to_coPset elem_of_union.
 Qed.
 
 Lemma coPset_of_gset_difference X Y:
-  coPset.of_gset (X ∖ Y) = coPset.of_gset X ∖ coPset.of_gset Y.
+  gset_to_coPset (X ∖ Y) = gset_to_coPset X ∖ gset_to_coPset Y.
 Proof.
   apply leibniz_equiv. move => x.
-  by rewrite elem_of_difference !coPset.elem_of_of_gset elem_of_difference.
+  by rewrite elem_of_difference !elem_of_gset_to_coPset elem_of_difference.
 Qed.
 
 Lemma coPset_of_gset_difference_union (X Y Z: gset positive)
   (Disj: Y ## Z) (Sub: Y ⊆ X):
-  coPset.of_gset (X ∖ Z) = coPset.of_gset (X ∖ (Y ∪ Z)) ∪ coPset.of_gset Y.
+  gset_to_coPset (X ∖ Z) = gset_to_coPset (X ∖ (Y ∪ Z)) ∪ gset_to_coPset Y.
 Proof.
   apply leibniz_equiv. move => x.
-  rewrite elem_of_union !coPset.elem_of_of_gset
+  rewrite elem_of_union !elem_of_gset_to_coPset
           !elem_of_difference elem_of_union.
   split.
   - move => [InX NIn]. case (decide (x ∈ Y)) => [?|NInY].
@@ -71,33 +71,33 @@ Proof.
 Qed.
 
 Lemma coPset_of_gset_difference_disjoint (X Y Z: gset positive):
-  coPset.of_gset (X ∖ (Y ∪ Z)) ## coPset.of_gset Y.
+  gset_to_coPset (X ∖ (Y ∪ Z)) ## gset_to_coPset Y.
 Proof.
   rewrite elem_of_disjoint.
-  move => x. rewrite !coPset.elem_of_of_gset elem_of_difference elem_of_union.
+  move => x. rewrite !elem_of_gset_to_coPset elem_of_difference elem_of_union.
   set_solver.
 Qed.
 
 Lemma coPset_of_gset_top_difference (X Y: gset positive) (Disj: X ## Y):
-  ⊤ ∖  coPset.of_gset X = (⊤ ∖  coPset.of_gset (Y ∪ X)) ∪ coPset.of_gset Y.
+  ⊤ ∖  gset_to_coPset X = (⊤ ∖  gset_to_coPset (Y ∪ X)) ∪ gset_to_coPset Y.
 Proof.
   apply leibniz_equiv. move => x.
   rewrite elem_of_union !elem_of_difference
-          !coPset.elem_of_of_gset elem_of_union.
+          !elem_of_gset_to_coPset elem_of_union.
   split.
   - move => [_ NIn]. case (decide (x ∈ Y)) => [|?]; [by right|left]. set_solver.
   - set_solver.
 Qed.
 
 Lemma coPset_of_gset_top_disjoint (X Y: gset positive):
-  (⊤ ∖  coPset.of_gset (Y ∪ X)) ## coPset.of_gset Y.
+  (⊤ ∖  gset_to_coPset (Y ∪ X)) ## gset_to_coPset Y.
 Proof.
   rewrite elem_of_disjoint.
   move => x. rewrite elem_of_difference coPset_of_gset_union. set_solver.
 Qed.
 
 Lemma coPset_of_gset_empty :
-  coPset.of_gset ∅ = ∅.
+  gset_to_coPset ∅ = ∅.
 Proof. by apply leibniz_equiv. Qed.
 
 Lemma coPset_difference_top_empty:
diff --git a/theories/examples/rcu_data.v b/theories/examples/rcu_data.v
index 071c36c3dd397322a9e77b3ed959931c2d377eac..36637cfa9afa3016fca3adce8eb0321dbb58ebf8 100644
--- a/theories/examples/rcu_data.v
+++ b/theories/examples/rcu_data.v
@@ -44,13 +44,13 @@ Section RCUData.
   Definition hist D i := hist' (D.1) i.
   Definition info' M i : list (loc * gname)
     := ((λ p, (p.1.2, p.2)) <$> {[p <- M | p.1.1 = i]}).
-  Definition infos D i : gset (loc * gname) := of_list (info' (D.2) i).
+  Definition infos D i : gset (loc * gname) := list_to_set (info' (D.2) i).
   Definition info D i : option (loc * gname) := hd_error (info' (D.2) i).
 
   Global Instance RCUInfo_dom : Dom RCUInfo (gset aloc)
-    := λ M, of_list (fst ∘ fst <$> M).
+    := λ M, list_to_set (fst ∘ fst <$> M).
   Global Instance RCUHist_dom : Dom RCUHist (gset aloc)
-    := λ H, of_list (fst <$> H).
+    := λ H, list_to_set (fst <$> H).
   Global Instance RCUData_dom : Dom RCUData (gset aloc)
     := λ D, dom _ (D.1).
 
@@ -70,14 +70,14 @@ Section RCUData.
   Qed.
 
   Definition basel' H : list aloc :=  {[ i <- (fst <$> H) | is_base H i]}.
-  Definition base' H : gset aloc := of_list (basel' H).
+  Definition base' H : gset aloc := list_to_set (basel' H).
   Definition basel D := basel' (D.1).
   Definition base D := base' (D.1).
 
   Lemma rcu_base_live b D:
     b ∈ base D → b ∈ live D.
   Proof.
-    rewrite /base /base' elem_of_of_list /basel' elem_of_list_filter.
+    rewrite /base /base' elem_of_list_to_set /basel' elem_of_list_filter.
     by move => [[? ?] ?].
   Qed.
 
@@ -120,7 +120,7 @@ Section RCUData.
     dom (gset loc) H1 ⊆ dom _ H2.
   Proof.
     move => ?.
-    rewrite !elem_of_of_list !elem_of_list_fmap.
+    rewrite !elem_of_list_to_set !elem_of_list_fmap.
     move => [b [? In]]. exists b. split; first auto.
     by eapply elem_of_suffix.
   Qed.
@@ -135,7 +135,7 @@ Section RCUData.
   Lemma RCUInfo_ext_dom: ∀ M1 M2, M1 ⊑ M2 → dom (gset loc) M1 ⊆ dom _ M2.
   Proof.
     move => ????.
-    rewrite !elem_of_of_list !elem_of_list_fmap.
+    rewrite !elem_of_list_to_set !elem_of_list_fmap.
     move => [b [??]]. exists b. split; first auto.
     by eapply elem_of_suffix.
   Qed.
@@ -217,12 +217,12 @@ Section RCUData.
 
   Lemma elem_of_rcu_infos D i p:
     p ∈ infos D i ↔ (i,p.1,p.2) ∈ D.2.
-  Proof. by rewrite elem_of_of_list elem_of_rcu_info'. Qed.
+  Proof. by rewrite elem_of_list_to_set elem_of_rcu_info'. Qed.
 
   Lemma rcu_dom'_cons H i b :
     dom (gset loc) ((i,b)::H) ≡ {[i]} ∪ dom (gset _) H.
   Proof.
-    rewrite /= /RCUHist_dom => x. by rewrite elem_of_of_list fmap_cons.
+    rewrite /= /RCUHist_dom => x. by rewrite elem_of_list_to_set fmap_cons.
   Qed.
 
   Lemma rcu_dom'_cons_in H i b (In: i ∈ dom (gset _) H):
@@ -232,7 +232,7 @@ Section RCUData.
   Lemma elem_of_rcu_info_dom M i:
     i ∈ dom (gset _) M ↔ ∃ l γ, (i,l,γ) ∈ M.
   Proof.
-    rewrite /= /RCUInfo_dom elem_of_of_list elem_of_list_fmap. split.
+    rewrite /= /RCUInfo_dom elem_of_list_to_set elem_of_list_fmap. split.
     - move => [[[??]?] [/= -> ?]]. by do 2 eexists.
     - move => [l [γ ?]]. by exists (i,l,γ).
   Qed.
@@ -240,7 +240,7 @@ Section RCUData.
   Lemma elem_of_rcu_hist_dom H i:
     i ∈ dom (gset _) H ↔ ∃ b, b ∈ hist' H i.
   Proof.
-    rewrite /= /RCUHist_dom /hist' elem_of_of_list elem_of_list_fmap.
+    rewrite /= /RCUHist_dom /hist' elem_of_list_to_set elem_of_list_fmap.
     setoid_rewrite elem_of_list_fmap.
     setoid_rewrite elem_of_list_filter.
     split.
@@ -251,7 +251,7 @@ Section RCUData.
   Lemma elem_of_rcu_hist_dom_2 H i:
     i ∈ dom (gset _) H ↔ ∃ y, i = y.1 ∧ y ∈ H.
   Proof.
-    by rewrite /= /RCUHist_dom /hist' elem_of_of_list elem_of_list_fmap.
+    by rewrite /= /RCUHist_dom /hist' elem_of_list_to_set elem_of_list_fmap.
   Qed.
 
   Lemma elem_of_rcu_hist'_mono H1 H2 i:
@@ -263,7 +263,7 @@ Section RCUData.
   Lemma elem_of_rcu_hist_dom_mono H1 H2:
     dom (gset loc) H2 ⊆ dom (gset _) (H1 ++ H2)%list.
   Proof.
-    move => b. rewrite /= /RCUHist_dom 2!elem_of_of_list fmap_app elem_of_app.
+    move => b. rewrite /= /RCUHist_dom 2!elem_of_list_to_set fmap_app elem_of_app.
     by right.
   Qed.
 
@@ -303,7 +303,7 @@ Section RCUData.
     - move => NIn. apply elem_of_nil_inv. move => x In2.
       apply NIn, elem_of_rcu_hist_dom. by exists x.
     - rewrite /= /RCUHist_dom. move => /fmap_nil_inv EqN.
-      rewrite elem_of_of_list elem_of_list_fmap.
+      rewrite elem_of_list_to_set elem_of_list_fmap.
       move => [y [Eq In]]. apply (elem_of_nil y).
       by rewrite -EqN elem_of_list_filter.
   Qed.
@@ -317,7 +317,7 @@ Section RCUData.
   Proof.
     move => i.
     rewrite /dead' !elem_of_filter /= /RCUHist_dom /hist'
-            !elem_of_of_list filter_app !fmap_app !elem_of_app.
+            !elem_of_list_to_set filter_app !fmap_app !elem_of_app.
     move => [? ?]. split; by [left|right].
   Qed.
 
@@ -351,7 +351,7 @@ Section RCUData.
   Proof.
     rewrite /live' /= /RCUHist_dom !elem_of_difference.
     move => [In NIn]. split.
-    - move : In. rewrite 2!elem_of_of_list fmap_app elem_of_app. by right.
+    - move : In. rewrite 2!elem_of_list_to_set fmap_app elem_of_app. by right.
     - move : NIn. rewrite /dead'.
       rewrite !elem_of_filter /hist' filter_app fmap_app elem_of_app.
       move => NIn [[HD|HD] _].
@@ -365,7 +365,7 @@ Section RCUData.
     i ∈ live' H2 ↔ i ∈ live' (H1++H2)%list.
   Proof.
     rewrite /live' /dead'/= /RCUHist_dom !elem_of_difference !elem_of_filter
-            !elem_of_of_list /hist' filter_app 2!fmap_app 2!elem_of_app.
+            !elem_of_list_to_set /hist' filter_app 2!fmap_app 2!elem_of_app.
     split.
     - move => [In NIn]. split; first by right.
       move => [HD [In'|In']].
@@ -418,7 +418,7 @@ Section RCUData.
     dom (gset loc) (H1 ++ H2)%list ≡ dom (gset _) H1 ∪ dom (gset _) H2.
   Proof.
     move => i. by rewrite /= /RCUHist_dom elem_of_union
-                          !elem_of_of_list fmap_app elem_of_app.
+                          !elem_of_list_to_set fmap_app elem_of_app.
   Qed.
 
   Lemma rcu_hist_dom_cons i b H:
@@ -430,7 +430,7 @@ Section RCUData.
   Proof.
     move => i.
     by rewrite /= /RCUInfo_dom elem_of_union
-               !elem_of_of_list fmap_app elem_of_app.
+               !elem_of_list_to_set fmap_app elem_of_app.
   Qed.
 
   Lemma rcu_info_dom_cons i x γ M:
@@ -462,7 +462,7 @@ Section RCUData.
                   ∃ j, (j, Abs (p.1)) ∈ H1) :
     base' H2 ≡ base' (H1 ++ H2)%list.
   Proof.
-    move => i. rewrite /base' !elem_of_of_list /basel' !elem_of_list_filter.
+    move => i. rewrite /base' !elem_of_list_to_set /basel' !elem_of_list_filter.
     split; move => [IB Ini].
     - rewrite fmap_app elem_of_app.
       split; last by right. split.
@@ -481,7 +481,7 @@ Section RCUData.
         move => [|//]. rewrite elem_of_list_fmap.
         move => [y [Eqi Iny]]. exfalso.
         destruct (NoAdd _ Iny) as [j Inj].
-        - rewrite -Eqi. by rewrite /= /RCUHist_dom elem_of_of_list.
+        - rewrite -Eqi. by rewrite /= /RCUHist_dom elem_of_list_to_set.
         - assert (Abs i ∈ hist' H1 j).
           { rewrite Eqi elem_of_list_fmap. exists (j, Abs (y.1)).
             by rewrite elem_of_list_filter. }
@@ -491,7 +491,7 @@ Section RCUData.
           + rewrite rcu_hist'_app elem_of_app. by left. }
       split; last auto; split.
       + apply (elem_of_rcu_live'_mono2 _ H1).
-        * by rewrite /= /RCUHist_dom elem_of_of_list.
+        * by rewrite /= /RCUHist_dom elem_of_list_to_set.
         * by destruct IB.
       + destruct IB as [? IB].
         move => i' InD Ina. apply (IB i').
@@ -781,13 +781,13 @@ Section RCUData.
     - left. split; first by left.
       move: W1 => [_ [EqD _]]. rewrite EqN in EqD.
       move: EqD. rewrite /= /RCUHist_dom /=. rewrite /RCUInfo_dom /=.
-      move => EqD. symmetry in EqD. apply of_list_nil_eq, fmap_nil_inv in EqD.
+      move => EqD. symmetry in EqD. apply list_to_set_nil_eq, fmap_nil_inv in EqD.
       rewrite EqD. apply suffix_nil.
     - destruct Le2 as [EqN|?].
       + right. split; first by left.
       move: W2 => [_ [EqD _]]. rewrite EqN in EqD.
       move: EqD. rewrite /= /RCUHist_dom /=. rewrite /RCUInfo_dom /=.
-      move => EqD. symmetry in EqD. apply of_list_nil_eq, fmap_nil_inv in EqD.
+      move => EqD. symmetry in EqD. apply list_to_set_nil_eq, fmap_nil_inv in EqD.
       rewrite EqD. apply suffix_nil.
       + apply (RCUData_ext_share_total_1 _ _ D3 W1 W2); by intuition.
   Qed.
@@ -825,7 +825,7 @@ Section RCUData.
             /(elem_of_suffix _ _(RCUData_info_suffix _ _ _ Dle2)).
     move: W2 => [-> /elem_of_nil //|[_ [_ [/(_ i) W2 _]]]] In.
     assert (Len: length (info' (D2.2) i) = 1%nat).
-      { apply W2. rewrite /= /RCUInfo_dom elem_of_of_list elem_of_list_fmap.
+      { apply W2. rewrite /= /RCUInfo_dom elem_of_list_to_set elem_of_list_fmap.
         apply elem_of_rcu_info' in In. by exists (i, p.1, p.2). }
     rewrite /info. move: In.
     case (info' (D2.2) i) as [|p' L']
@@ -947,7 +947,7 @@ Section RCUData.
           apply (is_fresh (dom (gset aloc) D)).
           destruct W as (_ & W & _).
           rewrite {2}/dom /RCUData_dom W.
-          rewrite /= /RCUInfo_dom elem_of_of_list elem_of_list_fmap.
+          rewrite /= /RCUInfo_dom elem_of_list_to_set elem_of_list_fmap.
           exists a. by rewrite -/j -Eqj.
         * rewrite /info' list_filter_cons_not; first by apply W.
           move => ?. subst i'. move : In.
@@ -980,7 +980,7 @@ Section RCUData.
       + move => k Ink.
         assert (j ∈ live' (D'.1)).
         { apply elem_of_difference. split.
-          - apply elem_of_of_list, elem_of_list_fmap. exists (j,Null).
+          - apply elem_of_list_to_set, elem_of_list_fmap. exists (j,Null).
             split; first auto. right. left.
           - move => /elem_of_filter [HD _].
             apply elem_of_rcu_hist'_further in HD; last auto.
@@ -1144,7 +1144,7 @@ Section RCUData.
           apply (is_fresh (dom (gset aloc) D)).
           destruct W as (_ & W & _).
           rewrite {2}/dom /RCUData_dom W.
-          rewrite /= /RCUInfo_dom elem_of_of_list elem_of_list_fmap.
+          rewrite /= /RCUInfo_dom elem_of_list_to_set elem_of_list_fmap.
           exists a. by rewrite -/j0 -Eqj.
         * rewrite /info' list_filter_cons_not; first by apply W.
           move => ?. subst i'. move : In.
@@ -1197,7 +1197,7 @@ Section RCUData.
       + move => k Ink.
         assert (j0 ∈ live' (D'.1)).
         { apply elem_of_difference. split.
-          - apply elem_of_of_list, elem_of_list_fmap. exists (j0, bj).
+          - apply elem_of_list_to_set, elem_of_list_fmap. exists (j0, bj).
             split; first auto. right. left.
           - move => /elem_of_filter [HD _].
             apply elem_of_rcu_hist'_further in HD; last auto.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 82edca1129264559218a0dd87a50acc94ec7abc5..5c281070897dd4ea9b465803ae0793ce330f7c69 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -212,14 +212,14 @@ Section TicketLock.
     Qed.
 
     Lemma Waiting_dom_size (M: gmapNOpN)
-      (DS : dom (gset nat) M ≡ seq_set 0 (Pos.to_nat C)):
+      (DS : dom (gset nat) M ≡ set_seq 0 (Pos.to_nat C)):
       Z.pos C = size (dom (gset nat) M).
     Proof.
-      by rewrite (collection_size_proper _ _ DS) -positive_nat_Z seq_set_size.
+      by rewrite (set_size_proper _ _ DS) -positive_nat_Z set_seq_size.
     Qed.
 
     Lemma Waiting_size_le (M: gmapNOpN) (n: nat)
-      (DS: dom (gset nat) M ≡ seq_set 0 (Pos.to_nat C)):
+      (DS: dom (gset nat) M ≡ set_seq 0 (Pos.to_nat C)):
       Ws M n ≤ Z.pos C.
     Proof.
       rewrite (_: Z.pos C = size (dom (gset nat) M)).
@@ -228,7 +228,7 @@ Section TicketLock.
     Qed.
 
     Lemma Waiting_size_lt (M: gmapNOpN) (n i: nat) (ot: option nat)
-      (DS: dom (gset nat) M ≡ seq_set 0 (Pos.to_nat C))
+      (DS: dom (gset nat) M ≡ set_seq 0 (Pos.to_nat C))
       (Ini: M !! i = Excl' ot) (Lt: ot = None ∨ ∃ t, ot = Some t ∧ t < n):
       Ws M n < Z.pos C.
     Proof.
@@ -266,7 +266,7 @@ Section TicketLock.
 
     Lemma ns_tkt_bound_update (M: gmapNOpN) (t n i: nat) (ot : option nat)
       (Ini: M !! i = Excl' ot) (BO: ns_tkt_bound M t n)
-      (DS: dom (gset nat) M ≡ seq_set 0 (Pos.to_nat C)):
+      (DS: dom (gset nat) M ≡ set_seq 0 (Pos.to_nat C)):
       ∃ (n': nat),
         (ot = None → n' = n) ∧
         (∀ t0, ot = Some t0 → n' = S t0 ∨ n' = n) ∧ t < n' + Z.pos C
@@ -286,7 +286,7 @@ Section TicketLock.
             apply Zplus_le_compat_r. etrans; first apply LE2.
             assert (Eqs :=
             subseteq_union_1 _ _ (Waiting_subseteq_update _ _ t _ _ Ini Le)).
-            rewrite /Ws -(collection_size_proper _ _ Eqs) size_union_alt.
+            rewrite /Ws -(set_size_proper _ _ Eqs) size_union_alt.
             rewrite Nat2Z.inj_add (Z.add_comm (size _)) Zplus_assoc.
             apply Zplus_le_compat_r. etrans.
             { instantiate (1:= n + size (Mtkt_range M n t0)).
@@ -410,21 +410,21 @@ Section TicketLock.
       apply: singleton_local_update; [eauto| exact: exclusive_local_update].
     Qed.
 
-    Definition map_excl (S: gset nat) (t : option nat) := to_gmap (Excl t) S.
-    Definition setC: gset nat := seq_set 0 (Pos.to_nat C).
+    Definition map_excl (S: gset nat) (t : option nat) := gset_to_gmap (Excl t) S.
+    Definition setC: gset nat := set_seq 0 (Pos.to_nat C).
     Definition firstMap := map_excl setC None.
 
     Lemma Tkt_set_alloc γ j n t:
-       ⎡own γ (ε, ◯ map_excl (seq_set j n) t)⎤
-       ⊢ ([∗ set] i ∈ seq_set j n, MyTkt γ i t)%I.
+       ⎡own γ (ε, ◯ map_excl (set_seq j n) t)⎤
+       ⊢ ([∗ set] i ∈ set_seq j n, MyTkt γ i t)%I.
     Proof.
       revert j. induction n => j /=; iIntros "MyTkts".
       - by rewrite big_sepS_empty.
       - rewrite big_sepS_insert; last first.
-        { move => /elem_of_seq_set [Le _]. omega. }
-        rewrite /map_excl to_gmap_union_singleton insert_singleton_op;
+        { move => /elem_of_set_seq [Le _]. omega. }
+        rewrite /map_excl gset_to_gmap_union_singleton insert_singleton_op;
           last first.
-        { apply lookup_to_gmap_None. move => /elem_of_seq_set [Le _]. omega. }
+        { apply lookup_gset_to_gmap_None. move => /elem_of_set_seq [Le _]. omega. }
         iDestruct "MyTkts" as "[$ MyTkts]".
         by iApply IHn.
     Qed.
@@ -438,7 +438,7 @@ Section TicketLock.
         as (γ) "Own".
       { split; first done. apply auth_valid_discrete_2. split; first done.
         move => i. destruct (firstMap !! i) eqn:Eq; last by rewrite Eq.
-        rewrite Eq. by move :Eq => /lookup_to_gmap_Some [_ <-]. }
+        rewrite Eq. by move :Eq => /lookup_gset_to_gmap_Some [_ <-]. }
       iExists γ. rewrite pair_split.
       iDestruct "Own" as "[$ [$ MyTkts]]". iModIntro.
       rewrite /firstMap /setC. by iApply Tkt_set_alloc.
@@ -488,7 +488,7 @@ Section TicketLock.
       if b
       then (∃ (t n: nat) (M: gmapNOpN),
             AllTkts γ M ∗ Perms γ t
-            ∗ ⌜dom (gset nat) M ≡ seq_set 0 (Pos.to_nat C)
+            ∗ ⌜dom (gset nat) M ≡ set_seq 0 (Pos.to_nat C)
                 ∧ y = t `mod` Z.pos C ∧ ns_tkt_bound M t n⌝
             ∗ [XP (ZplusPos ns x) in n | NSP P γ ]_R)
       else True.
@@ -571,11 +571,12 @@ Section TicketLock.
         iPureIntro. split; last split.
         + rewrite /firstMap /map_excl. apply set_unfold_2. move => i.
           rewrite elem_of_dom. split.
-          * move => [e /lookup_to_gmap_Some [//]].
-          * move => In. exists (Excl None). by apply lookup_to_gmap_Some.
+          * move => [e /lookup_gset_to_gmap_Some [/elem_of_set_seq //]].
+          * move => In. exists (Excl None).
+            by rewrite lookup_gset_to_gmap_Some elem_of_set_seq.
         + by rewrite Zmod_0_l.
         + split; [done|split]; first omega.
-          move => ? ? /lookup_to_gmap_Some [_ //].
+          move => ? ? /lookup_gset_to_gmap_Some [_ //].
       }
 
       iNext. iIntros "#TCP". wp_seq.
diff --git a/theories/gps/shared.v b/theories/gps/shared.v
index 5618e16b35e9d357283ba141a4ce731e43dc1bc2..cf0c95cf15f9f02ed0feb1d4257d8ad4646de76a 100644
--- a/theories/gps/shared.v
+++ b/theories/gps/shared.v
@@ -135,10 +135,10 @@ Section Setup.
         st_time l S1 ⊑ st_time l S2 → st_prst S1 ⊑ st_prst S2.
 
     Definition Consistent ζ h : Prop :=
-      @equiv _ collection_equiv {[ (VInj (st_val e), st_view e) | e <- ζ]} h.
+      @equiv _ set_equiv {[ (VInj (st_val e), st_view e) | e <- ζ]} h.
 
     Instance Consistent_proper:
-      Proper (collection_equiv ==> collection_equiv ==> (flip impl) ) Consistent.
+      Proper (set_equiv ==> set_equiv ==> (flip impl) ) Consistent.
     Proof.
       unfold Consistent.
       move => X Y HXY h1 h2 Hh12 ?.
diff --git a/theories/gps/shared2.v b/theories/gps/shared2.v
index 6c0f1e053ea70d604682e21d5e1a5af9d02faa6a..0b3de3608483c971006ac4eb4f75ea34b8d81af5 100644
--- a/theories/gps/shared2.v
+++ b/theories/gps/shared2.v
@@ -123,10 +123,10 @@ Section Setup.
         st_time l S1 ⊑ st_time l S2 → st_prst S1 ⊑ st_prst S2.
 
     Definition Consistent ζ h : Prop :=
-      @equiv _ collection_equiv {[ (st_val e, st_view e) | e <- ζ]} h.
+      @equiv _ set_equiv {[ (st_val e, st_view e) | e <- ζ]} h.
 
     Instance Consistent_proper:
-      Proper (collection_equiv ==> collection_equiv ==> (flip impl) ) Consistent.
+      Proper (set_equiv ==> set_equiv ==> (flip impl) ) Consistent.
     Proof.
       unfold Consistent.
       move => X Y HXY h1 h2 Hh12 ?.
diff --git a/theories/history.v b/theories/history.v
index 8d2c4722cb5b405b432d2ab91da6fb12e2ffef53..8a1722b61cca0e1e72e78f8a845a6e1a84340440 100644
--- a/theories/history.v
+++ b/theories/history.v
@@ -1,5 +1,5 @@
 From Coq.ssr Require Import ssreflect.
-From stdpp Require Export strings list numbers sorting gmap finite set mapset.
+From stdpp Require Export strings list numbers sorting gmap finite propset mapset.
 
 Global Generalizable All Variables.
 Global Set Asymmetric Patterns.
diff --git a/theories/infrastructure.v b/theories/infrastructure.v
index 45c146ea479708d568e65be95f4f3d7c261bd69c..0225e86e8dc17347ded6da62913ad616577aa36e 100644
--- a/theories/infrastructure.v
+++ b/theories/infrastructure.v
@@ -1,21 +1,19 @@
 From Coq.ssr Require Export ssreflect.
-From stdpp Require Export list numbers set gmap finite mapset fin_collections.
-Global Generalizable All Variables.
-Global Set Asymmetric Patterns.
+From stdpp Require Export list numbers propset gmap finite mapset fin_sets.
 Global Set Bullet Behavior "Strict Subproofs".
 From Coq Require Export Utf8.
 Require Import Setoid.
 
 Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
 
-Lemma seq_set_size (s n: nat):  size (seq_set s n : gset nat) = n.
+Lemma set_seq_size (s n: nat):  size (set_seq s n : gset nat) = n.
 Proof.
   induction n; [done|].
-  rewrite seq_set_S_union_L /=.
+  rewrite set_seq_S_end_union_L /=.
   rewrite size_union.
     + rewrite IHn size_singleton. lia.
     + apply disjoint_singleton_l.
-      move => /elem_of_seq_set [_ ?]. omega.
+      move => /elem_of_set_seq [_ ?]. omega.
 Qed.
 
 Lemma seq_S i n : seq i (S n) = (seq i n ++ (i + n)%nat::nil)%list.
@@ -85,17 +83,17 @@ Section suffixes.
     symmetry in H1. apply app_nil in H1 as [_ ?]. by subst y1.
   Qed.
 
-  Lemma of_list_nil_eq
+  Lemma list_to_set_nil_eq
     {C : Type} `{Empty C} `{ElemOf A C} `{Singleton A C} `{Union C}
-    `{SimpleCollection A C} (l: list A):
-    of_list l ≡ (∅ : C) ↔ l = nil.
+    `{SemiSet A C} (l: list A):
+    list_to_set l ≡ (∅ : C) ↔ l = nil.
   Proof.
     split.
     - move => Eq. destruct l; first done.
-      rewrite of_list_cons in Eq. exfalso.
+      rewrite list_to_set_cons in Eq. exfalso.
       apply empty_union in Eq as [Eq _].
       eapply not_elem_of_empty. rewrite -Eq elem_of_singleton. done.
-    - move => ->. by rewrite of_list_nil.
+    - move => ->. by rewrite list_to_set_nil.
   Qed.
 
   Lemma hd_error_some_elem a l :
@@ -144,7 +142,7 @@ Section suffixes.
 End suffixes.
 
 Section Max.
-  Context {A C : Type} `{Collection A C}.
+  Context {A C : Type} `{Set_ A C}.
 
   Inductive Max (R : relation A) (c : C) : Type :=
   | max_none (HEmp : c ≡ ∅)
@@ -242,7 +240,7 @@ Proof. set_solver. Qed.
 
 (* Extra lemmas for set difference *)
 
-Lemma difference_mono `{Collection A C}:
+Lemma difference_mono `{Set_ A C}:
   Proper ((⊆) ==> (≡) ==> (⊆)) (@difference C _).
 Proof.
   intros X1 X2 HX Y1 Y2 HY. rewrite HY.
@@ -260,7 +258,7 @@ Lemma gset_difference_mono `{Countable A} (X Y Z: gset A):
   X ⊆ Y → X ∖ Z ⊆ Y ∖ Z.
 Proof. intro Sub. by apply (difference_mono). Qed.
 
-Lemma difference_twice_union `{Collection A C} (X Y Z: C):
+Lemma difference_twice_union `{Set_ A C} (X Y Z: C):
   (X ∖ Y ∖ Z ≡ X ∖ (Y ∪ Z))%stdpp.
 Proof.
   apply elem_of_equiv. move => ?.
@@ -330,12 +328,12 @@ Section Map_GSet.
            {CB : @Countable B EqDecB}.
   Set Default Proof Using "Type* EqDecA EqDecB CA CB".
   Definition map_gset f (M : gset A) : gset B
-    := of_list (f <$> (elements M)).
+    := list_to_set (f <$> (elements M)).
   Typeclasses Opaque map_gset.
 
   Lemma elem_of_map_gset f M b : b ∈ map_gset f M ↔ ∃ a, b = f a ∧ a ∈ M.
   Proof.
-    rewrite elem_of_of_list elem_of_list_fmap.
+    rewrite elem_of_list_to_set elem_of_list_fmap.
       by setoid_rewrite elem_of_elements.
   Qed.
   Global Instance set_unfold_map_gset f M b Q :
@@ -812,7 +810,7 @@ Lemma gset_neg_Forall `{Countable A} (P : A -> Prop)
   : ¬ set_Forall P s ↔ set_Exists (λ x, ¬ P x) s.
 Proof.
   split.
-  - case: (collection_choose_or_empty (filter (λ x, ¬ P x) s)) => [[x]|].
+  - case: (set_choose_or_empty (filter (λ x, ¬ P x) s)) => [[x]|].
     + set_unfold => [[? ?]] _. by exists x.
     + set_unfold => H2 H3. exfalso. apply: H3 => x Inx.
       specialize (H2 x).
@@ -976,8 +974,8 @@ Proof.
   move => m'. case (decide (m = m')) => [-> //|]. abstract set_solver+SR.
 Qed.
 
-Instance gset_SimpleCollection `{Countable K} : SimpleCollection K (gset K) := _.
-Instance gset_Collection `{Countable K} : Collection K (gset K) := _.
+Instance gset_SemiSet `{Countable K} : SemiSet K (gset K) := _.
+Instance gset_Set_ `{Countable K} : Set_ K (gset K) := _.
 
 
 Program Definition Pos2Qp (n: positive) : Qp := mk_Qp (Zpos n) _.
diff --git a/theories/rsl_sts.v b/theories/rsl_sts.v
index 1ea5177579d80ed8ef40a9bb238418a0cff8116c..ecc099a3661d135fa340322ef1a0597ab943e754 100644
--- a/theories/rsl_sts.v
+++ b/theories/rsl_sts.v
@@ -65,7 +65,7 @@ Lemma rISet2_subseteq s:
   rISet2 s ⊆ rISet s.
 Proof. by destruct s. Qed.
 
-Definition tok s: set token
+Definition tok s: propset token
   := {[ t | ∃ i, t = Change i ∧ i ∉ rISet2 s ]}.
 
 Global Arguments tok !_ /.
@@ -73,7 +73,7 @@ Global Arguments tok !_ /.
 Canonical Structure rsl_sts := sts.Sts prim_step tok.
 
 
-Definition i_states i : set state := {[ s | i ∈ rISet2 s ]}.
+Definition i_states i : propset state := {[ s | i ∈ rISet2 s ]}.
 
 
 Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.