diff --git a/docs/constructions.tex b/docs/constructions.tex
index 939281c8bb65b9b0d30f78d96e18ac554bfd7fd2..0afec08f23bf5c15dd0e03a70f1cfb10c8cfc8ac 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -6,7 +6,7 @@
 
 Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
 \begin{align*}
-  \monoid \eqdef{}& \setComp{(c, V) \subseteq (\mathbb{N} \to T) \times \mathbb{N}}{ \All n, m. n \geq m \Ra n \in V \Ra m \in V  } \\
+  \monoid \eqdef{}& \setComp{(c, V) \in (\mathbb{N} \to T) \times \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in V \Ra m \in V  } \\
   & \text{quotiented by} \\
   (c_1, V_1) \equiv (c_1, V_2) \eqdef{}& V_1 = V_2 \land \All n. n \in V_1 \Ra c_1(n) \nequiv{n} c_2(n) \\
   (c_1, V_1) \nequiv{n} (c_1, V_2) \eqdef{}& (\All m \leq n. m \in V_1 \Lra m \in V_2) \land (\All m \leq n. m \in V_1 \Ra c_1(m) \nequiv{m} c_2(m)) \\
diff --git a/docs/iris.sty b/docs/iris.sty
index b5e3df222d1a31f4870145f5559da7b06a235149..5b3721f46ab9d31802c7a14320123dc47074767b 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -106,10 +106,12 @@
 
 
 %% Some commonly used identifiers
+\newcommand{\SProp}{\textdom{SProp}}
 \newcommand{\UPred}{\textdom{UPred}}
 \newcommand{\mProp}{\textdom{Prop}} % meta-level prop
 \newcommand{\iProp}{\textdom{iProp}}
 \newcommand{\Wld}{\textdom{Wld}}
+\newcommand{\Res}{\textdom{Res}}
 
 \newcommand{\cofe}{T}
 \newcommand{\cofeB}{U}