diff --git a/CHANGELOG.md b/CHANGELOG.md
index cd50794e2e4cd92684fe8d6267fa37d9cdb43a54..571ee447f1b490af02778bb405db7f8640083284 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,8 @@ API-breaking change is listed.
   example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as a
   prefix, as done in VST. A sed script to perform the renaming can be found at:
   https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/93
+- Add type class `TopSet` for sets with a `⊤` element. Provide instances for
+  `boolset`, `propset`, and `coPset`.
 
 ## std++ 1.2.1 (released 2019-08-29)
 
diff --git a/theories/base.v b/theories/base.v
index 30feccb2b6759ea57976109a1017f33b460b4069..0d143c06817b7e14b5517179a1905dcda9e252de 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1158,17 +1158,62 @@ Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
 Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 
 
+(** * Notations for lattices. *)
+(** SqSubsetEq registers the "canonical" partial order for a type, and is used
+for the \sqsubseteq symbol. *)
+Class SqSubsetEq A := sqsubseteq: relation A.
+Hint Mode SqSubsetEq ! : typeclass_instances.
+Instance: Params (@sqsubseteq) 2 := {}.
+Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
+Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
+Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
+Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
+
+Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
+Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
+
+Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
+
+Hint Extern 0 (_ ⊑ _) => reflexivity : core.
+
+Class Meet A := meet: A → A → A.
+Hint Mode Meet ! : typeclass_instances.
+Instance: Params (@meet) 2 := {}.
+Infix "⊓" := meet (at level 40) : stdpp_scope.
+Notation "(⊓)" := meet (only parsing) : stdpp_scope.
+Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
+Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
+
+Class Join A := join: A → A → A.
+Hint Mode Join ! : typeclass_instances.
+Instance: Params (@join) 2 := {}.
+Infix "⊔" := join (at level 50) : stdpp_scope.
+Notation "(⊔)" := join (only parsing) : stdpp_scope.
+Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
+Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
+
+Class Top A := top : A.
+Hint Mode Top ! : typeclass_instances.
+Notation "⊤" := top (format "⊤") : stdpp_scope.
+
+Class Bottom A := bottom : A.
+Hint Mode Bottom ! : typeclass_instances.
+Notation "⊥" := bottom (format "⊥") : stdpp_scope.
+
+
 (** * 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.
+(** The classes [SemiSet A C], [Set_ A C], and [TopSet A C] axiomatize sets 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 ∉@{C} ∅;
+  not_elem_of_empty (x : A) : x ∉@{C} ∅; (* We prove
+  [elem_of_empty : x ∈@{C} ∅ ↔ False] in [sets.v], which is more convenient for
+  rewriting. *)
   elem_of_singleton (x y : A) : x ∈@{C} {[ y ]} ↔ x = y;
   elem_of_union (X Y : C) (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
 }.
@@ -1178,6 +1223,12 @@ Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
   elem_of_intersection (X Y : C) (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
   elem_of_difference (X Y : C) (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
+Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
+    Union C, Intersection C, Difference C} : Prop := {
+  top_set_set :> Set_ A C;
+  elem_of_top' (x : A) : x ∈@{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
+  in [sets.v], which is more convenient for rewriting. *)
+}.
 
 (** 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
@@ -1276,45 +1327,3 @@ Class Half A := half: A → A.
 Hint Mode Half ! : typeclass_instances.
 Notation "½" := half (format "½") : stdpp_scope.
 Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
-
-(** * Notations for lattices. *)
-(** SqSubsetEq registers the "canonical" partial order for a type, and is used
-for the \sqsubseteq symbol. *)
-Class SqSubsetEq A := sqsubseteq: relation A.
-Hint Mode SqSubsetEq ! : typeclass_instances.
-Instance: Params (@sqsubseteq) 2 := {}.
-Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
-Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
-Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
-Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
-
-Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
-Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
-
-Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
-
-Hint Extern 0 (_ ⊑ _) => reflexivity : core.
-
-Class Meet A := meet: A → A → A.
-Hint Mode Meet ! : typeclass_instances.
-Instance: Params (@meet) 2 := {}.
-Infix "⊓" := meet (at level 40) : stdpp_scope.
-Notation "(⊓)" := meet (only parsing) : stdpp_scope.
-Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
-Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
-
-Class Join A := join: A → A → A.
-Hint Mode Join ! : typeclass_instances.
-Instance: Params (@join) 2 := {}.
-Infix "⊔" := join (at level 50) : stdpp_scope.
-Notation "(⊔)" := join (only parsing) : stdpp_scope.
-Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
-Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
-
-Class Top A := top : A.
-Hint Mode Top ! : typeclass_instances.
-Notation "⊤" := top (format "⊤") : stdpp_scope.
-
-Class Bottom A := bottom : A.
-Hint Mode Bottom ! : typeclass_instances.
-Notation "⊥" := bottom (format "⊥") : stdpp_scope.
diff --git a/theories/boolset.v b/theories/boolset.v
index cd4efe1a56d0e4a7b46144c11158605c3992a9a1..3bfa3b3d394180c7d9d4ddba5db98f1a87468949 100644
--- a/theories/boolset.v
+++ b/theories/boolset.v
@@ -19,15 +19,16 @@ 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).
+Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
 Proof.
-  split; [split| |].
+  split; [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.
+  - done.
 Qed.
 Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
 Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
diff --git a/theories/coPset.v b/theories/coPset.v
index ada2caeb738de0b0a004740ad4f9d6a7c04ff20e..1b21418116ebaaa36ad6e72a90641ff303ecb724 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -169,9 +169,9 @@ 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_set : Set_ positive coPset.
+Instance coPset_top_set : TopSet positive coPset.
 Proof.
-  split; [split| |].
+  split; [split; [split| |]|].
   - by intros ??.
   - intros p q. apply coPset_elem_of_singleton.
   - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
@@ -181,6 +181,7 @@ Proof.
   - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
     by rewrite coPset_elem_of_intersection,
       coPset_elem_of_opp, andb_True, negb_True.
+  - done.
 Qed.
 
 Instance coPset_leibniz : LeibnizEquiv coPset.
@@ -204,11 +205,6 @@ Proof.
  refine (λ X Y, cast_if (decide (X ∪ Y = Y))); abstract (by rewrite subseteq_union_L).
 Defined.
 
-(** * Top *)
-Lemma coPset_top_subseteq (X : coPset) : X ⊆ ⊤.
-Proof. done. Qed.
-Hint Resolve coPset_top_subseteq : core.
-
 (** * Finite sets *)
 Fixpoint coPset_finite (t : coPset_raw) : bool :=
   match t with
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 04f9e931143bac93cd0465fcf847f923f23aedde..67f7447a0994dbc5022486d8a5a633a5aea5fa95 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -80,6 +80,7 @@ Create HintDb ndisj.
 considering they are. *)
 Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj.
 Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
+Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : ndisj.
 Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress. *)
 Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
diff --git a/theories/propset.v b/theories/propset.v
index 529dd471075eb1b5f217c1ebbcaa7c39ad729aca..70e649d9412a502642223b812203a319e3f0a53e 100644
--- a/theories/propset.v
+++ b/theories/propset.v
@@ -21,18 +21,13 @@ 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.
+Instance propset_top_set {A} : TopSet A (propset A).
+Proof. split; [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.
 
 Definition set_to_propset `{ElemOf A C} (X : C) : propset A :=
   {[ x | x ∈ X ]}.
@@ -50,8 +45,6 @@ Instance propset_join : MJoin propset := λ A (XX : propset (propset A)),
 Instance propset_monad_set : MonadSet propset.
 Proof. by split; try apply _. Qed.
 
-Instance set_unfold_propset_top {A} (x : A) : SetUnfoldElemOf x (⊤ : propset A) True.
-Proof. by constructor. Qed.
 Instance set_unfold_PropSet {A} (P : A → Prop) x Q :
   SetUnfoldSimpl (P x) Q → SetUnfoldElemOf x (PropSet P) Q.
 Proof. intros HPQ. constructor. apply HPQ. Qed.
diff --git a/theories/sets.v b/theories/sets.v
index aaaa9ce9d55e88e41a11fd778ac8353bc57e0a07..9ccac38bd6e4994649156ba5b09f8ddc5c871615 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -242,6 +242,10 @@ Section set_unfold.
   Qed.
 End set_unfold.
 
+Instance set_unfold_top `{TopSet A C} (x : A) :
+  SetUnfoldElemOf x (⊤ : C) True.
+Proof. constructor. split; [done|intros; apply elem_of_top']. Qed.
+
 Section set_unfold_monad.
   Context `{MonadSet M}.
 
@@ -793,6 +797,19 @@ Section set.
 End set.
 
 
+(** * Sets with [∪], [∩], [∖], [∅], [{[_]}], and [⊤] *)
+Section top_set.
+  Context `{TopSet A C}.
+  Implicit Types x y : A.
+  Implicit Types X Y : C.
+
+  Lemma elem_of_top x : x ∈@{C} ⊤ ↔ True.
+  Proof. split; [done|intros; apply elem_of_top']. Qed.
+  Lemma top_subseteq X : X ⊆ ⊤.
+  Proof. intros x. by rewrite elem_of_top. Qed.
+End top_set.
+
+
 (** * Conversion of option and list *)
 Section option_and_list_to_set.
   Context `{SemiSet A C}.