diff --git a/_CoqProject b/_CoqProject
index 735493d4ae89550563ae2cfcccbfb603d417f04d..6e7e43577c09648ade870d5a63c72b9ece87bfca 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,13 +3,13 @@ theories/base.v
 theories/tactics.v
 theories/option.v
 theories/fin_map_dom.v
-theories/bset.v
+theories/boolset.v
 theories/fin_maps.v
 theories/fin.v
 theories/vector.v
 theories/pmap.v
 theories/stringmap.v
-theories/fin_collections.v
+theories/fin_sets.v
 theories/mapset.v
 theories/proof_irrel.v
 theories/hashset.v
@@ -19,7 +19,7 @@ theories/orders.v
 theories/natmap.v
 theories/strings.v
 theories/relations.v
-theories/collections.v
+theories/sets.v
 theories/listset.v
 theories/streams.v
 theories/gmap.v
@@ -32,7 +32,7 @@ theories/nmap.v
 theories/zmap.v
 theories/coPset.v
 theories/lexico.v
-theories/set.v
+theories/propset.v
 theories/decidable.v
 theories/list.v
 theories/functions.v
diff --git a/theories/base.v b/theories/base.v
index c16f05c9f26c79eb09d32b6a35545de874b61684..e0034cc2e96d56e1359eeed9b65ed19151e7831e 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects type class interfaces, notations, and general theorems
 that are used throughout the whole development. Most importantly it contains
-abstract interfaces for ordered structures, collections, and various other data
+abstract interfaces for ordered structures, sets, and various other data
 structures. *)
 
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
@@ -753,9 +753,9 @@ End sig_map.
 Arguments sig_map _ _ _ _ _ _ !_ / : assert.
 
 
