diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 154a6bf58cc4313e6c1f2095619150716116dbc3..8d15141405245ee9c6501c9b2338aa4b3bf05b53 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -140,6 +140,104 @@ The following rules identify the class of timeless propositions:
 \end{mathparpagebreakable}
 
 
+\subsection{Dynamic Composeable Higher-Order Resources}
+\label{sec:composeable-resources}
+
+The base logic described in \Sref{sec:base-logic} works over an arbitrary camera $\monoid$ defining the structure of the resources.
+It turns out that we can generalize this further and permit picking cameras ``$\iFunc(\Prop)$'' that depend on the structure of propositions themselves.
+Of course, $\Prop$ is just the syntactic type of propositions; for this to make sense we have to look at the semantics.
+
+Furthermore, there is a composability problem with the given logic: if we have one proof performed with camera $\monoid_1$, and another proof carried out with a \emph{different} camera $\monoid_2$, then the two proofs are actually carried out in two \emph{entirely separate logics} and hence cannot be combined.
+
+Finally, in many cases just having a single ``instance'' of a camera available for reasoning is not enough.
+For example, when reasoning about a dynamically allocated data structure, every time a new instance of that data structure is created, we will want a fresh resource governing the state of this particular instance.
+While it would be possible to handle this problem whenever it comes up, it turns out to be useful to provide a general solution.
+
+The purpose of this section is to describe how we solve these issues.
+
+\paragraph{Picking the resources.}
+The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.
+To instantiate the logic with dynamic higher-order ghost state, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs^\op \times \OFEs \to \CMRAs)_{i \in \mathcal{I}}$.
+(This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.)
+
+From this, we construct the bifunctor defining the overall resources as follows:
+\begin{align*}
+  \GName \eqdef{}& \nat \\
+  \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \GName \fpfn \iFunc_i(\ofe^\op, \ofe)
+\end{align*}
+We will motivate both the use of a product and the finite partial function below.
+$\textdom{ResF}(\ofe^\op, \ofe)$ is a camera by lifting the individual cameras pointwise, and it has a unit (using the empty finite partial function).
+Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF}$.
+
+Now we can write down the recursive domain equation:
+\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
+Here, $\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor, which exists and is unique up to isomorphism by \thmref{thm:america_rutten}, so we obtain some object $\iPreProp$ such that:
+\begin{align*}
+  \Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
+  \iProp &\eqdef \UPred(\Res) \\
+	\wIso &: \iProp \nfn \iPreProp \\
+	\wIso^{-1} &: \iPreProp \nfn \iProp \\
+  \wIso(\wIso^{-1}(x)) &\eqdef x \\
+  \wIso^{-1}(\wIso(x)) &\eqdef x
+\end{align*}
+Now we can instantiate the base logic described in \Sref{sec:base-logic} with $\Res$ as the chosen camera:
+\[ \Sem{\Prop} \eqdef \UPred(\Res) \]
+We obtain that $\Sem{\Prop} = \iProp$.
+Effectively, we just defined a way to instantiate the base logic with $\Res$ as the camera of resources, while providing a way for $\Res$ to depend on $\iPreProp$, which is isomorphic to $\Sem\Prop$.
+
+We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical propositions $\Sem\Prop$ and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic.
+
+\paragraph{Proof composability.}
+To make our proofs composeable, we \emph{generalize} our proofs over the family of functors.
+This is possible because we made $\Res$ a \emph{product} of all the cameras picked by the user, and because we can actually work with that product ``pointwise''.
+So instead of picking a \emph{concrete} family, proofs will assume to be given an \emph{arbitrary} family of functors, plus a proof that this family \emph{contains the functors they need}.
+Composing two proofs is then merely a matter of conjoining the assumptions they make about the functors.
+Since the logic is entirely parametric in the choice of functors, there is no trouble reasoning without full knowledge of the family of functors.
+
+Only when the top-level proof is completed we will ``close'' the proof by picking a concrete family that contains exactly those functors the proof needs.
+
+\paragraph{Dynamic resources.}
+Finally, the use of finite partial functions lets us have as many instances of any camera as we could wish for:
+Because there can only ever be finitely many instances already allocated, it is always possible to create a fresh instance with any desired (valid) starting state.
+This is best demonstrated by giving some proof rules.
+
+So let us first define the notion of ghost ownership that we use in this logic.
+Assuming that the family of functors contains the functor $\Sigma_i$ at index $i$, and furthermore assuming that $\monoid_i = \Sigma_i(\iPreProp, \iPreProp)$, given some $\melt \in \monoid_i$ we define:
+\[ \ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\mapsingleton \gname \melt, \emptyset, \ldots)} \]
+This is ownership of the pair (element of the product over all the functors) that has the empty finite partial function in all components \emph{except for} the component corresponding to index $i$, where we own the element $\melt$ at index $\gname$ in the finite partial function.
+
+We can show the following properties for this form of ownership:
+\begin{mathparpagebreakable}
+  \inferH{res-alloc}{\text{$G$ infinite} \and \melt \in \mval_{M_i}}
+  {  \TRUE \proves \upd \Exists\gname\in G. \ownGhost\gname{\melt : M_i}
+  }
+  \and
+  \inferH{res-update}
+    {\melt \mupd_{M_i} B}
+    {\ownGhost\gname{\melt : M_i} \proves \upd \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}}
+
+  \inferH{res-empty}
+  {\text{$\munit$ is a unit of $M_i$}}
+  {\TRUE \proves \upd \ownGhost\gname\munit}
+
+  \axiomH{res-op}
+    {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \provesIff \ownGhost\gname{\melt\mtimes\meltB : M_i}}
+
+  \axiomH{res-valid}
+    {\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}
+
+  \inferH{res-timeless}
+    {\text{$\melt$ is a discrete OFE element}}
+    {\timeless{\ownGhost\gname{\melt : M_i}}}
+\end{mathparpagebreakable}
+
+Below, we will always work within (an instance of) the logic as described here.
+Whenever a camera is used in a proof, we implicitly assume it to be available in the global family of functors.
+We will typically leave the $M_i$ implicit when asserting ghost ownership, as the type of $\melt$ will be clear from the context.
+
+
+
+
 
 %%% Local Variables:
 %%% mode: latex
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index df72785caaed76f5f05af3443bdeb568e30aa31f..908b19d17a7eefe893464f976c6ac79a41a3af67 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -4,101 +4,7 @@
 
 This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the base logic.
 So in the following, we assume that some language $\Lang$ was fixed.
