diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 6c3c701900d8ee9d5d988249d4093c1cb4589c41..338acd4caec5a3e2edf9ef37ee577dca71930a1c 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -231,18 +231,18 @@ The purpose of the adequacy statement is to show that our notion of weakest prec
 The most general form of the adequacy statement is about proving properties of an arbitrary program execution.
 
 \begin{thm}[Adequacy]
-  Assume we are given some $\expr_0$, $\state_0$, $\vec\obs$, $\tpool_1$, $\state_1$ such that $([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1)$, and we are also given a \emph{meta-level} property $\metaprop$ that we want to show.
+  Assume we are given some $\expr_1$, $\state_1$, $\vec\obs$, $\tpool_2$, $\state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we are also given a \emph{meta-level} property $\metaprop$ that we want to show.
   To verify that $\metaprop$ holds, it is sufficient to show the following Iris entailment:
 \begin{align*}
- &\TRUE \proves \pvs[\top] \Exists \stuckness, \stateinterp, \pred, \pred_F. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\stuckness;\top]{x.\; \pred(x)} * \left(\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_1, \state_1) \vs[\top][\emptyset] \hat{\metaprop}\right)
+ &\TRUE \proves \pvs[\top] \Exists \stuckness, \stateinterp, \pred, \pred_F. \stateinterp(\state_1,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{x.\; \pred(x)} * \left(\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \hat{\metaprop}\right)
 \end{align*}
 where $\consstate$ describes states that are consistent with the state interpretation and postconditions:
 \begin{align*}
- \consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_1, \state_1) \eqdef{}&\Exists \expr_1, \tpool_1'. \tpool_1 = [\expr_1] \dplus \tpool_1' * {}\\
- &\quad (s = \NotStuck \Ra \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1) ) *{}\\
- &\quad \stateinterp(\state_1, (), |\tpool_1'|) *{}\\
- &\quad (\toval(\expr_1) \ne \bot \wand \pred(\toval(\expr_1))) *{}\\
- &\quad \left(\Sep[\expr \in \tpool_1'] \toval(\expr) \ne \bot \wand \pred_F(\toval(\expr))\right)
+ \consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \eqdef{}&\Exists \expr_2, \tpool_2'. \tpool_2 = [\expr_2] \dplus \tpool_2' * {}\\
+ &\quad (s = \NotStuck \Ra \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2) ) *{}\\
+ &\quad \stateinterp(\state_2, (), |\tpool_2'|) *{}\\
+ &\quad (\toval(\expr_2) \ne \bot \wand \pred(\toval(\expr_2))) *{}\\
+ &\quad \left(\Sep[\expr \in \tpool_2'] \toval(\expr) \ne \bot \wand \pred_F(\toval(\expr))\right)
 \end{align*}
 The $\hat\metaprop$ here arises because we need a way to talk about $\metaprop$ inside Iris.
 To this end, we assume that the signature $\Sig$ contains some assertion $\hat{\metaprop}$:
@@ -259,15 +259,15 @@ In other words, to show that $\metaprop$ holds, we have to prove an entailment i
 \begin{itemize}
   \item the initial state interpretation,
   \item a weakest-precondition,
-  \item and a view shift showing the desired $\hat\metaprop$ under the extra assumption $\consstate(\tpool_1, \state_1)$.
+  \item and a view shift showing the desired $\hat\metaprop$ under the extra assumption $\consstate(\tpool_2, \state_2)$.
 \end{itemize}
 Notice that the state interpretation and the postconditions are chosen \emph{after} doing a fancy update, which allows them to depend on the names of ghost variables that are picked in that initial fancy update.
 This gives us a chance to allocate some ``global'' ghost state that state interpretation and postcondition can refer to.
 
-$\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_1, \state_1)$ says that:
+$\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2)$ says that:
 \begin{itemize}
-\item The final thread-pool $\tpool_1$ contains the final state of the main thread $\expr_1$, and any number of additional forked threads in $\tpool_1'$.
-\item If this is a stuck-free weakest precondition, then all threads in the final thread-pool are either values or are reducible in the final state $\state_1$.
+\item The final thread-pool $\tpool_2$ contains the final state of the main thread $\expr_2$, and any number of additional forked threads in $\tpool_2'$.
+\item If this is a stuck-free weakest precondition, then all threads in the final thread-pool are either values or are reducible in the final state $\state_2$.
 \item The state interpretation $\stateinterp$ holds for the final state.
 \item If the main thread reduced to a value, the post-condition $\pred$ of the weakest precondition holds for that value.
 \item If any other thread reduced to a value, the forked-thread post-condition $\pred_F$ holds for that value.
@@ -275,56 +275,56 @@ $\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_1, \state_1)$ says
 
 ~\par
 
-As an example for how to use this adequacy theorem, let us say we wanted to prove that a program $\expr_0$ for which we derived a $\NotStuck$ weakest-precondition cannot get stuck:
+As an example for how to use this adequacy theorem, let us say we wanted to prove that a program $\expr_1$ for which we derived a $\NotStuck$ weakest-precondition cannot get stuck:
 \begin{cor}[Stuck-freedom]
-  Assume we are given some $\expr_0$ such that the following holds:
+  Assume we are given some $\expr_1$ such that the following holds:
 \[
-\TRUE \proves \All\state_0, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred, \pred_F. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\NotStuck;\top]{x.\; \pred(x)}
+\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred, \pred_F. \stateinterp(\state_1,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\NotStuck;\top]{x.\; \pred(x)}
 \]
   Then it is the case that:
 \[
-\All \state_0, \vec\obs, \tpool_1, \state_1. ([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1) \Ra \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1)
+\All \state_1, \vec\obs, \tpool_2, \state_2. ([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2) \Ra \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2)
 \]
 \end{cor}
-To prove the conclusion of this corollary, we assume some $\state_0, \vec\obs, \tpool_1, \state_1$ and $([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1)$, and we instantiate the main theorem with this execution and $\metaprop \eqdef \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1)$.
+To prove the conclusion of this corollary, we assume some $\state_1, \vec\obs, \tpool_2, \state_2$ and $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we instantiate the main theorem with this execution and $\metaprop \eqdef \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2)$.
 We can then show the premise of adequacy using the Iris entailment that we assumed in the corollary and:
