diff --git a/docs/logic.tex b/docs/logic.tex
index 88ec1bbbfa53a03d8f4f8e387ef3820fc399459c..5f358f8d73a324362b3a44e2f65dc4c9c03faae9 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -604,7 +604,7 @@ Here we define $\wpre{\expr'}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr' =
 
 \subsection{Adequacy}
 
-The adequacy statement reads as follows:
+The adequacy statement concerning functional correctness reads as follows:
 \begin{align*}
  &\All \mask, \expr, \val, \pred, \state, \melt, \state', \tpool'.
  \\&(\All n. \melt \in \mval_n) \Ra
@@ -615,6 +615,17 @@ The adequacy statement reads as follows:
 \end{align*}
 where $\pred$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants.
 
+Furthermore, the following adequacy statement shows that our weakest preconditions imply that the execution never gets \emph{stuck}: Every expression in the thread pool either is a value, or can reduce further.
+\begin{align*}
+ &\All \mask, \expr, \state, \melt, \state', \tpool'.
+ \\&(\All n. \melt \in \mval_n) \Ra
+ \\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
+ \\&\cfg{\state}{[\expr]} \step^\ast
+     \cfg{\state'}{\tpool'} \Ra
+     \\&\All\expr'\in\tpool'. \toval(\expr) \neq \bot \lor \red(\expr, \state')
+\end{align*}
+Notice that this is stronger than saying that the thread pool can reduce; we actually assert that \emph{every} non-finished thread can take a step.
+
 
 % RJ: If we want this section back, we should port it to primitive view shifts and prove it in Coq.
 % \subsection{Unsound rules}
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 94e2d5e8d0cf087ed906f51928def1bd5bf41a5b..55090ec664ac1e21f1dc0ff3ce0e2f3afb9b11b1 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -112,18 +112,20 @@ Lemma wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
   ✓ m →
   (ownP σ1 ★ ownG m) ⊑ #> e1 @ E {{ Φ }} →
   rtc step ([e1], σ1) (t2, σ2) →
-  e2 ∈ t2 → to_val e2 = None → reducible e2 σ2.
+  e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2).
 Proof.
-  intros Hv ? Hs [i ?]%elem_of_list_lookup He.
+  intros Hv ? Hs [i ?]%elem_of_list_lookup.
   destruct (wp_adequacy_own Φ e1 t2 σ1 m σ2) as (rs2&Φs&?&?); auto.
   { by rewrite -(wp_mask_weaken E ⊤). }
   destruct (Forall3_lookup_l (λ e Φ r, wp ⊤ e Φ 2 r) t2
     (Φ :: Φs) rs2 i e2) as (Φ'&r2&?&?&Hwp); auto.
+  case He:(to_val e2)=>[v2|]; first by eauto. right.
   destruct (wp_step_inv ⊤ ∅ Φ' e2 1 2 σ2 r2 (big_op (delete i rs2)));
     rewrite ?right_id_L ?big_op_delete; auto.
   by rewrite -wp_eq.
 Qed.
 
+(* Connect this up to the threadpool-semantics. *)
 Theorem wp_adequacy_safe E Φ e1 t2 σ1 m σ2 :
   ✓ m →
   (ownP σ1 ★ ownG m) ⊑ #> e1 @ E {{ Φ }} →
@@ -133,8 +135,9 @@ Proof.
   intros.
   destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
   apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
-  destruct (wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?);
+  destruct (wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as [?|(e3&σ3&ef&?)];
     rewrite ?eq_None_not_Some; auto.
+  { exfalso. eauto. }
   destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
   right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
 Qed.