-
-\subsection{Dynamic Composeable Higher-Order Resources}
-\label{sec:composeable-resources}
-
-The base logic described in \Sref{sec:base-logic} works over an arbitrary camera $\monoid$ defining the structure of the resources.
-It turns out that we can generalize this further and permit picking cameras ``$\iFunc(\Prop)$'' that depend on the structure of propositions themselves.
-Of course, $\Prop$ is just the syntactic type of propositions; for this to make sense we have to look at the semantics.
-
-Furthermore, there is a composability problem with the given logic: if we have one proof performed with camera $\monoid_1$, and another proof carried out with a \emph{different} camera $\monoid_2$, then the two proofs are actually carried out in two \emph{entirely separate logics} and hence cannot be combined.
-
-Finally, in many cases just having a single ``instance'' of a camera available for reasoning is not enough.
-For example, when reasoning about a dynamically allocated data structure, every time a new instance of that data structure is created, we will want a fresh resource governing the state of this particular instance.
-While it would be possible to handle this problem whenever it comes up, it turns out to be useful to provide a general solution.
-
-The purpose of this section is to describe how we solve these issues.
-
-\paragraph{Picking the resources.}
-The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.
-To instantiate the program logic, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs \to \CMRAs)_{i \in \mathcal{I}}$.
-(This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.)
-
-From this, we construct the bifunctor defining the overall resources as follows:
-\begin{align*}
-  \GName \eqdef{}& \nat \\
-  \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \GName \fpfn \iFunc_i(\ofe^\op, \ofe)
-\end{align*}
-We will motivate both the use of a product and the finite partial function below.
-$\textdom{ResF}(\ofe^\op, \ofe)$ is a camera by lifting the individual cameras pointwise, and it has a unit (using the empty finite partial functions).
-Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF}$.
-
-Now we can write down the recursive domain equation:
-\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
-Here, $\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor, which exists and is unique up to isomorphism by \thmref{thm:america_rutten}.
-We do not need to consider how the object $\iPreProp$ is constructed, we only need the isomorphism, given by:
-\begin{align*}
-  \Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
-  \iProp &\eqdef \UPred(\Res) \\
-	\wIso &: \iProp \nfn \iPreProp \\
-	\wIso^{-1} &: \iPreProp \nfn \iProp
-\end{align*}
-
-Notice that $\iProp$ is the semantic model of propositions for the base logic described in \Sref{sec:base-logic} with $\Res$:
-\[ \Sem{\Prop} \eqdef \iProp = \UPred(\Res) \]
-Effectively, we just defined a way to instantiate the base logic with $\Res$ as the camera of resources, while providing a way for $\Res$ to depend on $\iPreProp$, which is isomorphic to $\Sem\Prop$.
-
-We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical propositions $\Sem\Prop$ and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic.
-
-\paragraph{Proof composability.}
-To make our proofs composeable, we \emph{generalize} our proofs over the family of functors.
-This is possible because we made $\Res$ a \emph{product} of all the cameras picked by the user, and because we can actually work with that product ``pointwise''.
-So instead of picking a \emph{concrete} family, proofs will assume to be given an \emph{arbitrary} family of functors, plus a proof that this family \emph{contains the functors they need}.
-Composing two proofs is then merely a matter of conjoining the assumptions they make about the functors.
-Since the logic is entirely parametric in the choice of functors, there is no trouble reasoning without full knowledge of the family of functors.
-
-Only when the top-level proof is completed we will ``close'' the proof by picking a concrete family that contains exactly those functors the proof needs.
-
-\paragraph{Dynamic resources.}
-Finally, the use of finite partial functions lets us have as many instances of any camera as we could wish for:
-Because there can only ever be finitely many instances already allocated, it is always possible to create a fresh instance with any desired (valid) starting state.
-This is best demonstrated by giving some proof rules.
-
-So let us first define the notion of ghost ownership that we use in this logic.
-Assuming that the family of functors contains the functor $\Sigma_i$ at index $i$, and furthermore assuming that $\monoid_i = \Sigma_i(\iPreProp, \iPreProp)$, given some $\melt \in \monoid_i$ we define:
-\[ \ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\mapsingleton \gname \melt, \emptyset, \ldots)} \]
-This is ownership of the pair (element of the product over all the functors) that has the empty finite partial function in all components \emph{except for} the component corresponding to index $i$, where we own the element $\melt$ at index $\gname$ in the finite partial function.
-
-We can show the following properties for this form of ownership:
-\begin{mathparpagebreakable}
-  \inferH{res-alloc}{\text{$G$ infinite} \and \melt \in \mval_{M_i}}
-  {  \TRUE \proves \upd \Exists\gname\in G. \ownGhost\gname{\melt : M_i}
-  }
-  \and
-  \inferH{res-update}
-    {\melt \mupd_{M_i} B}
-    {\ownGhost\gname{\melt : M_i} \proves \upd \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}}
-
-  \inferH{res-empty}
-  {\text{$\munit$ is a unit of $M_i$}}
-  {\TRUE \proves \upd \ownGhost\gname\munit}
-  
-  \axiomH{res-op}
-    {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \provesIff \ownGhost\gname{\melt\mtimes\meltB : M_i}}
-
-  \axiomH{res-valid}
-    {\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}
-
-  \inferH{res-timeless}
-    {\text{$\melt$ is a discrete OFE element}}
-    {\timeless{\ownGhost\gname{\melt : M_i}}}
-\end{mathparpagebreakable}
-
-Below, we will always work within (an instance of) the logic as described here.
-Whenever a camera is used in a proof, we implicitly assume it to be available in the global family of functors.
-We will typically leave the $M_i$ implicit when asserting ghost ownership, as the type of $\melt$ will be clear from the context.
-
+Furthermore, we work in the logic with higher-order ghost state as described in \Sref{sec:composeable-resources}.
 
 
 \subsection{World Satisfaction, Invariants, Fancy Updates}