-(** * Operations on collections *)
+(** * Operations on sets *)
 (** We define operational type classes for the traditional operations and
-relations on collections: the empty collection [∅], the union [(∪)],
+relations on sets: the empty set [∅], the union [(∪)],
 intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 [(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
 Class Empty A := empty: A.
@@ -1053,7 +1053,7 @@ Instance: Params (@partial_alter) 4 := {}.
 Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [dom C m] should yield the domain of [m]. That is a finite
-collection of type [C] that contains the keys that are a member of [m]. *)
+set of type [C] that contains the keys that are a member of [m]. *)
 Class Dom (M C : Type) := dom: M → C.
 Hint Mode Dom ! ! : typeclass_instances.
 Instance: Params (@dom) 3 := {}.
@@ -1110,23 +1110,28 @@ Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
 Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 
 
-(** * Axiomatization of collections *)
-(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
-elements of type [A]. *)
-Class SimpleCollection A C `{ElemOf A C,
+(** * Axiomatization of sets *)
+(** The classes [SemiSet A C] and [Set_ A C] axiomatize sset of type [C] with
+elements of type [A]. The first class, [SemiSet] does not include intersection
+and difference. It is useful for the case of lists, where decidable equality
+is needed to implement intersection and difference, but not union.
+
+Note that we cannot use the name [Set] since that is a reserved keyword. Hence
+we use [Set_]. *)
+Class SemiSet A C `{ElemOf A C,
     Empty C, Singleton A C, Union C} : Prop := {
   not_elem_of_empty (x : A) : x ∉ ∅;
   elem_of_singleton (x y : A) : x ∈ {[ y ]} ↔ x = y;
   elem_of_union X Y (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
 }.
-Class Collection A C `{ElemOf A C, Empty C, Singleton A C,
+Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
-  collection_simple :>> SimpleCollection A C;
+  set_semi_set :>> SemiSet A C;
   elem_of_intersection X Y (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
   elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
 
-(** We axiomative a finite collection as a collection whose elements can be
+(** We axiomative a finite set as a set whose elements can be
 enumerated as a list. These elements, given by the [elements] function, may be
 in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
@@ -1159,9 +1164,9 @@ Qed.
 
 (** Decidability of equality of the carrier set is admissible, but we add it
 anyway so as to avoid cycles in type class search. *)
-Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
+Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
     Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
-  fin_collection :>> Collection A C;
+  fin_set_set :>> Set_ A C;
   elem_of_elements X x : x ∈ elements X ↔ x ∈ X;
   NoDup_elements X : NoDup (elements X)
 }.
@@ -1170,18 +1175,18 @@ Hint Mode Size ! : typeclass_instances.
 Arguments size {_ _} !_ / : simpl nomatch, assert.
 Instance: Params (@size) 2 := {}.
 
-(** The class [CollectionMonad M] axiomatizes a type constructor [M] that can be
-used to construct a collection [M A] with elements of type [A]. The advantage
-of this class, compared to [Collection], is that it also axiomatizes the
+(** The class [MonadSet M] axiomatizes a type constructor [M] that can be
+used to construct a set [M A] with elements of type [A]. The advantage
+of this class, compared to [Set_], is that it also axiomatizes the
 the monadic operations. The disadvantage, is that not many inhabits are
 possible (we will only provide an inhabitant using unordered lists without
-duplicates removed). More interesting implementations typically need
-decidability of equality, or a total order on the elements, which do not fit
+duplicates). More interesting implementations typically need
+decidable equality, or a total order on the elements, which do not fit
 in a type constructor of type [Type → Type]. *)
-Class CollectionMonad M `{∀ A, ElemOf A (M A),
+Class MonadSet M `{∀ A, ElemOf A (M A),
     ∀ A, Empty (M A), ∀ A, Singleton A (M A), ∀ A, Union (M A),
     !MBind M, !MRet M, !FMap M, !MJoin M} : Prop := {
-  collection_monad_simple A :> SimpleCollection A (M A);
+  monad_set_semi_set A :> SemiSet A (M A);
   elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) :
     x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X;
   elem_of_ret {A} (x y : A) : x ∈ mret y ↔ x = y;
@@ -1192,13 +1197,13 @@ Class CollectionMonad M `{∀ A, ElemOf A (M A),
 
 (** The function [fresh X] yields an element that is not contained in [X]. We
 will later prove that [fresh] is [Proper] with respect to the induced setoid
-equality on collections. *)
+equality on sets. *)
 Class Fresh A C := fresh: C → A.
 Hint Mode Fresh - ! : typeclass_instances.
 Instance: Params (@fresh) 3 := {}.
 Class FreshSpec A C `{ElemOf A C,
     Empty C, Singleton A C, Union C, Fresh A C} : Prop := {
-  fresh_collection_simple :>> SimpleCollection A C;
+  fresh_set_semi_set :>> SemiSet A C;
   fresh_proper_alt X Y : (∀ x, x ∈ X ↔ x ∈ Y) → fresh X = fresh Y;
   is_fresh (X : C) : fresh X ∉ X
 }.
diff --git a/theories/boolset.v b/theories/boolset.v
new file mode 100644
index 0000000000000000000000000000000000000000..cd4efe1a56d0e4a7b46144c11158605c3992a9a1
--- /dev/null
+++ b/theories/boolset.v
@@ -0,0 +1,37 @@
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file implements boolsets as functions into Prop. *)
+From stdpp Require Export prelude.
+Set Default Proof Using "Type".
+
+Record boolset (A : Type) : Type := BoolSet { boolset_car : A → bool }.
+Arguments BoolSet {_} _ : assert.
+Arguments boolset_car {_} _ _ : assert.
+
+Instance boolset_top {A} : Top (boolset A) := BoolSet (λ _, true).
+Instance boolset_empty {A} : Empty (boolset A) := BoolSet (λ _, false).
+Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A) := λ x,
+  BoolSet (λ y, bool_decide (y = x)).
+Instance boolset_elem_of {A} : ElemOf A (boolset A) := λ x X, boolset_car X x.
+Instance boolset_union {A} : Union (boolset A) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x || boolset_car X2 x).
+Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
+Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
+Instance boolset_set `{EqDecision A} : Set_ A (boolset A).
+Proof.
+  split; [split| |].
+  - by intros x ?.
+  - by intros x y; rewrite <-(bool_decide_spec (x = y)).
+  - split. apply orb_prop_elim. apply orb_prop_intro.
+  - split. apply andb_prop_elim. apply andb_prop_intro.
+  - intros X Y x; unfold elem_of, boolset_elem_of; simpl. 
+    destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
+Qed.
+Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
+Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
+
+Typeclasses Opaque boolset_elem_of.
+Global Opaque boolset_empty boolset_singleton boolset_union
+  boolset_intersection boolset_difference.
diff --git a/theories/bset.v b/theories/bset.v
deleted file mode 100644
index ffb599f1db4dc5cae590aaa3c014b49d1c81f93b..0000000000000000000000000000000000000000
--- a/theories/bset.v
+++ /dev/null
@@ -1,37 +0,0 @@
-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
-(** This file implements bsets as functions into Prop. *)
-From stdpp Require Export prelude.
-Set Default Proof Using "Type".
-
-Record bset (A : Type) : Type := mkBSet { bset_car : A → bool }.
-Arguments mkBSet {_} _ : assert.
-Arguments bset_car {_} _ _ : assert.
-
-Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
-Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
-Instance bset_singleton `{EqDecision A} : Singleton A (bset A) := λ x,
-  mkBSet (λ y, bool_decide (y = x)).
-Instance bset_elem_of {A} : ElemOf A (bset A) := λ x X, bset_car X x.
-Instance bset_union {A} : Union (bset A) := λ X1 X2,
-  mkBSet (λ x, bset_car X1 x || bset_car X2 x).
-Instance bset_intersection {A} : Intersection (bset A) := λ X1 X2,
-  mkBSet (λ x, bset_car X1 x && bset_car X2 x).
-Instance bset_difference {A} : Difference (bset A) := λ X1 X2,
-  mkBSet (λ x, bset_car X1 x && negb (bset_car X2 x)).
-Instance bset_collection `{EqDecision A} : Collection A (bset A).
-Proof.
-  split; [split| |].
-  - by intros x ?.
-  - by intros x y; rewrite <-(bool_decide_spec (x = y)).
-  - split. apply orb_prop_elim. apply orb_prop_intro.
-  - split. apply andb_prop_elim. apply andb_prop_intro.
-  - intros X Y x; unfold elem_of, bset_elem_of; simpl. 
-    destruct (bset_car X x), (bset_car Y x); simpl; tauto.
-Qed.
-Instance bset_elem_of_dec {A} : RelDecision (∈@{bset A}).
-Proof. refine (λ x X, cast_if (decide (bset_car X x))); done. Defined.
-
-Typeclasses Opaque bset_elem_of.
-Global Opaque bset_empty bset_singleton bset_union
-  bset_intersection bset_difference.
diff --git a/theories/coPset.v b/theories/coPset.v
index f0a8f51656e9f48bb6f32b3e3781a0181851958b..4b583ed71d7c9086bd945fa1e748879130d06151 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -11,7 +11,7 @@ membership, as well as extensional equality (i.e. [X = Y ↔ ∀ x, x ∈ X ↔
 
 Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
 to the decision function that map bitstrings to bools. *)
-From stdpp Require Export collections.
+From stdpp Require Export sets.
 From stdpp Require Import pmap gmap mapset.
 Set Default Proof Using "Type".
 Local Open Scope positive_scope.
@@ -126,26 +126,26 @@ Lemma coPset_intersection_wf t1 t2 :
 Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
 Lemma coPset_opp_wf t : coPset_wf (coPset_opp_raw t).
 Proof. induction t as [[]|[]]; simpl; eauto. Qed.
-Lemma elem_to_Pset_singleton p q : e_of p (coPset_singleton_raw q) ↔ p = q.
+Lemma coPset_elem_of_singleton p q : e_of p (coPset_singleton_raw q) ↔ p = q.
 Proof.
   split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node].
   by revert q; induction p; intros [?|?|]; simpl;
     rewrite ?coPset_elem_of_node; intros; f_equal/=; auto.
 Qed.
-Lemma elem_to_Pset_union t1 t2 p : e_of p (t1 ∪ t2) = e_of p t1 || e_of p t2.
+Lemma coPset_elem_of_union t1 t2 p : e_of p (t1 ∪ t2) = e_of p t1 || e_of p t2.
 Proof.
   by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl;
     rewrite ?coPset_elem_of_node; simpl;
     rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r.
 Qed.
-Lemma elem_to_Pset_intersection t1 t2 p :
+Lemma coPset_elem_of_intersection t1 t2 p :
   e_of p (t1 ∩ t2) = e_of p t1 && e_of p t2.
 Proof.
   by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl;
     rewrite ?coPset_elem_of_node; simpl;
     rewrite ?andb_true_l, ?andb_false_l, ?andb_true_r, ?andb_false_r.
 Qed.
-Lemma elem_to_Pset_opp t p : e_of p (coPset_opp_raw t) = negb (e_of p t).
+Lemma coPset_elem_of_opp t p : e_of p (coPset_opp_raw t) = negb (e_of p t).
 Proof.
   by revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
     rewrite ?coPset_elem_of_node; simpl.
@@ -169,18 +169,18 @@ Instance coPset_difference : Difference coPset := λ X Y,
   let (t1,Ht1) := X in let (t2,Ht2) := Y in
   (t1 ∩ coPset_opp_raw t2) ↾ coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
 
-Instance coPset_collection : Collection positive coPset.
+Instance coPset_set : Set_ positive coPset.
 Proof.
   split; [split| |].
   - by intros ??.
-  - intros p q. apply elem_to_Pset_singleton.
+  - intros p q. apply coPset_elem_of_singleton.
   - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
-    by rewrite elem_to_Pset_union, orb_True.
+    by rewrite coPset_elem_of_union, orb_True.
   - intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl.
-    by rewrite elem_to_Pset_intersection, andb_True.
+    by rewrite coPset_elem_of_intersection, andb_True.
   - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
-    by rewrite elem_to_Pset_intersection,
-      elem_to_Pset_opp, andb_True, negb_True.
+    by rewrite coPset_elem_of_intersection,
+      coPset_elem_of_opp, andb_True, negb_True.
 Qed.
 
 Instance coPset_leibniz : LeibnizEquiv coPset.
@@ -223,7 +223,7 @@ Proof.
   unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
   - induction t as [b|b l IHl r IHr]; simpl.
     { destruct b; simpl; [intros [l Hl]|done].
-      by apply (is_fresh (of_list l : Pset)), elem_of_of_list, Hl. }
+      by apply (is_fresh (list_to_set l : Pset)), elem_of_list_to_set, Hl. }
     intros [ll Hll]; rewrite andb_True; split.
     + apply IHl; exists (omap (maybe (~0)) ll); intros i.
       rewrite elem_of_list_omap; intros; exists (i~0); auto.
@@ -271,88 +271,88 @@ Proof.
 Qed.
 
 (** * Conversion to psets *)
-Fixpoint to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
+Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
   match t with
   | coPLeaf _ => PLeaf
-  | coPNode false l r => PNode' None (to_Pset_raw l) (to_Pset_raw r)
-  | coPNode true l r => PNode (Some ()) (to_Pset_raw l) (to_Pset_raw r)
+  | coPNode false l r => PNode' None (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
+  | coPNode true l r => PNode (Some ()) (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
   end.
-Lemma to_Pset_wf t : coPset_wf t → Pmap_wf (to_Pset_raw t).
+Lemma coPset_to_Pset_wf t : coPset_wf t → Pmap_wf (coPset_to_Pset_raw t).
 Proof. induction t as [|[]]; simpl; eauto using PNode_wf. Qed.
-Definition to_Pset (X : coPset) : Pset :=
-  let (t,Ht) := X in Mapset (PMap (to_Pset_raw t) (to_Pset_wf _ Ht)).
-Lemma elem_of_to_Pset X i : set_finite X → i ∈ to_Pset X ↔ i ∈ X.
+Definition coPset_to_Pset (X : coPset) : Pset :=
+  let (t,Ht) := X in Mapset (PMap (coPset_to_Pset_raw t) (coPset_to_Pset_wf _ Ht)).
+Lemma elem_of_coPset_to_Pset X i : set_finite X → i ∈ coPset_to_Pset X ↔ i ∈ X.
 Proof.
   rewrite coPset_finite_spec; destruct X as [t Ht].
-  change (coPset_finite t → to_Pset_raw t !! i = Some () ↔ e_of i t).
+  change (coPset_finite t → coPset_to_Pset_raw t !! i = Some () ↔ e_of i t).
   clear Ht; revert i; induction t as [[]|[] l IHl r IHr]; intros [i|i|];
     simpl; rewrite ?andb_True, ?PNode_lookup; naive_solver.
 Qed.
 
 (** * Conversion from psets *)
-Fixpoint of_Pset_raw (t : Pmap_raw ()) : coPset_raw :=
+Fixpoint Pset_to_coPset_raw (t : Pmap_raw ()) : coPset_raw :=
   match t with
   | PLeaf => coPLeaf false
-  | PNode None l r => coPNode false (of_Pset_raw l) (of_Pset_raw r)
-  | PNode (Some _) l r => coPNode true (of_Pset_raw l) (of_Pset_raw r)
+  | PNode None l r => coPNode false (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
+  | PNode (Some _) l r => coPNode true (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
   end.
-Lemma of_Pset_wf t : Pmap_wf t → coPset_wf (of_Pset_raw t).
+Lemma Pset_to_coPset_wf t : Pmap_wf t → coPset_wf (Pset_to_coPset_raw t).
 Proof.
   induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto.
   - intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
   - destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
       rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition.
 Qed.
-Lemma elem_of_of_Pset_raw i t : e_of i (of_Pset_raw t) ↔ t !! i = Some ().
+Lemma elem_of_Pset_to_coPset_raw i t : e_of i (Pset_to_coPset_raw t) ↔ t !! i = Some ().
 Proof. by revert i; induction t as [|[[]|]]; intros []; simpl; auto; split. Qed.
-Lemma of_Pset_raw_finite t : coPset_finite (of_Pset_raw t).
+Lemma Pset_to_coPset_raw_finite t : coPset_finite (Pset_to_coPset_raw t).
 Proof. induction t as [|[[]|]]; simpl; rewrite ?andb_True; auto. Qed.
 
-Definition of_Pset (X : Pset) : coPset :=
-  let 'Mapset (PMap t Ht) := X in of_Pset_raw t ↾ of_Pset_wf _ Ht.
-Lemma elem_of_of_Pset X i : i ∈ of_Pset X ↔ i ∈ X.
-Proof. destruct X as [[t ?]]; apply elem_of_of_Pset_raw. Qed.
-Lemma of_Pset_finite X : set_finite (of_Pset X).
+Definition Pset_to_coPset (X : Pset) : coPset :=
+  let 'Mapset (PMap t Ht) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
+Lemma elem_of_Pset_to_coPset X i : i ∈ Pset_to_coPset X ↔ i ∈ X.
+Proof. destruct X as [[t ?]]; apply elem_of_Pset_to_coPset_raw. Qed.
+Lemma Pset_to_coPset_finite X : set_finite (Pset_to_coPset X).
 Proof.
-  apply coPset_finite_spec; destruct X as [[t ?]]; apply of_Pset_raw_finite.
+  apply coPset_finite_spec; destruct X as [[t ?]]; apply Pset_to_coPset_raw_finite.
 Qed.
 
 (** * Conversion to and from gsets of positives *)
-Lemma to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m.
+Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m.
 Proof. done. Qed.
-Definition to_gset (X : coPset) : gset positive :=
-  let 'Mapset m := to_Pset X in
-  Mapset (GMap m (bool_decide_pack _ (to_gset_wf m))).
+Definition coPset_to_gset (X : coPset) : gset positive :=
+  let 'Mapset m := coPset_to_Pset X in
+  Mapset (GMap m (bool_decide_pack _ (coPset_to_gset_wf m))).
 
-Definition of_gset (X : gset positive) : coPset :=
-  let 'Mapset (GMap (PMap t Ht) _) := X in of_Pset_raw t ↾ of_Pset_wf _ Ht.
+Definition gset_to_coPset (X : gset positive) : coPset :=
+  let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
 
-Lemma elem_of_to_gset X i : set_finite X → i ∈ to_gset X ↔ i ∈ X.
+Lemma elem_of_coPset_to_gset X i : set_finite X → i ∈ coPset_to_gset X ↔ i ∈ X.
 Proof.
-  intros ?. rewrite <-elem_of_to_Pset by done.
-  unfold to_gset. by destruct (to_Pset X).
+  intros ?. rewrite <-elem_of_coPset_to_Pset by done.
+  unfold coPset_to_gset. by destruct (coPset_to_Pset X).
 Qed.
 
-Lemma elem_of_of_gset X i : i ∈ of_gset X ↔ i ∈ X.
-Proof. destruct X as [[[t ?]]]; apply elem_of_of_Pset_raw. Qed.
-Lemma of_gset_finite X : set_finite (of_gset X).
+Lemma elem_of_gset_to_coPset X i : i ∈ gset_to_coPset X ↔ i ∈ X.
+Proof. destruct X as [[[t ?]]]; apply elem_of_Pset_to_coPset_raw. Qed.
+Lemma gset_to_coPset_finite X : set_finite (gset_to_coPset X).
 Proof.
-  apply coPset_finite_spec; destruct X as [[[t ?]]]; apply of_Pset_raw_finite.
+  apply coPset_finite_spec; destruct X as [[[t ?]]]; apply Pset_to_coPset_raw_finite.
 Qed.
 
 (** * Domain of finite maps *)
-Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, of_Pset (dom _ m).
+Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, Pset_to_coPset (dom _ m).
 Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
 Proof.
   split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
-  by rewrite elem_of_of_Pset, elem_of_dom.
+  by rewrite elem_of_Pset_to_coPset, elem_of_dom.
 Qed.
 Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
-  of_gset (dom _ m).
+  gset_to_coPset (dom _ m).
 Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
 Proof.
   split; try apply _; intros A m i; unfold dom, gmap_dom_coPset.
-  by rewrite elem_of_of_gset, elem_of_dom.
+  by rewrite elem_of_gset_to_coPset, elem_of_dom.
 Qed.
 
 (** * Suffix sets *)
@@ -405,7 +405,7 @@ Definition coPset_r (X : coPset) : coPset :=
 Lemma coPset_lr_disjoint X : coPset_l X ∩ coPset_r X = ∅.
 Proof.
   apply elem_of_equiv_empty_L; intros p; apply Is_true_false.
-  destruct X as [t Ht]; simpl; clear Ht; rewrite elem_to_Pset_intersection.
+  destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_intersection.
   revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
     rewrite ?coPset_elem_of_node; simpl;
     rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; auto.
@@ -413,7 +413,7 @@ Qed.
 Lemma coPset_lr_union X : coPset_l X ∪ coPset_r X = X.
 Proof.
   apply elem_of_equiv_L; intros p; apply eq_bool_prop_elim.
-  destruct X as [t Ht]; simpl; clear Ht; rewrite elem_to_Pset_union.
+  destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_union.
   revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
     rewrite ?coPset_elem_of_node; simpl;
     rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; auto.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 761dd4baab781643d7da32e8e1c09e20b81d31bc..114ae30d4fd760ea54f39d939ff14cb99706f4f6 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -3,7 +3,7 @@
 (** This file provides an axiomatization of the domain function of finite
 maps. We provide such an axiomatization, instead of implementing the domain
 function in a generic way, to allow more efficient implementations. *)
-From stdpp Require Export collections fin_maps.
+From stdpp Require Export sets fin_maps.
 Set Default Proof Using "Type*".
 
 Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
@@ -12,7 +12,7 @@ Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
     ElemOf K D, Empty D, Singleton K D,
     Union D, Intersection D, Difference D} := {
   finmap_dom_map :>> FinMap K M;
-  finmap_dom_collection :>> Collection K D;
+  finmap_dom_set :>> Set_ K D;
   elem_of_dom {A} (m : M A) i : i ∈ dom D m ↔ is_Some (m !! i)
 }.
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d965b6c8c06bf1e7e83babf8f2339e493a9a77ca..02d9dcfc31176c9a33c4f24646383d322de60f66 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -5,7 +5,7 @@ finite maps and collects some theory on it. Most importantly, it proves useful
 induction principles for finite maps and implements the tactic
 [simplify_map_eq] to simplify goals involving finite maps. *)
 From Coq Require Import Permutation.
-From stdpp Require Export relations orders vector fin_collections.
+From stdpp Require Export relations orders vector fin_sets.
 (* FIXME: This file needs a 'Proof Using' hint, but the default we use
    everywhere makes for lots of extra ssumptions. *)
 
@@ -61,17 +61,17 @@ Instance map_delete `{PartialAlter K A M} : Delete K M :=
 Instance map_singleton `{PartialAlter K A M, Empty M} :
   SingletonM K A M := λ i x, <[i:=x]> ∅.
 
-Definition map_of_list `{Insert K A M, Empty M} : list (K * A) → M :=
+Definition list_to_map `{Insert K A M, Empty M} : list (K * A) → M :=
   fold_right (λ p, <[p.1:=p.2]>) ∅.
 
 Instance map_size `{FinMapToList K A M} : Size M := λ m, length (map_to_list m).
 
-Definition map_to_collection `{FinMapToList K A M,
+Definition map_to_set `{FinMapToList K A M,
     Singleton B C, Empty C, Union C} (f : K → A → B) (m : M) : C :=
-  of_list (curry f <$> map_to_list m).
-Definition map_of_collection `{Elements B C, Insert K A M, Empty M}
+  list_to_set (curry f <$> map_to_list m).
+Definition set_to_map `{Elements B C, Insert K A M, Empty M}
     (f : B → K * A) (X : C) : M :=
-  map_of_list (f <$> elements X).
+  list_to_map (f <$> elements X).
 
 Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
   λ f, merge (union_with f).
@@ -120,7 +120,7 @@ Instance map_difference `{Merge M} {A} : Difference (M A) :=
 of the elements. Implemented by conversion to lists, so not very efficient. *)
 Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
     ∀ A, FinMapToList K A (M A)} {A B} (f : K → A → option B) (m : M A) : M B :=
-  map_of_list (omap (λ ix, (fst ix,) <$> curry f ix) (map_to_list m)).
+  list_to_map (omap (λ ix, (fst ix,) <$> curry f ix) (map_to_list m)).
 
 (* The zip operation on maps combines two maps key-wise. The keys of resulting
 map correspond to the keys that are in both maps. *)
@@ -684,8 +684,8 @@ Lemma map_to_list_unique {A} (m : M A) i x y :
 Proof. rewrite !elem_of_map_to_list. congruence. Qed.
 Lemma NoDup_fst_map_to_list {A} (m : M A) : NoDup ((map_to_list m).*1).
 Proof. eauto using NoDup_fmap_fst, map_to_list_unique, NoDup_map_to_list. Qed.
-Lemma elem_of_map_of_list_1' {A} (l : list (K * A)) i x :
-  (∀ y, (i,y) ∈ l → x = y) → (i,x) ∈ l → (map_of_list l : M A) !! i = Some x.
+Lemma elem_of_list_to_map_1' {A} (l : list (K * A)) i x :
+  (∀ y, (i,y) ∈ l → x = y) → (i,x) ∈ l → (list_to_map l : M A) !! i = Some x.
 Proof.
   induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|].
   setoid_rewrite elem_of_cons.
@@ -694,91 +694,91 @@ Proof.
   - rewrite lookup_insert; f_equal; eauto using eq_sym.
   - rewrite lookup_insert_ne by done; eauto.
 Qed.
-Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x :
-  NoDup (l.*1) → (i,x) ∈ l → (map_of_list l : M A) !! i = Some x.
+Lemma elem_of_list_to_map_1 {A} (l : list (K * A)) i x :
+  NoDup (l.*1) → (i,x) ∈ l → (list_to_map l : M A) !! i = Some x.
 Proof.
-  intros ? Hx; apply elem_of_map_of_list_1'; eauto using NoDup_fmap_fst.
+  intros ? Hx; apply elem_of_list_to_map_1'; eauto using NoDup_fmap_fst.
   intros y; revert Hx. rewrite !elem_of_list_lookup; intros [i' Hi'] [j' Hj'].
   cut (i' = j'); [naive_solver|]. apply NoDup_lookup with (l.*1) i;
     by rewrite ?list_lookup_fmap, ?Hi', ?Hj'.
 Qed.
-Lemma elem_of_map_of_list_2 {A} (l : list (K * A)) i x :
-  (map_of_list l : M A) !! i = Some x → (i,x) ∈ l.
+Lemma elem_of_list_to_map_2 {A} (l : list (K * A)) i x :
+  (list_to_map l : M A) !! i = Some x → (i,x) ∈ l.
 Proof.
   induction l as [|[j y] l IH]; simpl; [by rewrite lookup_empty|].
   rewrite elem_of_cons. destruct (decide (i = j)) as [->|];
     rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
 Qed.
-Lemma elem_of_map_of_list' {A} (l : list (K * A)) i x :
+Lemma elem_of_list_to_map' {A} (l : list (K * A)) i x :
   (∀ x', (i,x) ∈ l → (i,x') ∈ l → x = x') →
-  (i,x) ∈ l ↔ (map_of_list l : M A) !! i = Some x.
-Proof. split; auto using elem_of_map_of_list_1', elem_of_map_of_list_2. Qed.
-Lemma elem_of_map_of_list {A} (l : list (K * A)) i x :
-  NoDup (l.*1) → (i,x) ∈ l ↔ (map_of_list l : M A) !! i = Some x.
-Proof. split; auto using elem_of_map_of_list_1, elem_of_map_of_list_2. Qed.
+  (i,x) ∈ l ↔ (list_to_map l : M A) !! i = Some x.
+Proof. split; auto using elem_of_list_to_map_1', elem_of_list_to_map_2. Qed.
+Lemma elem_of_list_to_map {A} (l : list (K * A)) i x :
+  NoDup (l.*1) → (i,x) ∈ l ↔ (list_to_map l : M A) !! i = Some x.
+Proof. split; auto using elem_of_list_to_map_1, elem_of_list_to_map_2. Qed.
 
-Lemma not_elem_of_map_of_list_1 {A} (l : list (K * A)) i :
-  i ∉ l.*1 → (map_of_list l : M A) !! i = None.
+Lemma not_elem_of_list_to_map_1 {A} (l : list (K * A)) i :
+  i ∉ l.*1 → (list_to_map l : M A) !! i = None.
 Proof.
   rewrite elem_of_list_fmap, eq_None_not_Some. intros Hi [x ?]; destruct Hi.
-  exists (i,x); simpl; auto using elem_of_map_of_list_2.
+  exists (i,x); simpl; auto using elem_of_list_to_map_2.
 Qed.
-Lemma not_elem_of_map_of_list_2 {A} (l : list (K * A)) i :
-  (map_of_list l : M A) !! i = None → i ∉ l.*1.
+Lemma not_elem_of_list_to_map_2 {A} (l : list (K * A)) i :
+  (list_to_map l : M A) !! i = None → i ∉ l.*1.
 Proof.
   induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|].
   rewrite elem_of_cons. destruct (decide (i = j)); simplify_eq.
   - by rewrite lookup_insert.
   - by rewrite lookup_insert_ne; intuition.
 Qed.