-\[ \TRUE \proves \consstate^{\stateinterp;\pred;\pred_F}_{\NotStuck}(\tpool_1, \state_1) \vs[\top][\emptyset] \metaprop \]
+\[ \TRUE \proves \consstate^{\stateinterp;\pred;\pred_F}_{\NotStuck}(\tpool_2, \state_2) \vs[\top][\emptyset] \metaprop \]
 This proof, just like the following, also exploits that we can freely swap between meta-level universal quantification ($\All x. \TRUE \proves \prop$) and quantification in Iris ($\TRUE \proves \All x. \prop$).
 
 ~\par
 
 Similarly we could show that the postcondition makes adequate statements about the possible final value of the main thread:
 \begin{cor}[Adequate postcondition]
-  Assume we are given some $\expr_0$ and a set $V \subseteq \Val$ such that the following holds (assuming we can talk about sets like $V$ inside the logic):
+  Assume we are given some $\expr_1$ and a set $V \subseteq \Val$ such that the following holds (assuming we can talk about sets like $V$ inside the logic):
 \[
-\TRUE \proves \All\state_0, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred_F. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\stuckness;\top]{x.\; x \in V}
+\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred_F. \stateinterp(\state_1,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{x.\; x \in V}
 \]
   Then it is the case that:
 \[
-\All \state_0, \vec\obs, \val_1, \tpool_1, \state_1. ([\expr_0], \state_0) \tpsteps[\vec\obs] ([\ofval(\val_1)] \dplus \tpool_1, \state_1) \Ra \val_1 \in V
+\All \state_1, \vec\obs, \val_2, \tpool_2, \state_2. ([\expr_1], \state_1) \tpsteps[\vec\obs] ([\ofval(\val_2)] \dplus \tpool_2, \state_2) \Ra \val_2 \in V
 \]
 \end{cor}
-To show this, we assume some $\state_0, \vec\obs, \val_1, \tpool_1, \state_1$ such that $([\expr_0], \state_0) \tpsteps[\vec\obs] ([\ofval(\val_1)] \dplus \tpool_1, \state_1)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \val_1 \in \Val$.
+To show this, we assume some $\state_1, \vec\obs, \val_2, \tpool_2, \state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] ([\ofval(\val_2)] \dplus \tpool_2, \state_2)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \val_2 \in \Val$.
 Then we only have to show:
-$$\TRUE \proves \consstate^{\stateinterp;(\Lam \val. \val \in \Val);\pred_F}_{\stuckness}([\ofval(\val_1)] \dplus \tpool_1, \state_1) \vs[\top][\emptyset] \val_1 \in \Val $$
+$$\TRUE \proves \consstate^{\stateinterp;(\Lam \val. \val \in \Val);\pred_F}_{\stuckness}([\ofval(\val_2)] \dplus \tpool_2, \state_2) \vs[\top][\emptyset] \val_2 \in \Val $$
 
 ~\par
 
 As a final example, we could use adequacy to show that the state $\state$ of the program is always in some set $\Sigma \subseteq \State$:
 \begin{cor}[Adequate state interpretation]
-  Assume we are given some $\expr_0$ and a set $\Sigma \subseteq \State$ such that the following holds (assuming we can talk about sets like $\Sigma$ inside the logic):
+  Assume we are given some $\expr_1$ and a set $\Sigma \subseteq \State$ such that the following holds (assuming we can talk about sets like $\Sigma$ inside the logic):
 \[
-\TRUE \proves \All\state_0, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred, \pred_F. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\stuckness;\top]{\pred} * (\All \state_1, m. \stateinterp(\state_1,(),m) \!\vs[\top][\emptyset] \state_1 \in \Sigma)
+\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred, \pred_F. \stateinterp(\state_1,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{\pred} * (\All \state_2, m. \stateinterp(\state_2,(),m) \!\vs[\top][\emptyset] \state_2 \in \Sigma)
 \]
   Then it is the case that:
 \[
-\All \state_0, \vec\obs, \tpool_1, \state_1. ([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1) \Ra \state_1 \in \Sigma
+\All \state_1, \vec\obs, \tpool_2, \state_2. ([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2) \Ra \state_2 \in \Sigma
 \]
 \end{cor}
-To show this, we assume some $\state_0, \vec\obs, \tpool_1, \state_1$ such that $([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \state_1 \in \Sigma$.
+To show this, we assume some $\state_1, \vec\obs, \tpool_2, \state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \state_2 \in \Sigma$.
 Then we have to show:
 \[
-(\All \state_1, m. \stateinterp(\state_1,(),m) \!\vs[\top][\emptyset] \state_1 \in \Sigma) \proves \consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_1, \state_1) \vs[\top][\emptyset] \state_1 \in \Sigma
+(\All \state_2, m. \stateinterp(\state_2,(),m) \!\vs[\top][\emptyset] \state_2 \in \Sigma) \proves \consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \state_2 \in \Sigma
 \]
 
 \paragraph{Hoare triples.}
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index ad5c8b907af86268c8fe8e9af0dafe3dfe5b004f..c6725a34764b0ef99dce3bd46762780735699fa0 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -114,7 +114,7 @@ Qed.
 End adequacy.
 
 (** Iris's generic adequacy result *)
-Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e σ1 n κs t2 σ2 φ :
+Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e1 σ1 n κs t2 σ2 φ :
   (∀ `{Hinv : !invG Σ},
      (|={⊤}=> ∃
          (s: stuckness)
@@ -122,7 +122,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e σ1 n κs t2 σ2 φ :
          (Φ fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        stateI σ1 κs 0 ∗
-       WP e @ s; ⊤ {{ Φ }} ∗
+       WP e1 @ s; ⊤ {{ Φ }} ∗
        (∀ e2 t2',
          (* e2 is the final state of the main thread, t2' the rest *)
          ⌜ t2 = e2 :: t2' ⌝ -∗
@@ -140,7 +140,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e σ1 n κs t2 σ2 φ :
          one can use [fupd_intro_mask'] or [fupd_mask_weaken] to introduce the
          fancy update. *)
          |={⊤,∅}=> ⌜ φ ⌝))%I) →
-  nsteps n ([e], σ1) κs (t2, σ2) →
+  nsteps n ([e1], σ1) κs (t2, σ2) →
   (* Then we can conclude [φ] at the meta-level. *)
   φ.
 Proof.