diff --git a/docs/constructions.tex b/docs/constructions.tex
index 9405ecd735dfdea31f4dc10ae610c566aa295f6d..7a08fa78cc0dfe9b33b1cd51b6efa8360037f6c1 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -5,24 +5,31 @@
 \subsection{Agreement}
 
 Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
+\newcommand{\agc}{\mathrm{c}} % the "c" field of an agreement element
+\newcommand{\agV}{\mathrm{V}} % the "V" field of an agreement element
 \begin{align*}
-  \monoid \eqdef{}& \recordComp{c : \mathbb{N} \to T , V : \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in V \Ra m \in V  } \\
+  \monoid \eqdef{}& \recordComp{\agc : \mathbb{N} \to T , \agV : \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in \agV \Ra m \in \agV  } \\
   & \text{quotiented by} \\
-  \melt \equiv \meltB \eqdef{}& \melt.V = \meltB.V \land \All n. n \in \melt.V \Ra \melt.c(n) \nequiv{n} \meltB.c(n) \\
-  \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.V \Lra m \in \meltB.V) \land (\All m \leq n. m \in \melt.V \Ra \melt.c(m) \nequiv{m} \meltB.c(m)) \\
-  \mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.V \land \All m \leq n. \melt.c(n) \nequiv{m} \melt.c(m) } \\
+  \melt \equiv \meltB \eqdef{}& \melt.\agV = \meltB.\agV \land \All n. n \in \melt.\agV \Ra \melt.\agc(n) \nequiv{n} \meltB.\agc(n) \\
+  \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.\agV \Lra m \in \meltB.\agV) \land (\All m \leq n. m \in \melt.\agV \Ra \melt.\agc(m) \nequiv{m} \meltB.\agc(m)) \\
+  \mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.\agV \land \All m \leq n. \melt.\agc(n) \nequiv{m} \melt.\agc(m) } \\
   \mcore\melt \eqdef{}& \melt \\
-  \melt \mtimes \meltB \eqdef{}& (\melt.c, \setComp{n}{n \in \melt.V \land n \in \meltB.V_2 \land \melt \nequiv{n} \meltB })
+  \melt \mtimes \meltB \eqdef{}& (\melt.\agc, \setComp{n}{n \in \melt.\agV \land n \in \meltB.\agV \land \melt \nequiv{n} \meltB })
 \end{align*}
 $\agm(-)$ is a locally non-expansive bifunctor from $\COFEs$ to $\CMRAs$.
 
 The reason we store a \emph{chain} $c$ of elements of $T$, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain.
 \ralf{Figure out why exactly this is not possible without adding an explicit chain here.}
 
+We define an injection $\ag$ into $\agm(\cofe)$ as follows:
+\[ \ag(x) \eqdef \record{\mathrm c \eqdef \Lam \any. x, \mathrm V \eqdef \mathbb{N}} \]
 There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following:
 \begin{mathpar}
-  \axiomH{ag-dup}{\melt = \melt \mtimes \melt}
-  \and\axiomH{ag-agree}{\melt \mtimes \meltB \in \mval_n \Ra \melt \nequiv{n} \meltB}
+  \axiomH{ag-val}{\ag(x) \in \mval_n}
+
+  \axiomH{ag-dup}{\ag(x) = \ag(x)\mtimes\ag(x)}
+  
+  \axiomH{ag-agree}{\ag(x) \mtimes \ag(y) \in \mval_n \Ra x \nequiv{n} y}
 \end{mathpar}
 
 
diff --git a/docs/iris.sty b/docs/iris.sty
index b9953fbacfa9ecc33c2ef10f038019370afcc546..0c73ddd2701dde561b4ef626deb4e9ab947e9921 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -313,6 +313,42 @@
 
 \newcommand{\cfg}[2]{{#1};{#2}}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% STANDARD DERIVED CONSTRUCTIONS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Agreement
+\newcommand{\agm}{\ensuremath{\textmon{Ag}}}
+\newcommand{\ag}{\textlog{ag}}
+
+% Fraction
+\newcommand{\fracm}{\ensuremath{\textmon{Frac}}}
+
+% Exclusive
+\newcommand{\exm}{\ensuremath{\textmon{Ex}}}
+
+% Auth
+\newcommand{\authm}{\textmon{Auth}}
+\newcommand{\authfull}{\mathord{\bullet}\,}
+\newcommand{\authfrag}{\mathord{\circ}\,}
+
+\newcommand{\AuthInv}{\textsf{AuthInv}}
+\newcommand{\Auth}{\textsf{Auth}}
+
+%% STSs
+\newcommand{\STSCtx}{\textlog{StsCtx}}
+\newcommand{\STSSt}{\textlog{StsSt}}
+\newcommand{\STSS}{\mathcal{S}} % states
+\newcommand{\STST}{\mathcal{T}} % tokens
+\newcommand{\STSL}{\mathcal{L}} % labels
+\newcommand{\ststrans}{\ra^{*}}%	the relation relevant to the STS rules
+
+
+\tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}]
+\tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}]
+
+%% Stored Propositions
+\newcommand{\mapstoprop}{\mathrel{\mapstochar\Ra}}
 
 
 \endinput
diff --git a/docs/setup.tex b/docs/setup.tex
index 849e836263be6927b42e776c0f224475dfc97ab9..8c5b92196c1351dd6338fe89b83b3394d4d77514 100644
--- a/docs/setup.tex
+++ b/docs/setup.tex
@@ -110,31 +110,3 @@
 	\let\ralf\hush%
 	\let\dave\hush%
 }
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% DERIVED CONSTRUCTIONS
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%% Commonly used identifiers
-\newcommand{\FHeap}{\textmon{FHeap}}
-\newcommand{\AFHeap}{\textmon{AFHeap}}
-
-\newcommand{\auth}[1]{\textmon{Auth}}
-\newcommand{\authfull}{\mathord{\bullet}\,}
-\newcommand{\authfrag}{\mathord{\circ}\,}
-
-\newcommand{\fracm}{\ensuremath{\textmon{Frac}}}
-\newcommand{\exm}{\ensuremath{\textmon{Ex}}}
-\newcommand{\agm}{\ensuremath{\textmon{Ag}}}
-
-\newcommand{\STSMon}[1]{\textmon{Sts}_{#1}}
-\newcommand{\STSInv}{\textsf{STSInv}}
-\newcommand{\STS}{\textsf{STS}}
-\newcommand{\STSS}{\mathcal{S}} % states
-\newcommand{\STST}{\mathcal{T}} % tokens
-\newcommand{\STSL}{\mathcal{L}} % labels
-\newcommand{\ststrans}{\ra^{*}}%	the relation relevant to the STS rules
-
-\newcommand{\AuthInv}{\textsf{AuthInv}}
-\newcommand{\Auth}{\textsf{Auth}}