-Lemma not_elem_of_map_of_list {A} (l : list (K * A)) i :
-  i ∉ l.*1 ↔ (map_of_list l : M A) !! i = None.
-Proof. red; auto using not_elem_of_map_of_list_1,not_elem_of_map_of_list_2. Qed.
-Lemma map_of_list_proper {A} (l1 l2 : list (K * A)) :
-  NoDup (l1.*1) → l1 ≡ₚ l2 → (map_of_list l1 : M A) = map_of_list l2.
+Lemma not_elem_of_list_to_map {A} (l : list (K * A)) i :
+  i ∉ l.*1 ↔ (list_to_map l : M A) !! i = None.
+Proof. red; auto using not_elem_of_list_to_map_1,not_elem_of_list_to_map_2. Qed.
+Lemma list_to_map_proper {A} (l1 l2 : list (K * A)) :
+  NoDup (l1.*1) → l1 ≡ₚ l2 → (list_to_map l1 : M A) = list_to_map l2.
 Proof.
   intros ? Hperm. apply map_eq. intros i. apply option_eq. intros x.
-  by rewrite <-!elem_of_map_of_list; rewrite <-?Hperm.
+  by rewrite <-!elem_of_list_to_map; rewrite <-?Hperm.
 Qed.
-Lemma map_of_list_inj {A} (l1 l2 : list (K * A)) :
+Lemma list_to_map_inj {A} (l1 l2 : list (K * A)) :
   NoDup (l1.*1) → NoDup (l2.*1) →
-  (map_of_list l1 : M A) = map_of_list l2 → l1 ≡ₚ l2.
+  (list_to_map l1 : M A) = list_to_map l2 → l1 ≡ₚ l2.
 Proof.
   intros ?? Hl1l2. apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
-  intros [i x]. by rewrite !elem_of_map_of_list, Hl1l2.
+  intros [i x]. by rewrite !elem_of_list_to_map, Hl1l2.
 Qed.
-Lemma map_of_to_list {A} (m : M A) : map_of_list (map_to_list m) = m.
+Lemma list_to_map_to_list {A} (m : M A) : list_to_map (map_to_list m) = m.
 Proof.
   apply map_eq. intros i. apply option_eq. intros x.
-  by rewrite <-elem_of_map_of_list, elem_of_map_to_list
+  by rewrite <-elem_of_list_to_map, elem_of_map_to_list
     by auto using NoDup_fst_map_to_list.
 Qed.
-Lemma map_to_of_list {A} (l : list (K * A)) :
-  NoDup (l.*1) → map_to_list (map_of_list l) ≡ₚ l.
-Proof. auto using map_of_list_inj, NoDup_fst_map_to_list, map_of_to_list. Qed.
+Lemma map_to_list_to_map {A} (l : list (K * A)) :
+  NoDup (l.*1) → map_to_list (list_to_map l) ≡ₚ l.
+Proof. auto using list_to_map_inj, NoDup_fst_map_to_list, list_to_map_to_list. Qed.
 Lemma map_to_list_inj {A} (m1 m2 : M A) :
   map_to_list m1 ≡ₚ map_to_list m2 → m1 = m2.
 Proof.
-  intros. rewrite <-(map_of_to_list m1), <-(map_of_to_list m2).
-  auto using map_of_list_proper, NoDup_fst_map_to_list.
+  intros. rewrite <-(list_to_map_to_list m1), <-(list_to_map_to_list m2).
+  auto using list_to_map_proper, NoDup_fst_map_to_list.
 Qed.
-Lemma map_to_of_list_flip {A} (m1 : M A) l2 :
-  map_to_list m1 ≡ₚ l2 → m1 = map_of_list l2.
+Lemma list_to_map_flip {A} (m1 : M A) l2 :
+  map_to_list m1 ≡ₚ l2 → m1 = list_to_map l2.
 Proof.
-  intros. rewrite <-(map_of_to_list m1).
-  auto using map_of_list_proper, NoDup_fst_map_to_list.
+  intros. rewrite <-(list_to_map_to_list m1).
+  auto using list_to_map_proper, NoDup_fst_map_to_list.
 Qed.
 
-Lemma map_of_list_nil {A} : map_of_list [] = (∅ : M A).
+Lemma list_to_map_nil {A} : list_to_map [] = (∅ : M A).
 Proof. done. Qed.
-Lemma map_of_list_cons {A} (l : list (K * A)) i x :
-  map_of_list ((i, x) :: l) = <[i:=x]>(map_of_list l : M A).
+Lemma list_to_map_cons {A} (l : list (K * A)) i x :
+  list_to_map ((i, x) :: l) = <[i:=x]>(list_to_map l : M A).
 Proof. done. Qed.
-Lemma map_of_list_fmap {A B} (f : A → B) l :
-  map_of_list (prod_map id f <$> l) = f <$> (map_of_list l : M A).
+Lemma list_to_map_fmap {A B} (f : A → B) l :
+  list_to_map (prod_map id f <$> l) = f <$> (list_to_map l : M A).
 Proof.
   induction l as [|[i x] l IH]; csimpl; rewrite ?fmap_empty; auto.
-  rewrite <-map_of_list_cons; simpl. by rewrite IH, <-fmap_insert.
+  rewrite <-list_to_map_cons; simpl. by rewrite IH, <-fmap_insert.
 Qed.
 
 Lemma map_to_list_empty {A} : map_to_list ∅ = @nil (K * A).
@@ -789,12 +789,12 @@ Qed.
 Lemma map_to_list_insert {A} (m : M A) i x :
   m !! i = None → map_to_list (<[i:=x]>m) ≡ₚ (i,x) :: map_to_list m.
 Proof.
-  intros. apply map_of_list_inj; csimpl.
+  intros. apply list_to_map_inj; csimpl.
   - apply NoDup_fst_map_to_list.
   - constructor; auto using NoDup_fst_map_to_list.
     rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
     rewrite elem_of_map_to_list in Hlookup. congruence.
-  - by rewrite !map_of_to_list.
+  - by rewrite !list_to_map_to_list.
 Qed.
 Lemma map_to_list_singleton {A} i (x : A) :
   map_to_list ({[i:=x]} : M A) = [(i,x)].
@@ -815,8 +815,8 @@ Proof.
   assert (NoDup ((prod_map id f <$> map_to_list m).*1)).
   { erewrite <-list_fmap_compose, (list_fmap_ext _ fst) by done.
     apply NoDup_fst_map_to_list. }
-  rewrite <-(map_of_to_list m) at 1.
-  by rewrite <-map_of_list_fmap, map_to_of_list.
+  rewrite <-(list_to_map_to_list m) at 1.
+  by rewrite <-list_to_map_fmap, map_to_list_to_map.
 Qed.
 
 Lemma map_to_list_empty_inv_alt {A}  (m : M A) : map_to_list m ≡ₚ [] → m = ∅.
@@ -829,14 +829,14 @@ Proof.
 Qed.
 
 Lemma map_to_list_insert_inv {A} (m : M A) l i x :
-  map_to_list m ≡ₚ (i,x) :: l → m = <[i:=x]>(map_of_list l).
+  map_to_list m ≡ₚ (i,x) :: l → m = <[i:=x]>(list_to_map l).
 Proof.
   intros Hperm. apply map_to_list_inj.
   assert (i ∉ l.*1 ∧ NoDup (l.*1)) as [].
   { rewrite <-NoDup_cons. change (NoDup (((i,x)::l).*1)). rewrite <-Hperm.
     auto using NoDup_fst_map_to_list. }
-  rewrite Hperm, map_to_list_insert, map_to_of_list;
-    auto using not_elem_of_map_of_list_1.
+  rewrite Hperm, map_to_list_insert, map_to_list_to_map;
+    auto using not_elem_of_list_to_map_1.
 Qed.
 
 Lemma map_choose {A} (m : M A) : m ≠ ∅ → ∃ i x, m !! i = Some x.
@@ -858,12 +858,12 @@ Lemma lookup_imap {A B} (f : K → A → option B) (m : M A) i :
 Proof.
   unfold map_imap; destruct (m !! i ≫= f i) as [y|] eqn:Hi; simpl.
   - destruct (m !! i) as [x|] eqn:?; simplify_eq/=.
-    apply elem_of_map_of_list_1'.
+    apply elem_of_list_to_map_1'.
     { intros y'; rewrite elem_of_list_omap; intros ([i' x']&Hi'&?).
       by rewrite elem_of_map_to_list in Hi'; simplify_option_eq. }
     apply elem_of_list_omap; exists (i,x); split;
       [by apply elem_of_map_to_list|by simplify_option_eq].
-  - apply not_elem_of_map_of_list; rewrite elem_of_list_fmap.
+  - apply not_elem_of_list_to_map; rewrite elem_of_list_fmap.
     intros ([i' x]&->&Hi'); simplify_eq/=.
     rewrite elem_of_list_omap in Hi'; destruct Hi' as ([j y]&Hj&?).
     rewrite elem_of_map_to_list in Hj; simplify_option_eq.
@@ -889,57 +889,57 @@ Proof. intros. unfold size, map_size. by rewrite map_to_list_insert. Qed.
 Lemma map_size_fmap {A B} (f : A -> B) (m : M A) : size (f <$> m) = size m.
 Proof. intros. unfold size, map_size. by rewrite map_to_list_fmap, fmap_length. Qed.
 
-(** ** Properties of conversion from collections *)
-Section map_of_to_collection.
-  Context {A : Type} `{FinCollection B C}.
+(** ** Properties of conversion from sets *)
+Section set_to_map.
+  Context {A : Type} `{FinSet B C}.
 
-  Lemma lookup_map_of_collection (f : B → K * A) (Y : C) i x :
+  Lemma lookup_set_to_map (f : B → K * A) (Y : C) i x :
     (∀ y y', y ∈ Y → y' ∈ Y → (f y).1 = (f y').1 → y = y') →
-    (map_of_collection f Y : M A) !! i = Some x ↔ ∃ y, y ∈ Y ∧ f y = (i,x).
+    (set_to_map f Y : M A) !! i = Some x ↔ ∃ y, y ∈ Y ∧ f y = (i,x).
   Proof.
     intros Hinj. assert (∀ x',
       (i, x) ∈ f <$> elements Y → (i, x') ∈ f <$> elements Y → x = x').
     { intros x'. intros (y&Hx&Hy)%elem_of_list_fmap (y'&Hx'&Hy')%elem_of_list_fmap.
       rewrite elem_of_elements in Hy, Hy'.
       cut (y = y'); [congruence|]. apply Hinj; auto. by rewrite <-Hx, <-Hx'. }
-    unfold map_of_collection; rewrite <-elem_of_map_of_list' by done.
+    unfold set_to_map; rewrite <-elem_of_list_to_map' by done.
     rewrite elem_of_list_fmap. setoid_rewrite elem_of_elements; naive_solver.
   Qed.
 
-  Lemma elem_of_map_to_collection (f : K → A → B) (m : M A) (y : B) :
-    y ∈ map_to_collection (C:=C) f m ↔ ∃ i x, m !! i = Some x ∧ f i x = y.
+  Lemma elem_of_map_to_set (f : K → A → B) (m : M A) (y : B) :
+    y ∈ map_to_set (C:=C) f m ↔ ∃ i x, m !! i = Some x ∧ f i x = y.
   Proof.
-    unfold map_to_collection; simpl.
-    rewrite elem_of_of_list, elem_of_list_fmap. split.
+    unfold map_to_set; simpl.
+    rewrite elem_of_list_to_set, elem_of_list_fmap. split.
     - intros ([i x] & ? & ?%elem_of_map_to_list); eauto.
     - intros (i&x&?&?). exists (i,x). by rewrite elem_of_map_to_list.
   Qed.
-  Lemma map_to_collection_empty (f : K → A → B) :
-    map_to_collection f (∅ : M A) = (∅ : C).
-  Proof. unfold map_to_collection; simpl. by rewrite map_to_list_empty. Qed.
-  Lemma map_to_collection_insert (f : K → A → B)(m : M A) i x :
+  Lemma map_to_set_empty (f : K → A → B) :
+    map_to_set f (∅ : M A) = (∅ : C).
+  Proof. unfold map_to_set; simpl. by rewrite map_to_list_empty. Qed.
+  Lemma map_to_set_insert (f : K → A → B)(m : M A) i x :
     m !! i = None →
-    map_to_collection f (<[i:=x]>m) ≡@{C} {[f i x]} ∪ map_to_collection f m.
+    map_to_set f (<[i:=x]>m) ≡@{C} {[f i x]} ∪ map_to_set f m.
   Proof.
-    intros. unfold map_to_collection; simpl. by rewrite map_to_list_insert.
+    intros. unfold map_to_set; simpl. by rewrite map_to_list_insert.
   Qed.
-  Lemma map_to_collection_insert_L `{!LeibnizEquiv C} (f : K → A → B) (m : M A) i x :
+  Lemma map_to_set_insert_L `{!LeibnizEquiv C} (f : K → A → B) (m : M A) i x :
     m !! i = None →
-    map_to_collection f (<[i:=x]>m) =@{C} {[f i x]} ∪ map_to_collection f m.
-  Proof. unfold_leibniz. apply map_to_collection_insert. Qed.
-End map_of_to_collection.
+    map_to_set f (<[i:=x]>m) =@{C} {[f i x]} ∪ map_to_set f m.
+  Proof. unfold_leibniz. apply map_to_set_insert. Qed.
+End set_to_map.
 
-Lemma lookup_map_of_collection_id `{FinCollection (K * A) C} (X : C) i x :
+Lemma lookup_set_to_map_id `{FinSet (K * A) C} (X : C) i x :
   (∀ i y y', (i,y) ∈ X → (i,y') ∈ X → y = y') →
-  (map_of_collection id X : M A) !! i = Some x ↔ (i,x) ∈ X.
+  (set_to_map id X : M A) !! i = Some x ↔ (i,x) ∈ X.
 Proof.
-  intros. etrans; [apply lookup_map_of_collection|naive_solver].
+  intros. etrans; [apply lookup_set_to_map|naive_solver].
   intros [] [] ???; simplify_eq/=; eauto with f_equal.
 Qed.
 
-Lemma elem_of_map_to_collection_pair `{FinCollection (K * A) C} (m : M A) i x :
-  (i,x) ∈ map_to_collection pair m ↔ m !! i = Some x.
-Proof. rewrite elem_of_map_to_collection. naive_solver. Qed.
+Lemma elem_of_map_to_set_pair `{FinSet (K * A) C} (m : M A) i x :
+  (i,x) ∈ map_to_set pair m ↔ m !! i = Some x.
+Proof. rewrite elem_of_map_to_set. naive_solver. Qed.
 
 (** ** Induction principles *)
 Lemma map_ind {A} (P : M A → Prop) :
@@ -952,8 +952,8 @@ Proof.
   { apply map_to_list_empty_inv_alt in Hml. by subst. }
   inversion_clear Hnodup.
   apply map_to_list_insert_inv in Hml; subst m. apply Hins.
-  - by apply not_elem_of_map_of_list_1.
-  - apply IH; auto using map_to_of_list.
+  - by apply not_elem_of_list_to_map_1.
+  - apply IH; auto using map_to_list_to_map.
 Qed.
 Lemma map_to_list_length {A} (m1 m2 : M A) :
   m1 ⊂ m2 → length (map_to_list m1) < length (map_to_list m2).
@@ -1685,7 +1685,7 @@ Proof.
   by apply map_disjoint_singleton_r.
 Qed.
 Lemma foldr_insert_union {A} (m : M A) l :
-  foldr (λ p, <[p.1:=p.2]>) m l = map_of_list l ∪ m.
+  foldr (λ p, <[p.1:=p.2]>) m l = list_to_map l ∪ m.
 Proof.
   induction l as [|i l IH]; simpl; [by rewrite (left_id_L _ _)|].
   by rewrite IH, insert_union_l.
@@ -1747,38 +1747,38 @@ Lemma foldr_delete_union {A} (m1 m2 : M A) is :
 Proof. apply foldr_delete_union_with. Qed.
 
 (** ** Properties on disjointness of conversion to lists *)
-Lemma map_disjoint_of_list_l {A} (m : M A) ixs :
-  map_of_list ixs ##ₘ m ↔ Forall (λ ix, m !! ix.1 = None) ixs.
+Lemma map_disjoint_list_to_map_l {A} (m : M A) ixs :
+  list_to_map ixs ##ₘ m ↔ Forall (λ ix, m !! ix.1 = None) ixs.
 Proof.
   split.
   - induction ixs; simpl; rewrite ?map_disjoint_insert_l in *; intuition.
   - induction 1; simpl; [apply map_disjoint_empty_l|].
     rewrite map_disjoint_insert_l. auto.
 Qed.
-Lemma map_disjoint_of_list_r {A} (m : M A) ixs :
-  m ##ₘ map_of_list ixs ↔ Forall (λ ix, m !! ix.1 = None) ixs.
-Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_of_list_l. Qed.
-Lemma map_disjoint_of_list_zip_l {A} (m : M A) is xs :
+Lemma map_disjoint_list_to_map_r {A} (m : M A) ixs :
+  m ##ₘ list_to_map ixs ↔ Forall (λ ix, m !! ix.1 = None) ixs.
+Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_list_to_map_l. Qed.
+Lemma map_disjoint_list_to_map_zip_l {A} (m : M A) is xs :
   length is = length xs →
-  map_of_list (zip is xs) ##ₘ m ↔ Forall (λ i, m !! i = None) is.
+  list_to_map (zip is xs) ##ₘ m ↔ Forall (λ i, m !! i = None) is.
 Proof.
-  intro. rewrite map_disjoint_of_list_l.
+  intro. rewrite map_disjoint_list_to_map_l.
   rewrite <-(fst_zip is xs) at 2 by lia. by rewrite Forall_fmap.
 Qed.
-Lemma map_disjoint_of_list_zip_r {A} (m : M A) is xs :
+Lemma map_disjoint_list_to_map_zip_r {A} (m : M A) is xs :
   length is = length xs →
-  m ##ₘ map_of_list (zip is xs) ↔ Forall (λ i, m !! i = None) is.
+  m ##ₘ list_to_map (zip is xs) ↔ Forall (λ i, m !! i = None) is.
 Proof.
-  intro. by rewrite (symmetry_iff map_disjoint), map_disjoint_of_list_zip_l.
+  intro. by rewrite (symmetry_iff map_disjoint), map_disjoint_list_to_map_zip_l.
 Qed.
-Lemma map_disjoint_of_list_zip_l_2 {A} (m : M A) is xs :
+Lemma map_disjoint_list_to_map_zip_l_2 {A} (m : M A) is xs :
   length is = length xs → Forall (λ i, m !! i = None) is →
-  map_of_list (zip is xs) ##ₘ m.
-Proof. intro. by rewrite map_disjoint_of_list_zip_l. Qed.
-Lemma map_disjoint_of_list_zip_r_2 {A} (m : M A) is xs :
+  list_to_map (zip is xs) ##ₘ m.
+Proof. intro. by rewrite map_disjoint_list_to_map_zip_l. Qed.
+Lemma map_disjoint_list_to_map_zip_r_2 {A} (m : M A) is xs :
   length is = length xs → Forall (λ i, m !! i = None) is →
-  m ##ₘ map_of_list (zip is xs).
-Proof. intro. by rewrite map_disjoint_of_list_zip_r. Qed.
+  m ##ₘ list_to_map (zip is xs).
+Proof. intro. by rewrite map_disjoint_list_to_map_zip_r. Qed.
 
 (** ** Properties of the [intersection_with] operation *)
 Section intersection_with.
@@ -1958,10 +1958,10 @@ Hint Extern 2 (<[_:=_]>_ ##ₘ _) => apply map_disjoint_insert_l_2 : map_disjoin
 Hint Extern 2 (_ ##ₘ <[_:=_]>_) => apply map_disjoint_insert_r_2 : map_disjoint.
 Hint Extern 2 (delete _ _ ##ₘ _) => apply map_disjoint_delete_l : map_disjoint.
 Hint Extern 2 (_ ##ₘ delete _ _) => apply map_disjoint_delete_r : map_disjoint.
-Hint Extern 2 (map_of_list _ ##ₘ _) =>
-  apply map_disjoint_of_list_zip_l_2 : mem_disjoint.
-Hint Extern 2 (_ ##ₘ map_of_list _) =>
-  apply map_disjoint_of_list_zip_r_2 : mem_disjoint.
+Hint Extern 2 (list_to_map _ ##ₘ _) =>
+  apply map_disjoint_list_to_map_zip_l_2 : mem_disjoint.
+Hint Extern 2 (_ ##ₘ list_to_map _) =>
+  apply map_disjoint_list_to_map_zip_r_2 : mem_disjoint.
 Hint Extern 2 (⋃ _ ##ₘ _) => apply map_disjoint_union_list_l_2 : mem_disjoint.
 Hint Extern 2 (_ ##ₘ ⋃ _) => apply map_disjoint_union_list_r_2 : mem_disjoint.
 Hint Extern 2 (foldr delete _ _ ##ₘ _) =>
diff --git a/theories/fin_collections.v b/theories/fin_sets.v
similarity index 77%
rename from theories/fin_collections.v
rename to theories/fin_sets.v
index aaf08653c54ff6e8e79d56dd2ef2eaf1ec45a989..11789c4aaf74ae027aaf65c3d5ce739a8a8cbbbc 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_sets.v
@@ -1,31 +1,31 @@
 (* Copyright (c) 2012-2019, Coq-std++ developers. *)
 (* This file is distributed under the terms of the BSD license. *)
-(** This file collects definitions and theorems on finite collections. Most
+(** This file collects definitions and theorems on finite sets. Most
 importantly, it implements a fold and size function and some useful induction
-principles on finite collections . *)
+principles on finite sets . *)
 From stdpp Require Import relations.
-From stdpp Require Export numbers collections.
+From stdpp Require Export numbers sets.
 Set Default Proof Using "Type*".
 
-Instance collection_size `{Elements A C} : Size C := length ∘ elements.
-Definition collection_fold `{Elements A C} {B}
+Instance set_size `{Elements A C} : Size C := length ∘ elements.
+Definition set_fold `{Elements A C} {B}
   (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
 
-Instance collection_filter
+Instance set_filter
     `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
-  of_list (filter P (elements X)).
-Typeclasses Opaque collection_filter.
+  list_to_set (filter P (elements X)).
+Typeclasses Opaque set_filter.
 
-Definition collection_map `{Elements A C, Singleton B D, Empty D, Union D}
+Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
     (f : A → B) (X : C) : D :=
-  of_list (f <$> elements X).
-Typeclasses Opaque collection_map.
+  list_to_set (f <$> elements X).
+Typeclasses Opaque set_map.
 
-Section fin_collection.
-Context `{FinCollection A C}.
+Section fin_set.
+Context `{FinSet A C}.
 Implicit Types X Y : C.
 
-Lemma fin_collection_finite X : set_finite X.
+Lemma fin_set_finite X : set_finite X.
 Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
 
 Instance elem_of_dec_slow : RelDecision (∈@{C}) | 100.
@@ -80,11 +80,11 @@ Proof.
 Qed.
 
 (** * The [size] operation *)
-Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _).
+Global Instance set_size_proper: Proper ((≡) ==> (=)) (@size C _).
 Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
 
 Lemma size_empty : size (∅ : C) = 0.
-Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
+Proof. unfold size, set_size. simpl. by rewrite elements_empty. Qed.
 Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
 Proof.
   intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
@@ -95,27 +95,27 @@ Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
 Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅.
 Proof. by rewrite size_empty_iff. Qed.
 
-Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
+Lemma set_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
 Proof.
   destruct (elements X) as [|x l] eqn:HX; [right|left].
   - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
   - exists x. rewrite <-elem_of_elements, HX. by left.
 Qed.
-Lemma collection_choose X : X ≢ ∅ → ∃ x, x ∈ X.
-Proof. intros. by destruct (collection_choose_or_empty X). Qed.
-Lemma collection_choose_L `{!LeibnizEquiv C} X : X ≠ ∅ → ∃ x, x ∈ X.
-Proof. unfold_leibniz. apply collection_choose. Qed.
+Lemma set_choose X : X ≢ ∅ → ∃ x, x ∈ X.
+Proof. intros. by destruct (set_choose_or_empty X). Qed.
+Lemma set_choose_L `{!LeibnizEquiv C} X : X ≠ ∅ → ∃ x, x ∈ X.
+Proof. unfold_leibniz. apply set_choose. Qed.
 Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
 Proof.
-  intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
+  intros Hsz. destruct (set_choose_or_empty X) as [|HX]; [done|].
   contradict Hsz. rewrite HX, size_empty; lia.
 Qed.
 
 Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.
-Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed.
+Proof. unfold size, set_size. simpl. by rewrite elements_singleton. Qed.
 Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
-  unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
+  unfold size, set_size. simpl. rewrite <-!elem_of_elements.
   generalize (elements X). intros [|? l]; intro; simplify_eq/=.
   rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
 Qed.
@@ -129,7 +129,7 @@ Qed.
 
 Lemma size_union X Y : X ## Y → size (X ∪ Y) = size X + size Y.
 Proof.
-  intros. unfold size, collection_size. simpl. rewrite <-app_length.
+  intros. unfold size, set_size. simpl. rewrite <-app_length.
   apply Permutation_length, NoDup_Permutation.
   - apply NoDup_elements.
   - apply NoDup_app; repeat split; try apply NoDup_elements.
@@ -154,28 +154,28 @@ Proof.
 Qed.
 
 (** * Induction principles *)
-Lemma collection_wf : wf (⊂@{C}).
+Lemma set_wf : wf (⊂@{C}).
 Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
-Lemma collection_ind (P : C → Prop) :
+Lemma set_ind (P : C → Prop) :
   Proper ((≡) ==> iff) P →
   P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
 Proof.
   intros ? Hemp Hadd. apply well_founded_induction with (⊂).
-  { apply collection_wf. }
-  intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
+  { apply set_wf. }
+  intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX].
   - rewrite (union_difference {[ x ]} X) by set_solver.
     apply Hadd. set_solver. apply IH; set_solver.
   - by rewrite HX.
 Qed.
-Lemma collection_ind_L `{!LeibnizEquiv C} (P : C → Prop) :
+Lemma set_ind_L `{!LeibnizEquiv C} (P : C → Prop) :
   P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
-Proof. apply collection_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
+Proof. apply set_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
 
-(** * The [collection_fold] operation *)
-Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
+(** * The [set_fold] operation *)
+Lemma set_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
   Proper ((=) ==> (≡) ==> iff) P →
   P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
-  ∀ X, P (collection_fold f b X) X.
+  ∀ X, P (set_fold f b X) X.
 Proof.
   intros ? Hemp Hadd.
   cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X).
@@ -188,20 +188,20 @@ Proof.
     rewrite (union_difference {[ x ]} X) by set_solver.
     apply Hadd. set_solver. apply IH. set_solver.
 Qed.
-Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
+Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R}
     (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
     (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
-  Proper ((≡) ==> R) (collection_fold f b : C → B).
+  Proper ((≡) ==> R) (set_fold f b : C → B).
 Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
 
 (** * Minimal elements *)
 Lemma minimal_exists R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) :
   X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
 Proof.
-  pattern X; apply collection_ind; clear X.
+  pattern X; apply set_ind; clear X.
   { by intros X X' HX; setoid_rewrite HX. }
   { done. }
-  intros x X ? IH Hemp. destruct (collection_choose_or_empty X) as [[z ?]|HX].
+  intros x X ? IH Hemp. destruct (set_choose_or_empty X) as [[z ?]|HX].
   { destruct IH as (x' & Hx' & Hmin); [set_solver|].
     destruct (decide (R x x')).
     - exists x; split; [set_solver|].
@@ -222,8 +222,8 @@ Section filter.
 
   Lemma elem_of_filter X x : x ∈ filter P X ↔ P x ∧ x ∈ X.
   Proof.
-    unfold filter, collection_filter.
-    by rewrite elem_of_of_list, elem_of_list_filter, elem_of_elements.
+    unfold filter, set_filter.
+    by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
   Qed.
   Global Instance set_unfold_filter X Q :
     SetUnfold (x ∈ X) Q → SetUnfold (x ∈ filter P X) (P x ∧ Q).
@@ -255,34 +255,34 @@ End filter.
 
 (** * Map *)
 Section map.
-  Context `{Collection B D}.
+  Context `{Set_ B D}.
 
   Lemma elem_of_map (f : A → B) (X : C) y :
-    y ∈ collection_map (D:=D) f X ↔ ∃ x, y = f x ∧ x ∈ X.
+    y ∈ set_map (D:=D) f X ↔ ∃ x, y = f x ∧ x ∈ X.
   Proof.
-    unfold collection_map. rewrite elem_of_of_list, elem_of_list_fmap.
+    unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap.
     by setoid_rewrite elem_of_elements.
   Qed.
   Global Instance set_unfold_map (f : A → B) (X : C) (P : A → Prop) :
     (∀ y, SetUnfold (y ∈ X) (P y)) →
-    SetUnfold (x ∈ collection_map (D:=D) f X) (∃ y, x = f y ∧ P y).
+    SetUnfold (x ∈ set_map (D:=D) f X) (∃ y, x = f y ∧ P y).
   Proof. constructor. rewrite elem_of_map; naive_solver. Qed.
 
-  Global Instance collection_map_proper :
-    Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (collection_map (C:=C) (D:=D)).
+  Global Instance set_map_proper :
+    Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (set_map (C:=C) (D:=D)).
   Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
-  Global Instance collection_map_mono :
-    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (collection_map (C:=C) (D:=D)).
+  Global Instance set_map_mono :
+    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (set_map (C:=C) (D:=D)).
   Proof. intros f g ? X Y. set_unfold; naive_solver. Qed.
 
   Lemma elem_of_map_1 (f : A → B) (X : C) (y : B) :
-    y ∈ collection_map (D:=D) f X → ∃ x, y = f x ∧ x ∈ X.
+    y ∈ set_map (D:=D) f X → ∃ x, y = f x ∧ x ∈ X.
   Proof. set_solver. Qed.
   Lemma elem_of_map_2 (f : A → B) (X : C) (x : A) :
-    x ∈ X → f x ∈ collection_map (D:=D) f X.
+    x ∈ X → f x ∈ set_map (D:=D) f X.
   Proof. set_solver. Qed.
   Lemma elem_of_map_2_alt (f : A → B) (X : C) (x : A) (y : B) :
-    x ∈ X → y = f x → y ∈ collection_map (D:=D) f X.
+    x ∈ X → y = f x → y ∈ set_map (D:=D) f X.
   Proof. set_solver. Qed.
 End map.
 
@@ -321,4 +321,4 @@ Proof.
  refine (cast_if (decide (Exists P (elements X))));
    by rewrite set_Exists_elements.
 Defined.
-End fin_collection.
+End fin_set.
diff --git a/theories/gmap.v b/theories/gmap.v
index e7c9f9aba6e0f8fc7d6610a3f7cb768e9ee177bd..81958ea5d77888d554d26e4e09bf22306fe48b56 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -3,8 +3,8 @@
 (** This file implements finite maps and finite sets with keys of any countable
 type. The implementation is based on [Pmap]s, radix-2 search trees. *)
 From stdpp Require Export countable infinite fin_maps fin_map_dom.
-From stdpp Require Import pmap mapset set.
-Set Default Proof Using "Type".
+From stdpp Require Import pmap mapset propset.
+(* Set Default Proof Using "Type". *)
 
 (** * The data structure *)
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
@@ -116,11 +116,11 @@ Qed.
 Program Instance gmap_countable
     `{Countable K, Countable A} : Countable (gmap K A) := {
   encode m := encode (map_to_list m : list (K * A));
-  decode p := map_of_list <$> decode p
+  decode p := list_to_map <$> decode p
 }.
 Next Obligation.
   intros K ?? A ?? m; simpl. rewrite decode_encode; simpl.
-  by rewrite map_of_to_list.
+  by rewrite list_to_map_to_list.
 Qed.
 
 (** * Curry and uncurry *)
@@ -218,47 +218,48 @@ Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
 Instance gset_dom_spec `{Countable K} :
   FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
-Definition of_gset `{Countable A} (X : gset A) : set A := mkSet (λ x, x ∈ X).
-Lemma elem_of_of_gset `{Countable A} (X : gset A) x : x ∈ of_gset X ↔ x ∈ X.
+Definition gset_to_propset `{Countable A} (X : gset A) : propset A :=
+  {[ x | x ∈ X ]}.
+Lemma elem_of_gset_to_propset `{Countable A} (X : gset A) x : x ∈ gset_to_propset X ↔ x ∈ X.
 Proof. done. Qed.
 
-Definition to_gmap `{Countable K} {A} (x : A) (X : gset K) : gmap K A :=
+Definition gset_to_gmap `{Countable K} {A} (x : A) (X : gset K) : gmap K A :=
   (λ _, x) <$> mapset_car X.
 
-Lemma lookup_to_gmap `{Countable K} {A} (x : A) (X : gset K) i :
-  to_gmap x X !! i = guard (i ∈ X); Some x.
+Lemma lookup_gset_to_gmap `{Countable K} {A} (x : A) (X : gset K) i :
+  gset_to_gmap x X !! i = guard (i ∈ X); Some x.
 Proof.
-  destruct X as [X]; unfold to_gmap, elem_of, mapset_elem_of; simpl.
+  destruct X as [X]; unfold gset_to_gmap, elem_of, mapset_elem_of; simpl.
   rewrite lookup_fmap.
   case_option_guard; destruct (X !! i) as [[]|]; naive_solver.
 Qed.
-Lemma lookup_to_gmap_Some `{Countable K} {A} (x : A) (X : gset K) i y :
-  to_gmap x X !! i = Some y ↔ i ∈ X ∧ x = y.
-Proof. rewrite lookup_to_gmap. simplify_option_eq; naive_solver. Qed.
-Lemma lookup_to_gmap_None `{Countable K} {A} (x : A) (X : gset K) i :
-  to_gmap x X !! i = None ↔ i ∉ X.
-Proof. rewrite lookup_to_gmap. simplify_option_eq; naive_solver. Qed.
+Lemma lookup_gset_to_gmap_Some `{Countable K} {A} (x : A) (X : gset K) i y :
+  gset_to_gmap x X !! i = Some y ↔ i ∈ X ∧ x = y.
+Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
+Lemma lookup_gset_to_gmap_None `{Countable K} {A} (x : A) (X : gset K) i :
+  gset_to_gmap x X !! i = None ↔ i ∉ X.
+Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
 
-Lemma to_gmap_empty `{Countable K} {A} (x : A) : to_gmap x ∅ = ∅.
+Lemma gset_to_gmap_empty `{Countable K} {A} (x : A) : gset_to_gmap x ∅ = ∅.
 Proof. apply fmap_empty. Qed.
-Lemma to_gmap_union_singleton `{Countable K} {A} (x : A) i Y :
-  to_gmap x ({[ i ]} ∪ Y) = <[i:=x]>(to_gmap x Y).
+Lemma gset_to_gmap_union_singleton `{Countable K} {A} (x : A) i Y :
+  gset_to_gmap x ({[ i ]} ∪ Y) = <[i:=x]>(gset_to_gmap x Y).
 Proof.
   apply map_eq; intros j; apply option_eq; intros y.
-  rewrite lookup_insert_Some, !lookup_to_gmap_Some, elem_of_union,
+  rewrite lookup_insert_Some, !lookup_gset_to_gmap_Some, elem_of_union,
     elem_of_singleton; destruct (decide (i = j)); intuition.
 Qed.
 
-Lemma fmap_to_gmap `{Countable K} {A B} (f : A → B) (X : gset K) (x : A) :
-  f <$> to_gmap x X = to_gmap (f x) X.
+Lemma fmap_gset_to_gmap `{Countable K} {A B} (f : A → B) (X : gset K) (x : A) :
+  f <$> gset_to_gmap x X = gset_to_gmap (f x) X.
 Proof.
-  apply map_eq; intros j. rewrite lookup_fmap, !lookup_to_gmap.
+  apply map_eq; intros j. rewrite lookup_fmap, !lookup_gset_to_gmap.
   by simplify_option_eq.
 Qed.
-Lemma to_gmap_dom `{Countable K} {A B} (m : gmap K A) (y : B) :
-  to_gmap y (dom _ m) = const y <$> m.
+Lemma gset_to_gmap_dom `{Countable K} {A B} (m : gmap K A) (y : B) :
+  gset_to_gmap y (dom _ m) = const y <$> m.
 Proof.
-  apply map_eq; intros j. rewrite lookup_fmap, lookup_to_gmap.
+  apply map_eq; intros j. rewrite lookup_fmap, lookup_gset_to_gmap.
   destruct (m !! j) as [x|] eqn:?.
   - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
   - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 8af0dec025840f181366e83b3db7d47ac0c99eb4..b7b332fe4e61baf7422b9df47703e74f168e47e1 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -66,7 +66,7 @@ Proof.
 Qed.
 Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
 Proof. intros X Y. by rewrite gmultiset_eq. Qed.
-Global Instance gmultiset_equivalence : Equivalence (≡@{gmultiset A}).
+Global Instance gmultiset_equiv_equivalence : Equivalence (≡@{gmultiset A}).
 Proof. constructor; repeat intro; naive_solver. Qed.
 
 (* Multiplicity *)
@@ -90,11 +90,11 @@ Proof.
   destruct (X !! _), (Y !! _); simplify_option_eq; lia.
 Qed.
 
-(* Collection *)
+(* Set_ *)
 Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X.
 Proof. done. Qed.
 
-Global Instance gmultiset_simple_collection : SimpleCollection A (gmultiset A).
+Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
 Proof.
   split.
   - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
diff --git a/theories/hashset.v b/theories/hashset.v
index 48dd2ec71cf837d0c3816f7dcee94d94aa659f25..9494fe2ec5e3b0a1d11d0d73a8fc92bfbed07949 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -61,7 +61,7 @@ Qed.
 Global Instance hashset_elements: Elements A (hashset hash) := λ m,
   map_to_list (hashset_car m) ≫= snd.
 
-Global Instance hashset_fin_collection : FinCollection A (hashset hash).
+Global Instance hashset_fin_set : FinSet A (hashset hash).
 Proof.
   split; [split; [split| |]| |].
   - intros ? (?&?&?); simplify_map_eq/=.
diff --git a/theories/infinite.v b/theories/infinite.v
index 8125833f4cf3f61b050ac5b1e8bca521f938148e..ff94d49d18b3faf3d9186537109aa40320fcec7c 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -1,6 +1,6 @@
 (* Copyright (c) 2012-2019, Coq-std++ developers. *)
 (* This file is distributed under the terms of the BSD license. *)
-From stdpp Require Export fin_collections.
+From stdpp Require Export fin_sets.
 From stdpp Require Import pretty relations.
 
 (** The class [Infinite] axiomatizes types with infinitely many elements
@@ -47,7 +47,7 @@ Since [fresh_generic] is too inefficient for all practical purposes, we seal
 off its definition. That way, Coq will not accidentally unfold it during
 unification or other tactics. *)
 Section fresh_generic.
-  Context `{FinCollection A C, Infinite A, !RelDecision (∈@{C})}.
+  Context `{FinSet A C, Infinite A, !RelDecision (∈@{C})}.
 
   Definition fresh_generic_body (s : C) (rec : ∀ s', s' ⊂ s → nat → A) (n : nat) : A :=
     let cand := inject n in
@@ -57,7 +57,7 @@ Section fresh_generic.
     end.
 
   Definition fresh_generic_fix_aux :
-    seal (Fix collection_wf (const (nat → A)) fresh_generic_body). by eexists. Qed.
+    seal (Fix set_wf (const (nat → A)) fresh_generic_body). by eexists. Qed.
   Definition fresh_generic_fix := fresh_generic_fix_aux.(unseal).
 
   Lemma fresh_generic_fixpoint_unfold s n:
@@ -73,7 +73,7 @@ Section fresh_generic.
          ∀ i, n ≤ i < m → inject i ∈ s.
   Proof.
     revert n.
-    induction s as [s IH] using (well_founded_ind collection_wf); intros n.
+    induction s as [s IH] using (well_founded_ind set_wf); intros n.
     setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body.
     destruct decide as [Hcase|Hcase]; [|by eauto with lia].
     destruct (IH _ (subset_difference_elem_of Hcase) (S n))
diff --git a/theories/listset.v b/theories/listset.v
index 0d864ce8f584415ec0d022a9856bd0ecd92dc480..d6c0926ffe4b5b505c3c235dad47471b7633e75e 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements finite set as unordered lists without duplicates
 removed. This implementation forms a monad. *)
-From stdpp Require Export collections list.
+From stdpp Require Export sets list.
 Set Default Proof Using "Type".
 
 Record listset A := Listset { listset_car: list A }.
@@ -19,7 +19,7 @@ Global Instance listset_union: Union (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (l' ++ k').
 Global Opaque listset_singleton listset_empty.
 
-Global Instance listset_simple_collection : SimpleCollection A (listset A).
+Global Instance listset_simple_set : SemiSet A (listset A).
 Proof.
   split.
   - by apply not_elem_of_nil.
@@ -50,7 +50,7 @@ Global Instance listset_intersection: Intersection (listset A) := λ l k,
 Global Instance listset_difference: Difference (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (list_difference l' k').
 
-Instance listset_collection: Collection A (listset A).
+Instance listset_set: Set_ A (listset A).
 Proof.
   split.
   - apply _.
@@ -59,7 +59,7 @@ Proof.
 Qed.
 Global Instance listset_elements: Elements A (listset A) :=
   remove_dups ∘ listset_car.
-Global Instance listset_fin_collection : FinCollection A (listset A).
+Global Instance listset_fin_set : FinSet A (listset A).
 Proof.
   split.
   - apply _.
@@ -75,7 +75,7 @@ Instance listset_bind: MBind listset := λ A B f l,
   let (l') := l in Listset (mbind (listset_car ∘ f) l').
 Instance listset_join: MJoin listset := λ A, mbind id.
 
-Instance listset_collection_monad : CollectionMonad listset.
+Instance listset_set_monad : MonadSet listset.
 Proof.
   split.
   - intros. apply _.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index a4835acaac8a2149bea0d42cc8bf5a6240a5ee27..4c7e681070814736bb39a9cf3c814813d8a3b0f2 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -3,7 +3,7 @@
 (** This file implements finite as unordered lists without duplicates.
 Although this implementation is slow, it is very useful as decidable equality
 is the only constraint on the carrier set. *)
-From stdpp Require Export collections list.
+From stdpp Require Export sets list.
 Set Default Proof Using "Type".
 
 Record listset_nodup A := ListsetNoDup {
@@ -13,7 +13,7 @@ Arguments ListsetNoDup {_} _ _ : assert.
 Arguments listset_nodup_car {_} _ : assert.
 Arguments listset_nodup_prf {_} _ : assert.
 
-Section list_collection.
+Section list_set.
 Context `{EqDecision A}.
 Notation C := (listset_nodup A).
 
@@ -31,7 +31,7 @@ Instance listset_nodup_difference: Difference C := λ l k,
   let (l',Hl) := l in let (k',Hk) := k
   in ListsetNoDup _ (NoDup_list_difference _ k' Hl).
 
-Instance: Collection A C.
+Instance: Set_ A C.
 Proof.
   split; [split | | ].
   - by apply not_elem_of_nil.
@@ -42,9 +42,9 @@ Proof.
 Qed.
 
 Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
-Global Instance: FinCollection A C.
+Global Instance: FinSet A C.
 Proof. split. apply _. done. by intros [??]. Qed.
-End list_collection.
+End list_set.
 
 Hint Extern 1 (ElemOf _ (listset_nodup _)) =>
   eapply @listset_nodup_elem_of : typeclass_instances.
diff --git a/theories/mapset.v b/theories/mapset.v
index bb60accbbe0220baf72d4111843639aac1ebf973..72482ace2466ebe3e37a8049e7a88061cd55c83f 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -35,7 +35,7 @@ Proof.
   f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E.
 Qed.
 
-Instance mapset_collection: Collection K (mapset M).
+Instance mapset_set: Set_ K (mapset M).
 Proof.
   split; [split | | ].
   - unfold empty, elem_of, mapset_empty, mapset_elem_of.
@@ -56,7 +56,7 @@ Proof.
 Qed.
 Global Instance mapset_leibniz : LeibnizEquiv (mapset M).
 Proof. intros ??. apply mapset_eq. Qed.
-Global Instance mapset_fin_collection : FinCollection K (mapset M).
+Global Instance mapset_fin_set : FinSet K (mapset M).
 Proof.
   split.
   - apply _.
diff --git a/theories/natmap.v b/theories/natmap.v
index bc68edd6e8bb629889fd692998b0a86e465292c6..5d356484a3465e17e0c717bccc07c1859138e5e7 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -260,39 +260,39 @@ Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
 Instance: FinMapDom nat natmap natset := mapset_dom_spec.
 
 (* Fixpoint avoids this definition from being unfolded *)
-Fixpoint of_bools (βs : list bool) : natset :=
+Fixpoint bools_to_natset (βs : list bool) : natset :=
   let f (β : bool) := if β then Some () else None in
   Mapset $ list_to_natmap $ f <$> βs.
-Definition to_bools (sz : nat) (X : natset) : list bool :=
+Definition natset_to_bools (sz : nat) (X : natset) : list bool :=
   let f (mu : option ()) := match mu with Some _ => true | None => false end in
   resize sz false $ f <$> natmap_car (mapset_car X).
 
-Lemma of_bools_unfold βs :
+Lemma bools_to_natset_unfold βs :
   let f (β : bool) := if β then Some () else None in
-  of_bools βs = Mapset $ list_to_natmap $ f <$> βs.
+  bools_to_natset βs = Mapset $ list_to_natmap $ f <$> βs.
 Proof. by destruct βs. Qed.
-Lemma elem_of_of_bools βs i : i ∈ of_bools βs ↔ βs !! i = Some true.
+Lemma elem_of_bools_to_natset βs i : i ∈ bools_to_natset βs ↔ βs !! i = Some true.
 Proof.
-  rewrite of_bools_unfold; unfold elem_of, mapset_elem_of; simpl.
+  rewrite bools_to_natset_unfold; unfold elem_of, mapset_elem_of; simpl.
   rewrite list_to_natmap_spec, list_lookup_fmap.
   destruct (βs !! i) as [[]|]; compute; intuition congruence.
 Qed.
-Lemma of_bools_union βs1 βs2 :
+Lemma bools_to_natset_union βs1 βs2 :
   length βs1 = length βs2 →
-  of_bools (βs1 ||* βs2) = of_bools βs1 ∪ of_bools βs2.
+  bools_to_natset (βs1 ||* βs2) = bools_to_natset βs1 ∪ bools_to_natset βs2.
 Proof.
   rewrite <-Forall2_same_length; intros Hβs.
-  apply elem_of_equiv_L. intros i. rewrite elem_of_union, !elem_of_of_bools.
+  apply elem_of_equiv_L. intros i. rewrite elem_of_union, !elem_of_bools_to_natset.
   revert i. induction Hβs as [|[] []]; intros [|?]; naive_solver.
 Qed.
-Lemma to_bools_length (X : natset) sz : length (to_bools sz X) = sz.
+Lemma natset_to_bools_length (X : natset) sz : length (natset_to_bools sz X) = sz.
 Proof. apply resize_length. Qed.
-Lemma lookup_to_bools_ge sz X i : sz ≤ i → to_bools sz X !! i = None.
+Lemma lookup_natset_to_bools_ge sz X i : sz ≤ i → natset_to_bools sz X !! i = None.
 Proof. by apply lookup_resize_old. Qed.
-Lemma lookup_to_bools sz X i β :
-  i < sz → to_bools sz X !! i = Some β ↔ (i ∈ X ↔ β = true).
+Lemma lookup_natset_to_bools sz X i β :
+  i < sz → natset_to_bools sz X !! i = Some β ↔ (i ∈ X ↔ β = true).
 Proof.
-  unfold to_bools, elem_of, mapset_elem_of, lookup at 2, natmap_lookup; simpl.
+  unfold natset_to_bools, elem_of, mapset_elem_of, lookup at 2, natmap_lookup; simpl.
   intros. destruct (mapset_car X) as [l ?]; simpl.
   destruct (l !! i) as [mu|] eqn:Hmu; simpl.
   { rewrite lookup_resize, list_lookup_fmap, Hmu
@@ -301,30 +301,31 @@ Proof.
   rewrite lookup_resize_new by (rewrite ?fmap_length;
     eauto using lookup_ge_None_1); destruct β; intuition congruence.
 Qed.
-Lemma lookup_to_bools_true sz X i :
-  i < sz → to_bools sz X !! i = Some true ↔ i ∈ X.
-Proof. intros. rewrite lookup_to_bools by done. intuition. Qed.
-Lemma lookup_to_bools_false sz X i :
-  i < sz → to_bools sz X !! i = Some false ↔ i ∉ X.
-Proof. intros. rewrite lookup_to_bools by done. naive_solver. Qed.
-Lemma to_bools_union sz X1 X2 :
-  to_bools sz (X1 ∪ X2) = to_bools sz X1 ||* to_bools sz X2.
+Lemma lookup_natset_to_bools_true sz X i :
+  i < sz → natset_to_bools sz X !! i = Some true ↔ i ∈ X.
+Proof. intros. rewrite lookup_natset_to_bools by done. intuition. Qed.
+Lemma lookup_natset_to_bools_false sz X i :
+  i < sz → natset_to_bools sz X !! i = Some false ↔ i ∉ X.
+Proof. intros. rewrite lookup_natset_to_bools by done. naive_solver. Qed.
+Lemma natset_to_bools_union sz X1 X2 :
+  natset_to_bools sz (X1 ∪ X2) = natset_to_bools sz X1 ||* natset_to_bools sz X2.
 Proof.
   apply list_eq; intros i; rewrite lookup_zip_with.
-  destruct (decide (i < sz)); [|by rewrite !lookup_to_bools_ge by lia].
+  destruct (decide (i < sz)); [|by rewrite !lookup_natset_to_bools_ge by lia].
   apply option_eq; intros β.
-  rewrite lookup_to_bools, elem_of_union by done; intros.
+  rewrite lookup_natset_to_bools, elem_of_union by done; intros.
   destruct (decide (i ∈ X1)), (decide (i ∈ X2)); repeat first
-    [ rewrite (λ X H, proj2 (lookup_to_bools_true sz X i H)) by done
-    | rewrite (λ X H, proj2 (lookup_to_bools_false sz X i H)) by done];
+    [ rewrite (λ X H, proj2 (lookup_natset_to_bools_true sz X i H)) by done
+    | rewrite (λ X H, proj2 (lookup_natset_to_bools_false sz X i H)) by done];
     destruct β; naive_solver.
 Qed.
-Lemma to_of_bools βs sz : to_bools sz (of_bools βs) = resize sz false βs.
+Lemma natset_to_bools_to_natset βs sz :
+  natset_to_bools sz (bools_to_natset βs) = resize sz false βs.
 Proof.
   apply list_eq; intros i. destruct (decide (i < sz));
-    [|by rewrite lookup_to_bools_ge, lookup_resize_old by lia].
+    [|by rewrite lookup_natset_to_bools_ge, lookup_resize_old by lia].
   apply option_eq; intros β.
-  rewrite lookup_to_bools, elem_of_of_bools by done.
+  rewrite lookup_natset_to_bools, elem_of_bools_to_natset by done.
   destruct (decide (i < length βs)).
   { rewrite lookup_resize by done.
     destruct (lookup_lt_is_Some_2 βs i) as [[]]; destruct β; naive_solver. }
diff --git a/theories/pmap.v b/theories/pmap.v
index db46a61093cd2c9617b96803ccd0e29489200b94..994f8f95bf5c3120cfe3e151d08361e17cadb1a8 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -303,10 +303,10 @@ Qed.
 
 Program Instance Pmap_countable `{Countable A} : Countable (Pmap A) := {
   encode m := encode (map_to_list m : list (positive * A));
-  decode p := map_of_list <$> decode p
+  decode p := list_to_map <$> decode p
 }.
 Next Obligation.
-  intros A ?? m; simpl. rewrite decode_encode; simpl. by rewrite map_of_to_list.
+  intros A ?? m; simpl. rewrite decode_encode; simpl. by rewrite list_to_map_to_list.
 Qed.
 
 (** * Finite sets *)
diff --git a/theories/prelude.v b/theories/prelude.v
index fc2ea9d3cc23426ee7cf1413c6b80ccf717d5824..15b8d99042cbedad59dbe4be60b08bc86b2d2d00 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -8,8 +8,8 @@ From stdpp Require Export
   vector
   numbers
   relations
-  collections
-  fin_collections
+  sets
+  fin_sets
   listset
   list
   lexico.
diff --git a/theories/propset.v b/theories/propset.v
new file mode 100644
index 0000000000000000000000000000000000000000..f4a20ce187ef2524a2f1aee9d7d2ca521c5661de
--- /dev/null
+++ b/theories/propset.v
@@ -0,0 +1,55 @@
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file implements sets as functions into Prop. *)
+From stdpp Require Export sets.
+Set Default Proof Using "Type".
+
+Record propset (A : Type) : Type := PropSet { propset_car : A → Prop }.
+Add Printing Constructor propset.
+Arguments PropSet {_} _ : assert.
+Arguments propset_car {_} _ _ : assert.
+Notation "{[ x | P ]}" := (PropSet (λ x, P))
+  (at level 1, format "{[  x  |  P  ]}") : stdpp_scope.
+
+Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.
+
+Instance propset_top {A} : Top (propset A) := {[ _ | True ]}.
+Instance propset_empty {A} : Empty (propset A) := {[ _ | False ]}.
+Instance propset_singleton {A} : Singleton A (propset A) := λ y, {[ x | y = x ]}.
+Instance propset_union {A} : Union (propset A) := λ X1 X2, {[ x | x ∈ X1 ∨ x ∈ X2 ]}.
+Instance propset_intersection {A} : Intersection (propset A) := λ X1 X2,
+  {[ x | x ∈ X1 ∧ x ∈ X2 ]}.
+Instance propset_difference {A} : Difference (propset A) := λ X1 X2,
+  {[ x | x ∈ X1 ∧ x ∉ X2 ]}.
+Instance propset_set : Set_ A (propset A).
+Proof. split; [split | |]; by repeat intro. Qed.
+
+Lemma elem_of_top {A} (x : A) : x ∈ (⊤ : propset A) ↔ True.
+Proof. done. Qed.
+Lemma elem_of_PropSet {A} (P : A → Prop) x : x ∈ {[ x | P x ]} ↔ P x.
+Proof. done. Qed.
+Lemma not_elem_of_PropSet {A} (P : A → Prop) x : x ∉ {[ x | P x ]} ↔ ¬P x.
+Proof. done. Qed.
+Lemma top_subseteq {A} (X : propset A) : X ⊆ ⊤.
+Proof. done. Qed.
+Hint Resolve top_subseteq : core.
+
+Instance propset_ret : MRet propset := λ A (x : A), {[ x ]}.
+Instance propset_bind : MBind propset := λ A B (f : A → propset B) (X : propset A),
+  PropSet (λ b, ∃ a, b ∈ f a ∧ a ∈ X).
+Instance propset_fmap : FMap propset := λ A B (f : A → B) (X : propset A),
+  {[ b | ∃ a, b = f a ∧ a ∈ X ]}.
+Instance propset_join : MJoin propset := λ A (XX : propset (propset A)),
+  {[ a | ∃ X : propset A, a ∈ X ∧ X ∈ XX ]}.
+Instance propset_monad_set : MonadSet propset.
+Proof. by split; try apply _. Qed.
+
+Instance set_unfold_propset_top {A} (x : A) : SetUnfold (x ∈ (⊤ : propset A)) True.
+Proof. by constructor. Qed.
+Instance set_unfold_PropSet {A} (P : A → Prop) x Q :
+  SetUnfoldSimpl (P x) Q → SetUnfold (x ∈ PropSet P) Q.
+Proof. intros HPQ. constructor. apply HPQ. Qed.
+
+Global Opaque propset_elem_of propset_top propset_empty propset_singleton.
+Global Opaque propset_union propset_intersection propset_difference.
+Global Opaque propset_ret propset_bind propset_fmap propset_join.
diff --git a/theories/set.v b/theories/set.v
deleted file mode 100644
index a823d705526d0bb1f8a9c4e519cc39c6126138a1..0000000000000000000000000000000000000000
--- a/theories/set.v
+++ /dev/null
@@ -1,55 +0,0 @@
-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
-(** This file implements sets as functions into Prop. *)
-From stdpp Require Export collections.
-Set Default Proof Using "Type".
-
-Record set (A : Type) : Type := mkSet { set_car : A → Prop }.
-Add Printing Constructor set.
-Arguments mkSet {_} _ : assert.
-Arguments set_car {_} _ _ : assert.
-Notation "{[ x | P ]}" := (mkSet (λ x, P))
-  (at level 1, format "{[  x  |  P  ]}") : stdpp_scope.
-
-Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x.
-
-Instance set_top {A} : Top (set A) := {[ _ | True ]}.
-Instance set_empty {A} : Empty (set A) := {[ _ | False ]}.
-Instance set_singleton {A} : Singleton A (set A) := λ y, {[ x | y = x ]}.
-Instance set_union {A} : Union (set A) := λ X1 X2, {[ x | x ∈ X1 ∨ x ∈ X2 ]}.
-Instance set_intersection {A} : Intersection (set A) := λ X1 X2,
-  {[ x | x ∈ X1 ∧ x ∈ X2 ]}.
-Instance set_difference {A} : Difference (set A) := λ X1 X2,
-  {[ x | x ∈ X1 ∧ x ∉ X2 ]}.
-Instance set_collection : Collection A (set A).
-Proof. split; [split | |]; by repeat intro. Qed.
-
-Lemma elem_of_top {A} (x : A) : x ∈ (⊤ : set A) ↔ True.
-Proof. done. Qed.
-Lemma elem_of_mkSet {A} (P : A → Prop) x : x ∈ {[ x | P x ]} ↔ P x.
-Proof. done. Qed.
-Lemma not_elem_of_mkSet {A} (P : A → Prop) x : x ∉ {[ x | P x ]} ↔ ¬P x.
-Proof. done. Qed.
-Lemma top_subseteq {A} (X : set A) : X ⊆ ⊤.
-Proof. done. Qed.
-Hint Resolve top_subseteq : core.
-
-Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
-Instance set_bind : MBind set := λ A B (f : A → set B) (X : set A),
-  mkSet (λ b, ∃ a, b ∈ f a ∧ a ∈ X).
-Instance set_fmap : FMap set := λ A B (f : A → B) (X : set A),
-  {[ b | ∃ a, b = f a ∧ a ∈ X ]}.
-Instance set_join : MJoin set := λ A (XX : set (set A)),
-  {[ a | ∃ X : set A, a ∈ X ∧ X ∈ XX ]}.
-Instance set_collection_monad : CollectionMonad set.
-Proof. by split; try apply _. Qed.
-
-Instance set_unfold_set_all {A} (x : A) : SetUnfold (x ∈ (⊤ : set A)) True.
-Proof. by constructor. Qed.
-Instance set_unfold_mkSet {A} (P : A → Prop) x Q :
-  SetUnfoldSimpl (P x) Q → SetUnfold (x ∈ mkSet P) Q.
-Proof. intros HPQ. constructor. apply HPQ. Qed.
-
-Global Opaque set_elem_of set_top set_empty set_singleton.
-Global Opaque set_union set_intersection set_difference.
-Global Opaque set_ret set_bind set_fmap set_join.
diff --git a/theories/collections.v b/theories/sets.v
similarity index 88%
rename from theories/collections.v
rename to theories/sets.v
index 170507b0025cd4921e2060936f4f2ffcae50e196..d9c06d42d76d9c626d753995140d462f55a6cc25 100644
--- a/theories/collections.v
+++ b/theories/sets.v
@@ -1,27 +1,27 @@
 (* Copyright (c) 2012-2019, Coq-std++ developers. *)
 (* This file is distributed under the terms of the BSD license. *)
-(** This file collects definitions and theorems on collections. Most
+(** This file collects definitions and theorems on sets. Most
 importantly, it implements some tactics to automatically solve goals involving
-collections. *)
+sets. *)
 From stdpp Require Export orders list.
 (* FIXME: This file needs a 'Proof Using' hint, but the default we use
    everywhere makes for lots of extra ssumptions. *)
 
 (* Higher precedence to make sure these instances are not used for other types
 with an [ElemOf] instance, such as lists. *)
-Instance collection_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
+Instance set_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
   ∀ x, x ∈ X ↔ x ∈ Y.
-Instance collection_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
+Instance set_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y.
-Instance collection_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
+Instance set_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y → False.
-Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
+Typeclasses Opaque set_equiv set_subseteq set_disjoint.
 
 (** * Setoids *)
 Section setoids_simple.
-  Context `{SimpleCollection A C}.
+  Context `{SemiSet A C}.
 
-  Global Instance collection_equivalence : Equivalence (≡@{C}).
+  Global Instance set_equiv_equivalence : Equivalence (≡@{C}).
   Proof.
     split.
     - done.
@@ -47,7 +47,7 @@ Section setoids_simple.
 End setoids_simple.
 
 Section setoids.
-  Context `{Collection A C}.
+  Context `{Set_ A C}.
 
   (** * Setoids *)
   Global Instance intersection_proper :
@@ -63,21 +63,21 @@ Section setoids.
 End setoids.
 
 Section setoids_monad.
-  Context `{CollectionMonad M}.
+  Context `{MonadSet M}.
 
-  Global Instance collection_fmap_proper {A B} :
+  Global Instance set_fmap_proper {A B} :
     Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B).
   Proof.
     intros f1 f2 Hf X1 X2 HX x. rewrite !elem_of_fmap. f_equiv; intros z.
     by rewrite HX, Hf.
   Qed.
-  Global Instance collection_bind_proper {A B} :
+  Global Instance set_bind_proper {A B} :
     Proper (pointwise_relation _ (≡) ==> (≡) ==> (≡)) (@mbind M _ A B).
   Proof.
     intros f1 f2 Hf X1 X2 HX x. rewrite !elem_of_bind. f_equiv; intros z.
     by rewrite HX, (Hf z).
   Qed.
-  Global Instance collection_join_proper {A} :
+  Global Instance set_join_proper {A} :
     Proper ((≡) ==> (≡)) (@mjoin M _ A).
   Proof.
     intros X1 X2 HX x. rewrite !elem_of_join. f_equiv; intros z. by rewrite HX.
@@ -142,7 +142,7 @@ Hint Extern 0 (SetUnfold (∃ _, _) _) =>
   class_apply set_unfold_exist : typeclass_instances.
 
 Section set_unfold_simple.
-  Context `{SimpleCollection A C}.
+  Context `{SemiSet A C}.
   Implicit Types x y : A.
   Implicit Types X Y : C.
 
@@ -161,13 +161,13 @@ Section set_unfold_simple.
   Global Instance set_unfold_equiv_empty_l X (P : A → Prop) :
     (∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (∅ ≡ X) (∀ x, ¬P x) | 5.
   Proof.
-    intros ?; constructor. unfold equiv, collection_equiv.
+    intros ?; constructor. unfold equiv, set_equiv.
     pose proof (not_elem_of_empty (C:=C)); naive_solver.
   Qed.
   Global Instance set_unfold_equiv_empty_r (P : A → Prop) X :
     (∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (X ≡ ∅) (∀ x, ¬P x) | 5.
   Proof.
-    intros ?; constructor. unfold equiv, collection_equiv.
+    intros ?; constructor. unfold equiv, set_equiv.
     pose proof (not_elem_of_empty (C:=C)); naive_solver.
   Qed.
   Global Instance set_unfold_equiv (P Q : A → Prop) X :
@@ -188,7 +188,7 @@ Section set_unfold_simple.
   Global Instance set_unfold_disjoint (P Q : A → Prop) X Y :
     (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
     SetUnfold (X ## Y) (∀ x, P x → Q x → False).
-  Proof. constructor. unfold disjoint, collection_disjoint. naive_solver. Qed.
+  Proof. constructor. unfold disjoint, set_disjoint. naive_solver. Qed.
 
   Context `{!LeibnizEquiv C}.
   Global Instance set_unfold_equiv_same_L X : SetUnfold (X = X) True | 1.
@@ -206,7 +206,7 @@ Section set_unfold_simple.
 End set_unfold_simple.
 
 Section set_unfold.
-  Context `{Collection A C}.
+  Context `{Set_ A C}.
   Implicit Types x y : A.
   Implicit Types X Y : C.
 
@@ -225,7 +225,7 @@ Section set_unfold.
 End set_unfold.
 
 Section set_unfold_monad.
-  Context `{CollectionMonad M}.
+  Context `{MonadSet M}.
 
   Global Instance set_unfold_ret {A} (x y : A) :
     SetUnfold (x ∈ mret (M:=M) y) (x = y).
@@ -303,9 +303,9 @@ Hint Extern 1000 (_ ∈ _) => set_solver : set_solver.
 Hint Extern 1000 (_ ⊆ _) => set_solver : set_solver.
 
 
-(** * Collections with [∪], [∅] and [{[_]}] *)
-Section simple_collection.
-  Context `{SimpleCollection A C}.
+(** * Sets with [∪], [∅] and [{[_]}] *)
+Section semi_set.
+  Context `{SemiSet A C}.
   Implicit Types x y : A.
   Implicit Types X Y : C.
   Implicit Types Xs Ys : list C.
@@ -313,14 +313,14 @@ Section simple_collection.
   (** Equality *)
   Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
   Proof. set_solver. Qed.
-  Lemma collection_equiv_spec X Y : X ≡ Y ↔ X ⊆ Y ∧ Y ⊆ X.
+  Lemma set_equiv_spec X Y : X ≡ Y ↔ X ⊆ Y ∧ Y ⊆ X.
   Proof. set_solver. Qed.
 
   (** Subset relation *)
-  Global Instance collection_subseteq_antisymm: AntiSymm (≡) (⊆@{C}).
+  Global Instance set_subseteq_antisymm: AntiSymm (≡) (⊆@{C}).
   Proof. intros ??. set_solver. Qed.
 
-  Global Instance collection_subseteq_preorder: PreOrder (⊆@{C}).
+  Global Instance set_subseteq_preorder: PreOrder (⊆@{C}).
   Proof. split. by intros ??. intros ???; set_solver. Qed.
 
   Lemma subseteq_union X Y : X ⊆ Y ↔ X ∪ Y ≡ Y.
@@ -465,11 +465,11 @@ Section simple_collection.
 
     Lemma elem_of_equiv_L X Y : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
     Proof. unfold_leibniz. apply elem_of_equiv. Qed.
-    Lemma collection_equiv_spec_L X Y : X = Y ↔ X ⊆ Y ∧ Y ⊆ X.
-    Proof. unfold_leibniz. apply collection_equiv_spec. Qed.
+    Lemma set_equiv_spec_L X Y : X = Y ↔ X ⊆ Y ∧ Y ⊆ X.
+    Proof. unfold_leibniz. apply set_equiv_spec. Qed.
 
     (** Subset relation *)
-    Global Instance collection_subseteq_partialorder : PartialOrder (⊆@{C}).
+    Global Instance set_subseteq_partialorder : PartialOrder (⊆@{C}).
     Proof. split. apply _. intros ??. unfold_leibniz. apply (anti_symm _). Qed.
 
     Lemma subseteq_union_L X Y : X ⊆ Y ↔ X ∪ Y = Y.
@@ -528,9 +528,9 @@ Section simple_collection.
 
   Section dec.
     Context `{!RelDecision (≡@{C})}.
-    Lemma collection_subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y.
+    Lemma set_subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y.
     Proof. destruct (decide (X ≡ Y)); [by right|left;set_solver]. Qed.
-    Lemma collection_not_subset_inv X Y : X ⊄ Y → X ⊈ Y ∨ X ≡ Y.
+    Lemma set_not_subset_inv X Y : X ⊄ Y → X ⊈ Y ∨ X ≡ Y.
     Proof. destruct (decide (X ≡ Y)); [by right|left;set_solver]. Qed.
 
     Lemma non_empty_union X Y : X ∪ Y ≢ ∅ ↔ X ≢ ∅ ∨ Y ≢ ∅.
@@ -539,21 +539,21 @@ Section simple_collection.
     Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
 
     Context `{!LeibnizEquiv C}.
-    Lemma collection_subseteq_inv_L X Y : X ⊆ Y → X ⊂ Y ∨ X = Y.
-    Proof. unfold_leibniz. apply collection_subseteq_inv. Qed.
-    Lemma collection_not_subset_inv_L X Y : X ⊄ Y → X ⊈ Y ∨ X = Y.
-    Proof. unfold_leibniz. apply collection_not_subset_inv. Qed.
+    Lemma set_subseteq_inv_L X Y : X ⊆ Y → X ⊂ Y ∨ X = Y.
+    Proof. unfold_leibniz. apply set_subseteq_inv. Qed.
+    Lemma set_not_subset_inv_L X Y : X ⊄ Y → X ⊈ Y ∨ X = Y.
+    Proof. unfold_leibniz. apply set_not_subset_inv. Qed.
     Lemma non_empty_union_L X Y : X ∪ Y ≠ ∅ ↔ X ≠ ∅ ∨ Y ≠ ∅.
     Proof. unfold_leibniz. apply non_empty_union. Qed.
     Lemma non_empty_union_list_L Xs : ⋃ Xs ≠ ∅ → Exists (≠ ∅) Xs.
     Proof. unfold_leibniz. apply non_empty_union_list. Qed.
   End dec.
-End simple_collection.
+End semi_set.
 
 
-(** * Collections with [∪], [∩], [∖], [∅] and [{[_]}] *)
-Section collection.
-  Context `{Collection A C}.
+(** * Sets with [∪], [∩], [∖], [∅] and [{[_]}] *)
+Section set.
+  Context `{Set_ A C}.
   Implicit Types x y : A.
   Implicit Types X Y : C.
 
@@ -744,68 +744,68 @@ Section collection.
       {[x]} ∪ (X ∖ Y) = ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
     Proof. unfold_leibniz. apply singleton_union_difference. Qed.
   End dec.
-End collection.
+End set.
 
 
 (** * Conversion of option and list *)
-Definition of_option `{Singleton A C, Empty C} (mx : option A) : C :=
+Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C :=
   match mx with None => ∅ | Some x => {[ x ]} end.
-Fixpoint of_list `{Singleton A C, Empty C, Union C} (l : list A) : C :=
-  match l with [] => ∅ | x :: l => {[ x ]} ∪ of_list l end.
+Fixpoint list_to_set `{Singleton A C, Empty C, Union C} (l : list A) : C :=
+  match l with [] => ∅ | x :: l => {[ x ]} ∪ list_to_set l end.
 
-Section of_option_list.
-  Context `{SimpleCollection A C}.
+Section option_and_list_to_set.
+  Context `{SemiSet A C}.
   Implicit Types l : list A.
 
-  Lemma elem_of_of_option (x : A) mx: x ∈ of_option (C:=C) mx ↔ mx = Some x.
+  Lemma elem_of_option_to_set (x : A) mx: x ∈ option_to_set (C:=C) mx ↔ mx = Some x.
   Proof. destruct mx; set_solver. Qed.
-  Lemma not_elem_of_of_option (x : A) mx: x ∉ of_option (C:=C) mx ↔ mx ≠ Some x.
-  Proof. by rewrite elem_of_of_option. Qed.
+  Lemma not_elem_of_option_to_set (x : A) mx: x ∉ option_to_set (C:=C) mx ↔ mx ≠ Some x.
+  Proof. by rewrite elem_of_option_to_set. Qed.
 
-  Lemma elem_of_of_list (x : A) l : x ∈ of_list (C:=C) l ↔ x ∈ l.
+  Lemma elem_of_list_to_set (x : A) l : x ∈ list_to_set (C:=C) l ↔ x ∈ l.
   Proof.
     split.
     - induction l; simpl; [by rewrite elem_of_empty|].
       rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto.
     - induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
   Qed.
-  Lemma not_elem_of_of_list (x : A) l : x ∉ of_list (C:=C) l ↔ x ∉ l.
-  Proof. by rewrite elem_of_of_list. Qed.
+  Lemma not_elem_of_list_to_set (x : A) l : x ∉ list_to_set (C:=C) l ↔ x ∉ l.
+  Proof. by rewrite elem_of_list_to_set. Qed.
 
-  Global Instance set_unfold_of_option (mx : option A) x :
-    SetUnfold (x ∈ of_option (C:=C) mx) (mx = Some x).
-  Proof. constructor; apply elem_of_of_option. Qed.
-  Global Instance set_unfold_of_list (l : list A) x P :
-    SetUnfold (x ∈ l) P → SetUnfold (x ∈ of_list (C:=C) l) P.
-  Proof. constructor. by rewrite elem_of_of_list, (set_unfold (x ∈ l) P). Qed.
+  Global Instance set_unfold_option_to_set (mx : option A) x :
+    SetUnfold (x ∈ option_to_set (C:=C) mx) (mx = Some x).
+  Proof. constructor; apply elem_of_option_to_set. Qed.
+  Global Instance set_unfold_list_to_set (l : list A) x P :
+    SetUnfold (x ∈ l) P → SetUnfold (x ∈ list_to_set (C:=C) l) P.
+  Proof. constructor. by rewrite elem_of_list_to_set, (set_unfold (x ∈ l) P). Qed.
 
-  Lemma of_list_nil : of_list [] =@{C} ∅.
+  Lemma list_to_set_nil : list_to_set [] =@{C} ∅.
   Proof. done. Qed.
-  Lemma of_list_cons x l : of_list (x :: l) =@{C} {[ x ]} ∪ of_list l.
+  Lemma list_to_set_cons x l : list_to_set (x :: l) =@{C} {[ x ]} ∪ list_to_set l.
   Proof. done. Qed.
-  Lemma of_list_app l1 l2 : of_list (l1 ++ l2) ≡@{C} of_list l1 ∪ of_list l2.
+  Lemma list_to_set_app l1 l2 : list_to_set (l1 ++ l2) ≡@{C} list_to_set l1 ∪ list_to_set l2.
   Proof. set_solver. Qed.
-  Global Instance of_list_perm : Proper ((≡ₚ) ==> (≡)) (of_list (C:=C)).
+  Global Instance list_to_set_perm : Proper ((≡ₚ) ==> (≡)) (list_to_set (C:=C)).
   Proof. induction 1; set_solver. Qed.
 
   Context `{!LeibnizEquiv C}.
-  Lemma of_list_app_L l1 l2 : of_list (l1 ++ l2) =@{C} of_list l1 ∪ of_list l2.
+  Lemma list_to_set_app_L l1 l2 : list_to_set (l1 ++ l2) =@{C} list_to_set l1 ∪ list_to_set l2.
   Proof. set_solver. Qed.
-  Global Instance of_list_perm_L : Proper ((≡ₚ) ==> (=)) (of_list (C:=C)).
+  Global Instance list_to_set_perm_L : Proper ((≡ₚ) ==> (=)) (list_to_set (C:=C)).
   Proof. induction 1; set_solver. Qed.
-End of_option_list.
+End option_and_list_to_set.
 
 
 (** * Guard *)
-Global Instance collection_guard `{CollectionMonad M} : MGuard M :=
+Global Instance set_guard `{MonadSet M} : MGuard M :=
   λ P dec A x, match dec with left H => x H | _ => ∅ end.
 
-Section collection_monad_base.
-  Context `{CollectionMonad M}.
+Section set_monad_base.
+  Context `{MonadSet M}.
   Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) :
     (x ∈ guard P; X) ↔ P ∧ x ∈ X.
   Proof.
-    unfold mguard, collection_guard; simpl; case_match;
+    unfold mguard, set_guard; simpl; case_match;
       rewrite ?elem_of_empty; naive_solver.
   Qed.
   Lemma elem_of_guard_2 `{Decision P} {A} (x : A) (X : M A) :
@@ -822,7 +822,7 @@ Section collection_monad_base.
   Lemma bind_empty {A B} (f : A → M B) X :
     X ≫= f ≡ ∅ ↔ X ≡ ∅ ∨ ∀ x, x ∈ X → f x ≡ ∅.
   Proof. set_solver. Qed.
-End collection_monad_base.
+End set_monad_base.
 
 
 (** * Quantifiers *)
@@ -830,7 +830,7 @@ Definition set_Forall `{ElemOf A C} (P : A → Prop) (X : C) := ∀ x, x ∈ X 
 Definition set_Exists `{ElemOf A C} (P : A → Prop) (X : C) := ∃ x, x ∈ X ∧ P x.
 
 Section quantifiers.
-  Context `{SimpleCollection A C} (P : A → Prop).
+  Context `{SemiSet A C} (P : A → Prop).
   Implicit Types X Y : C.
 
   Lemma set_Forall_empty : set_Forall P (∅ : C).
@@ -859,7 +859,7 @@ Section quantifiers.
 End quantifiers.
 
 Section more_quantifiers.
-  Context `{SimpleCollection A C}.
+  Context `{SemiSet A C}.
   Implicit Types X : C.
 
   Lemma set_Forall_impl (P Q : A → Prop) X :
@@ -933,25 +933,25 @@ Section fresh.
   Qed.
 End fresh.
 
-(** * Properties of implementations of collections that form a monad *)
-Section collection_monad.
-  Context `{CollectionMonad M}.
+(** * Properties of implementations of sets that form a monad *)
+Section set_monad.
+  Context `{MonadSet M}.
 
-  Global Instance collection_fmap_mono {A B} :
+  Global Instance set_fmap_mono {A B} :
     Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap M _ A B).
   Proof. intros f g ? X Y ?; set_solver by eauto. Qed.
-  Global Instance collection_bind_mono {A B} :
+  Global Instance set_bind_mono {A B} :
     Proper (pointwise_relation _ (⊆) ==> (⊆) ==> (⊆)) (@mbind M _ A B).
   Proof. unfold respectful, pointwise_relation; intros f g Hfg X Y ?. set_solver. Qed.
-  Global Instance collection_join_mono {A} :
+  Global Instance set_join_mono {A} :
     Proper ((⊆) ==> (⊆)) (@mjoin M _ A).
   Proof. intros X Y ?; set_solver. Qed.
 
-  Lemma collection_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x.
+  Lemma set_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x.
   Proof. set_solver. Qed.
-  Lemma collection_guard_True {A} `{Decision P} (X : M A) : P → (guard P; X) ≡ X.
+  Lemma set_guard_True {A} `{Decision P} (X : M A) : P → (guard P; X) ≡ X.
   Proof. set_solver. Qed.
-  Lemma collection_fmap_compose {A B C} (f : A → B) (g : B → C) (X : M A) :
+  Lemma set_fmap_compose {A B C} (f : A → B) (g : B → C) (X : M A) :
     g ∘ f <$> X ≡ g <$> (f <$> X).
   Proof. set_solver. Qed.
   Lemma elem_of_fmap_1 {A B} (f : A → B) (X : M A) (y : B) :
@@ -971,7 +971,7 @@ Section collection_monad.
     - revert l. induction k; set_solver by eauto.
     - induction 1; set_solver.
   Qed.
-  Lemma collection_mapM_length {A B} (f : A → M B) l k :
+  Lemma set_mapM_length {A B} (f : A → M B) l k :
     l ∈ mapM f k → length l = length k.
   Proof. revert l; induction k; set_solver by eauto. Qed.
   Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k :
@@ -987,13 +987,13 @@ Section collection_monad.
     rewrite elem_of_mapM. intros Hl1. revert l2.
     induction Hl1; inversion_clear 1; constructor; auto.
   Qed.
-End collection_monad.
+End set_monad.
 
-(** Finite collections *)
+(** Finite sets *)
 Definition set_finite `{ElemOf A B} (X : B) := ∃ l : list A, ∀ x, x ∈ X → x ∈ l.
 
 Section finite.
-  Context `{SimpleCollection A C}.
+  Context `{SemiSet A C}.
   Implicit Types X Y : C.
 
   Global Instance set_finite_subseteq :
@@ -1017,7 +1017,7 @@ Section finite.
 End finite.
 
 Section more_finite.
-  Context `{Collection A C}.
+  Context `{Set_ A C}.
   Implicit Types X Y : C.
 
   Lemma intersection_finite_l X Y : set_finite X → set_finite (X ∩ Y).
@@ -1037,42 +1037,42 @@ End more_finite.
 (** Sets of sequences of natural numbers *)
 (* The set [seq_seq start len] of natural numbers contains the sequence
 [start, start + 1, ..., start + (len-1)]. *)
-Fixpoint seq_set `{Singleton nat C, Union C, Empty C} (start len : nat) : C :=
+Fixpoint set_seq `{Singleton nat C, Union C, Empty C} (start len : nat) : C :=
   match len with
   | O => ∅
-  | S len' => {[ start ]} ∪ seq_set (S start) len'
+  | S len' => {[ start ]} ∪ set_seq (S start) len'
   end.
 
-Section seq_set.
-  Context `{SimpleCollection nat C}.
+Section set_seq.
+  Context `{SemiSet nat C}.
   Implicit Types start len x : nat.
 
-  Lemma elem_of_seq_set start len x :
-    x ∈ seq_set (C:=C) start len ↔ start ≤ x < start + len.
+  Lemma elem_of_set_seq start len x :
+    x ∈ set_seq (C:=C) start len ↔ start ≤ x < start + len.
   Proof.
     revert start. induction len as [|len IH]; intros start; simpl.
     - rewrite elem_of_empty. lia.
     - rewrite elem_of_union, elem_of_singleton, IH. lia.
   Qed.
 
-  Lemma seq_set_start_disjoint start len :
-    {[ start ]} ## seq_set (C:=C) (S start) len.
-  Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. lia. Qed.
+  Lemma set_seq_start_disjoint start len :
+    {[ start ]} ## set_seq (C:=C) (S start) len.
+  Proof. intros x. rewrite elem_of_singleton, elem_of_set_seq. lia. Qed.
 
-  Lemma seq_set_S_disjoint start len :
-    {[ start + len ]} ## seq_set (C:=C) start len.
-  Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. lia. Qed.
+  Lemma set_seq_S_disjoint start len :
+    {[ start + len ]} ## set_seq (C:=C) start len.
+  Proof. intros x. rewrite elem_of_singleton, elem_of_set_seq. lia. Qed.
 
-  Lemma seq_set_S_union start len :
-    seq_set start (S len) ≡@{C} {[ start + len ]} ∪ seq_set start len.
+  Lemma set_seq_S_union start len :
+    set_seq start (S len) ≡@{C} {[ start + len ]} ∪ set_seq start len.
   Proof.
-    intros x. rewrite elem_of_union, elem_of_singleton, !elem_of_seq_set. lia.
+    intros x. rewrite elem_of_union, elem_of_singleton, !elem_of_set_seq. lia.
   Qed.
 
-  Lemma seq_set_S_union_L `{!LeibnizEquiv C} start len :
-    seq_set start (S len) =@{C} {[ start + len ]} ∪ seq_set start len.
-  Proof. unfold_leibniz. apply seq_set_S_union. Qed.
-End seq_set.
+  Lemma set_seq_S_union_L `{!LeibnizEquiv C} start len :
+    set_seq start (S len) =@{C} {[ start + len ]} ∪ set_seq start len.
+  Proof. unfold_leibniz. apply set_seq_S_union. Qed.
+End set_seq.
 
 (** Mimimal elements *)
 Definition minimal `{ElemOf A C} (R : relation A) (x : A) (X : C) : Prop :=
@@ -1081,7 +1081,7 @@ Instance: Params (@minimal) 5 := {}.
 Typeclasses Opaque minimal.
 
 Section minimal.
-  Context `{SimpleCollection A C} {R : relation A}.
+  Context `{SemiSet A C} {R : relation A}.
   Implicit Types X Y : C.
 
   Global Instance minimal_proper x : Proper ((≡@{C}) ==> iff) (minimal R x).
diff --git a/theories/tactics.v b/theories/tactics.v
index 51df63830261e1ccf861feae62286ded1afcfbb5..2fbf9234508cf27dca8d3357dd9c635f012d45df 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -472,7 +472,7 @@ Ltac find_pat pat tac :=
 
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
 particular, on those generated by the tactic [unfold_elem_ofs] which is used
-to solve propositions on collections. The [naive_solver] tactic implements an
+to solve propositions on sets. The [naive_solver] tactic implements an
 ad-hoc and incomplete [firstorder]-like solver using Ltac's backtracking
 mechanism. The tactic suffers from the following limitations:
 - It might leave unresolved evars as Ltac provides no way to detect that.