diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 72d5e833b88bf20acbbfd58f1eef6a2defa9c8c0..d712d79fd58e028a585de30a5d48338604ee6ada 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -14,9 +14,9 @@ Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. solve_inG. Qed.
 
-Definition heap_adequacy Σ `{heapPreG Σ} p e σ φ :
-  (∀ `{heapG Σ}, WP e @ p; ⊤ {{ v, ⌜φ v⌝ }}%I) →
-  adequate p e σ φ.
+Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
+  (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) →
+  adequate s e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index a8c487e7c7678c3c19a09077fdc4c23c2ceafb02..6061d0eb65a88f0d67eda52f20055180793e2d66 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -62,18 +62,18 @@ Implicit Types efs : list expr.
 Implicit Types σ : state.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
-Lemma wp_bind {p E e} K Φ :
-  WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }} ⊢ WP fill K e @ p; E {{ Φ }}.
+Lemma wp_bind {s E e} K Φ :
+  WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }} ⊢ WP fill K e @ s; E {{ Φ }}.
 Proof. exact: wp_ectx_bind. Qed.
 
-Lemma wp_bindi {p E e} Ki Φ :
-  WP e @ p; E {{ v, WP fill_item Ki (of_val v) @ p; E {{ Φ }} }} ⊢
-     WP fill_item Ki e @ p; E {{ Φ }}.
+Lemma wp_bindi {s E e} Ki Φ :
+  WP e @ s; E {{ v, WP fill_item Ki (of_val v) @ s; E {{ Φ }} }} ⊢
+     WP fill_item Ki e @ s; E {{ Φ }}.
 Proof. exact: weakestpre.wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork p E e Φ :
-  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ p; ⊤ {{ _, True }} ⊢ WP Fork e @ p; E {{ Φ }}.
+Lemma wp_fork s E e Φ :
+  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
   - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ _ (Lit _)) // right_id.
@@ -132,9 +132,9 @@ Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
 Proof. solve_pure_exec. Qed.
 
 (** Heap *)
-Lemma wp_alloc p E e v :
+Lemma wp_alloc s E e v :
   IntoVal e v →
-  {{{ True }}} Alloc e @ p; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
+  {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>"; iSplit; first by auto.
@@ -143,8 +143,8 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_load p E l q v :
-  {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ p; E {{{ RET v; l ↦{q} v }}}.
+Lemma wp_load s E l q v :
+  {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}.
 Proof.
   iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -153,9 +153,9 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_store p E l v' e v :
+Lemma wp_store s E l v' e v :
   IntoVal e v →
-  {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ p; E {{{ RET LitV LitUnit; l ↦ v }}}.
+  {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ s; E {{{ RET LitV LitUnit; l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
@@ -165,9 +165,9 @@ Proof.
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_fail p E l q v' e1 v1 e2 :
+Lemma wp_cas_fail s E l q v' e1 v1 e2 :
   IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
-  {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ p; E
+  {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
   {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
 Proof.
   iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) ">Hl HΦ".
@@ -177,9 +177,9 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_suc p E l e1 v1 e2 v2 :
+Lemma wp_cas_suc s E l e1 v1 e2 v2 :
   IntoVal e1 v1 → IntoVal e2 v2 →
-  {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ p; E
+  {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
   {{{ RET LitV (LitBool true); l ↦ v2 }}}.
 Proof.
   iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index c5d971d807cc8e8b3628966efe7175d5fd0682dd..0f95f3b9f44874d4a0052b39a848528bbda5d076 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -5,21 +5,21 @@ From iris.heap_lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma tac_wp_pure `{heapG Σ} K Δ Δ' p E e1 e2 φ Φ :
+Lemma tac_wp_pure `{heapG Σ} K Δ Δ' s E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
   IntoLaterNEnvs 1 Δ Δ' →
-  envs_entails Δ' (WP fill K e2 @ p; E {{ Φ }}) →
-  envs_entails Δ (WP fill K e1 @ p; E {{ Φ }}).
+  envs_entails Δ' (WP fill K e2 @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K e1 @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
   by rewrite -ectx_lifting.wp_ectx_bind_inv.
 Qed.
 
-Lemma tac_wp_value `{heapG Σ} Δ p E Φ e v :
+Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
   IntoVal e v →
-  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ p; E {{ Φ }}).
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
 
 Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
@@ -27,7 +27,7 @@ Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?p ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
     [simpl; apply _                 (* PureExec *)
@@ -52,9 +52,9 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
 Tactic Notation "wp_case" := wp_pure (Case _ _ _).
 Tactic Notation "wp_match" := wp_case; wp_let.
 
-Lemma tac_wp_bind `{heapG Σ} K Δ p E Φ e :
-  envs_entails Δ (WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }})%I →
-  envs_entails Δ (WP fill K e @ p; E {{ Φ }}).
+Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e :
+  envs_entails Δ (WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }})%I →
+  envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.
 
 Ltac wp_bind_core K :=
@@ -66,7 +66,7 @@ Ltac wp_bind_core K :=
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?p ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
     || fail "wp_bind: cannot find" efoc "in" e
   | _ => fail "wp_bind: not a 'wp'"
@@ -79,13 +79,13 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (iResUR Σ).
 
-Lemma tac_wp_alloc Δ Δ' p E j K e v Φ :
+Lemma tac_wp_alloc Δ Δ' s E j K e v Φ :
   IntoVal e v →
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ p; E {{ Φ }})) →
-  envs_entails Δ (WP fill K (Alloc e) @ p; E {{ Φ }}).
+    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ s; E {{ Φ }})) →
+  envs_entails Δ (WP fill K (Alloc e) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ?? HΔ.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
@@ -94,11 +94,11 @@ Proof.
   by rewrite right_id HΔ'.
 Qed.
 
-Lemma tac_wp_load Δ Δ' p E i K l q v Φ :
+Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  envs_entails Δ' (WP fill K (of_val v) @ p; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ p; E {{ Φ }}).
+  envs_entails Δ' (WP fill K (of_val v) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ???.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
@@ -106,13 +106,13 @@ Proof.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_store Δ Δ' Δ'' p E i K l v e v' Φ :
+Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
   IntoVal e v' →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  envs_entails Δ'' (WP fill K (Lit LitUnit) @ p; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ p; E {{ Φ }}).
+  envs_entails Δ'' (WP fill K (Lit LitUnit) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ?????.
   rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
@@ -120,12 +120,12 @@ Proof.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas_fail Δ Δ' p E i K l q v e1 v1 e2 Φ :
+Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
-  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ p; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ p; E {{ Φ }}).
+  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ??????.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
@@ -133,13 +133,13 @@ Proof.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas_suc Δ Δ' Δ'' p E i K l v e1 v1 e2 v2 Φ :
+Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
   IntoVal e1 v1 → IntoVal e2 v2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ p; E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ p; E {{ Φ }}).
+  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ???????; subst.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
@@ -151,7 +151,7 @@ End heap.
 Tactic Notation "wp_apply" open_constr(lem) :=
   iPoseProofCore lem as false true (fun H =>
     lazymatch goal with
-    | |- envs_entails _ (wp ?p ?E ?e ?Q) =>
+    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
         wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
       lazymatch iTypeOf H with
@@ -163,7 +163,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?p ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..])
@@ -182,7 +182,7 @@ Tactic Notation "wp_alloc" ident(l) :=
 Tactic Notation "wp_load" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?p ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
       |fail 1 "wp_load: cannot find 'Load' in" e];
@@ -196,7 +196,7 @@ Tactic Notation "wp_load" :=
 Tactic Notation "wp_store" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?p ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_store _ _ _ _ _ _ K); [apply _|..])
@@ -212,7 +212,7 @@ Tactic Notation "wp_store" :=
 Tactic Notation "wp_cas_fail" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?p ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..])
@@ -228,7 +228,7 @@ Tactic Notation "wp_cas_fail" :=
 Tactic Notation "wp_cas_suc" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?p ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [apply _|apply _|..])
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index f8920dd6e62cf3790e199a0639a4fa829589270c..a7f1bdd1d19dc7dc59e900ce4450365ce2988c29 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -34,24 +34,24 @@ Proof.
 Qed.
 
 (* Program logic adequacy *)
-Record adequate {Λ} (p : pbit) (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
+Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
   adequate_result t2 σ2 v2 :
    rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2;
   adequate_safe t2 σ2 e2 :
-   p = progress →
+   s = not_stuck →
    rtc step ([e1], σ1) (t2, σ2) →
    e2 ∈ t2 → progressive e2 σ2
 }.
 
 Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
-  adequate progress e1 σ1 φ →
+  adequate not_stuck e1 σ1 φ →
   rtc step ([e1], σ1) (t2, σ2) →
   Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
 Proof.
   intros Had ?.
   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 (adequate_safe progress e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
+  destruct (adequate_safe not_stuck e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
     rewrite ?eq_None_not_Some; auto.
   { exfalso. eauto. }
   destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
@@ -68,12 +68,12 @@ Implicit Types Φs : list (val Λ → iProp Σ).
 Notation world' E σ := (wsat ∗ ownE E ∗ state_interp σ)%I (only parsing).
 Notation world σ := (world' ⊤ σ) (only parsing).
 
-Notation wptp p t := ([∗ list] ef ∈ t, WP ef @ p; ⊤ {{ _, True }})%I.
+Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
 
-Lemma wp_step p E e1 σ1 e2 σ2 efs Φ :
+Lemma wp_step s E e1 σ1 e2 σ2 efs Φ :
   prim_step e1 σ1 e2 σ2 efs →
-  world' E σ1 ∗ WP e1 @ p; E {{ Φ }}
-  ==∗ ▷ |==> ◇ (world' E σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ wptp p efs).
+  world' E σ1 ∗ WP e1 @ s; E {{ Φ }}
+  ==∗ ▷ |==> ◇ (world' E σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
   rewrite (val_stuck e1 σ1 e2 σ2 efs) // fupd_eq /fupd_def.
@@ -82,10 +82,10 @@ Proof.
   iMod ("H" $! e2 σ2 efs with "[%] [$Hw $HE]") as ">($ & $ & $ & $)"; auto.
 Qed.
 
-Lemma wptp_step p e1 t1 t2 σ1 σ2 Φ :
+Lemma wptp_step s e1 t1 t2 σ1 σ2 Φ :
   step (e1 :: t1,σ1) (t2, σ2) →
-  world σ1 ∗ WP e1 @ p; ⊤ {{ Φ }} ∗ wptp p t1
-  ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 @ p; ⊤ {{ Φ }} ∗ wptp p t2').
+  world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
+  ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
   iIntros (Hstep) "(HW & He & Ht)".
   destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
@@ -96,11 +96,11 @@ Proof.
     iApply wp_step; eauto with iFrame.
 Qed.
 
-Lemma wptp_steps p n e1 t1 t2 σ1 σ2 Φ :
+Lemma wptp_steps s n e1 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  world σ1 ∗ WP e1 @ p; ⊤ {{ Φ }} ∗ wptp p t1 ⊢
+  world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢
   Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ WP e2 @ p; ⊤ {{ Φ }} ∗ wptp p t2').
+    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
   revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=.
   { inversion_clear 1; iIntros "?"; eauto 10. }
@@ -122,9 +122,9 @@ Proof.
   by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
 Qed.
 
-Lemma wptp_result p n e1 t1 v2 t2 σ1 σ2 φ :
+Lemma wptp_result s n e1 t1 v2 t2 σ1 σ2 φ :
   nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) →
-  world σ1 ∗ WP e1 @ p; ⊤ {{ v, ⌜φ v⌝ }} ∗ wptp p t1 ⊢ ▷^(S (S n)) ⌜φ v2⌝.
+  world σ1 ∗ WP e1 @ s; ⊤ {{ v, ⌜φ v⌝ }} ∗ wptp s t1 ⊢ ▷^(S (S n)) ⌜φ v2⌝.
 Proof.
   intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
   iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
@@ -144,7 +144,7 @@ Qed.
 
 Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp progress t1
+  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp not_stuck t1
   ⊢ ▷^(S (S n)) ⌜progressive e2 σ2⌝.
 Proof.
   intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
@@ -154,9 +154,9 @@ Proof.
   - iMod (wp_safe with "Hw [Htp]") as "$". by iApply (big_sepL_elem_of with "Htp").
 Qed.
 
-Lemma wptp_invariance p n e1 e2 t1 t2 σ1 σ2 φ Φ :
+Lemma wptp_invariance s n e1 e2 t1 t2 σ1 σ2 φ Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 @ p; ⊤ {{ Φ }} ∗ wptp p t1
+  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
   ⊢ ▷^(S (S n)) ⌜φ⌝.
 Proof.
   intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
@@ -167,12 +167,12 @@ Proof.
 Qed.
 End adequacy.
 
-Theorem wp_adequacy Σ Λ `{invPreG Σ} p e σ φ :
+Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
   (∀ `{Hinv : invG Σ},
      (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ ∗ WP e @ p; ⊤ {{ v, ⌜φ v⌝ }})%I) →
-  adequate p e σ φ.
+       stateI σ ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) →
+  adequate s e σ φ.
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n ?]%rtc_nsteps.
@@ -181,7 +181,7 @@ Proof.
     rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
     iDestruct "Hwp" as (Istate) "[HI Hwp]".
     iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
-  - destruct p; last done. intros t2 σ2 e2 _ [n ?]%rtc_nsteps ?.
+  - destruct s; last done. intros t2 σ2 e2 _ [n ?]%rtc_nsteps ?.
     eapply (soundness (M:=iResUR Σ) _ (S (S n))).
     iMod wsat_alloc as (Hinv) "[Hw HE]".
     rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
@@ -189,11 +189,11 @@ Proof.
     iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
 Qed.
 
-Theorem wp_invariance Σ Λ `{invPreG Σ} p e σ1 t2 σ2 φ :
+Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ},
      (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ1 ∗ WP e @ p; ⊤ {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) →
+       stateI σ1 ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) →
   rtc step ([e], σ1) (t2, σ2) →
   φ.
 Proof.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index bc417744dbbbdfe2cfc8f235156cbb7870daedb2..a3d0cb7684708402507ad5f82bf25013445236ee 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
 Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
-Implicit Types p : pbit.
+Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types v : val.
@@ -15,27 +15,27 @@ Hint Resolve head_prim_reducible head_reducible_prim_step.
 Hint Resolve (reducible_not_val _ inhabitant).
 Hint Resolve progressive_head_progressive.
 
-Lemma wp_ectx_bind {p E e} K Φ :
-  WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }}
-  ⊢ WP fill K e @ p; E {{ Φ }}.
+Lemma wp_ectx_bind {s E e} K Φ :
+  WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }}
+  ⊢ WP fill K e @ s; E {{ Φ }}.
 Proof. apply: weakestpre.wp_bind. Qed.
 
-Lemma wp_ectx_bind_inv {p E Φ} K e :
-  WP fill K e @ p; E {{ Φ }}
-  ⊢ WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }}.
+Lemma wp_ectx_bind_inv {s E Φ} K e :
+  WP fill K e @ s; E {{ Φ }}
+  ⊢ WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }}.
 Proof. apply: weakestpre.wp_bind_inv. Qed.
 
-Lemma wp_lift_head_step {p E Φ} e1 :
+Lemma wp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ p; E {{ Φ }}.
+      state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_step=>//. iIntros (σ1) "Hσ".
   iMod ("H" with "Hσ") as "[% H]"; iModIntro.
-  iSplit; first by destruct p; eauto. iNext. iIntros (e2 σ2 efs) "%".
+  iSplit; first by destruct s; eauto. iNext. iIntros (e2 σ2 efs) "%".
   iApply "H"; eauto.
 Qed.
 
@@ -48,15 +48,15 @@ Proof.
   iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto. 
 Qed.
 
-Lemma wp_lift_pure_head_step {p E E' Φ} e1 :
+Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
   (|={E,E'}▷=> ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
-    WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ p; E {{ Φ }}.
+    WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   iIntros (??) "H". iApply wp_lift_pure_step; eauto.
-  { by destruct p; auto. }
+  { by destruct s; auto. }
   iApply (step_fupd_wand with "H"); iIntros "H".
   iIntros (????). iApply "H"; eauto.
 Qed.
@@ -72,28 +72,28 @@ Proof using Hinh.
   move=>[] K [] e1 [] Hfill [] e2 [] σ2 [] efs /= Hstep. exact: Hnstep.
 Qed.
 
-Lemma wp_lift_atomic_head_step {p E Φ} e1 :
+Lemma wp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ p; E {{ Φ }}.
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
-  iSplit; first by destruct p; auto. iNext. iIntros (e2 σ2 efs) "%".
+  iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs) "%".
   iApply "H"; auto.
 Qed.
 
-Lemma wp_lift_atomic_head_step_no_fork {p E Φ} e1 :
+Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
       ⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
-  ⊢ WP e1 @ p; E {{ Φ }}.
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
@@ -101,29 +101,29 @@ Proof.
   iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
 Qed.
 
-Lemma wp_lift_pure_det_head_step {p E E' Φ} e1 e2 efs :
+Lemma wp_lift_pure_det_head_step {s E E' Φ} e1 e2 efs :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs',
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-  (|={E,E'}▷=> WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ p; E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 efs); eauto.
-  destruct p; by auto.
+  destruct s; by auto.
 Qed.
 
-Lemma wp_lift_pure_det_head_step_no_fork {p E E' Φ} e1 e2 :
+Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs',
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
-  (|={E,E'}▷=> WP e2 @ p; E {{ Φ }}) ⊢ WP e1 @ p; E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
-  destruct p; by auto.
+  destruct s; by auto.
 Qed.
 
-Lemma wp_lift_pure_det_head_step_no_fork' {p E Φ} e1 e2 :
+Lemma wp_lift_pure_det_head_step_no_fork' {s E Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs',
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index bacf594b100b77c1503315e173d690d7468e45cd..549db62c565dcf36658a84f1caf4ee943c56f5ff 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -3,83 +3,83 @@ From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition ht `{irisG Λ Σ} (p : pbit) (E : coPset) (P : iProp Σ)
+Definition ht `{irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
-  (□ (P -∗ WP e @ p; E {{ Φ }}))%I.
+  (□ (P -∗ WP e @ s; E {{ Φ }}))%I.
 Instance: Params (@ht) 5.
 
-Notation "{{ P } } e @ p ; E {{ Φ } }" := (ht p E P%I e%E Φ%I)
+Notation "{{ P } } e @ s ; E {{ Φ } }" := (ht s E P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
-   format "{{  P  } }  e  @  p ;  E  {{  Φ  } }") : C_scope.
-Notation "{{ P } } e @ E {{ Φ } }" := (ht progress E P%I e%E Φ%I)
+   format "{{  P  } }  e  @  s ;  E  {{  Φ  } }") : C_scope.
+Notation "{{ P } } e @ E {{ Φ } }" := (ht not_stuck E P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
-Notation "{{ P } } e @ E ? {{ Φ } }" := (ht noprogress E P%I e%E Φ%I)
+Notation "{{ P } } e @ E ? {{ Φ } }" := (ht maybe_stuck E P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  ? {{  Φ  } }") : C_scope.
-Notation "{{ P } } e {{ Φ } }" := (ht progress ⊤ P%I e%E Φ%I)
+Notation "{{ P } } e {{ Φ } }" := (ht not_stuck ⊤ P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : C_scope.
-Notation "{{ P } } e ? {{ Φ } }" := (ht noprogress ⊤ P%I e%E Φ%I)
+Notation "{{ P } } e ? {{ Φ } }" := (ht maybe_stuck ⊤ P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  ? {{  Φ  } }") : C_scope.
 
-Notation "{{ P } } e @ p ; E {{ v , Q } }" := (ht p E P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e @ s ; E {{ v , Q } }" := (ht s E P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
-   format "{{  P  } }  e  @  p ;  E  {{  v ,  Q  } }") : C_scope.
-Notation "{{ P } } e @ E {{ v , Q } }" := (ht progress E P%I e%E (λ v, Q)%I)
+   format "{{  P  } }  e  @  s ;  E  {{  v ,  Q  } }") : C_scope.
+Notation "{{ P } } e @ E {{ v , Q } }" := (ht not_stuck E P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
-Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht noprogress E P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht maybe_stuck E P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  ? {{  v ,  Q  } }") : C_scope.
-Notation "{{ P } } e {{ v , Q } }" := (ht progress ⊤ P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e {{ v , Q } }" := (ht not_stuck ⊤ P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.
-Notation "{{ P } } e ? {{ v , Q } }" := (ht noprogress ⊤ P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e ? {{ v , Q } }" := (ht maybe_stuck ⊤ P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  ? {{  v ,  Q  } }") : C_scope.
 
 Section hoare.
 Context `{irisG Λ Σ}.
-Implicit Types p : pbit.
+Implicit Types s : stuckness.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ Ψ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Import uPred.
 
-Global Instance ht_ne p E n :
-  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht p E).
+Global Instance ht_ne s E n :
+  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht s E).
 Proof. solve_proper. Qed.
-Global Instance ht_proper p E :
-  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht p E).
+Global Instance ht_proper s E :
+  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht s E).
 Proof. solve_proper. Qed.
-Lemma ht_mono p E P P' Φ Φ' e :
-  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ p; E {{ Φ' }} ⊢ {{ P }} e @ p; E {{ Φ }}.
+Lemma ht_mono s E P P' Φ Φ' e :
+  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ s; E {{ Φ' }} ⊢ {{ P }} e @ s; E {{ Φ }}.
 Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
-Global Instance ht_mono' p E :
-  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht p E).
+Global Instance ht_mono' s E :
+  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E).
 Proof. solve_proper. Qed.
 
-Lemma ht_alt p E P Φ e : (P ⊢ WP e @ p; E {{ Φ }}) → {{ P }} e @ p; E {{ Φ }}.
+Lemma ht_alt s E P Φ e : (P ⊢ WP e @ s; E {{ Φ }}) → {{ P }} e @ s; E {{ Φ }}.
 Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.
 
-Lemma ht_val p E v : {{ True }} of_val v @ p; E {{ v', ⌜v = v'⌝ }}.
+Lemma ht_val s E v : {{ True }} of_val v @ s; E {{ v', ⌜v = v'⌝ }}.
 Proof. iIntros "!# _". by iApply wp_value'. Qed.
 
-Lemma ht_vs p E P P' Φ Φ' e :
-  (P ={E}=> P') ∧ {{ P' }} e @ p; E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
-  ⊢ {{ P }} e @ p; E {{ Φ }}.
+Lemma ht_vs s E P P' Φ Φ' e :
+  (P ={E}=> P') ∧ {{ P' }} e @ s; E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
+  ⊢ {{ P }} e @ s; E {{ Φ }}.
 Proof.
   iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
   iApply wp_fupd. iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
-Lemma ht_atomic' p E1 E2 P P' Φ Φ' e :
-  StronglyAtomic e ∨ p = progress ∧ Atomic e →
-  (P ={E1,E2}=> P') ∧ {{ P' }} e @ p; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
-  ⊢ {{ P }} e @ p; E1 {{ Φ }}.
+Lemma ht_atomic' s E1 E2 P P' Φ Φ' e :
+  StronglyAtomic e ∨ s = not_stuck ∧ Atomic e →
+  (P ={E1,E2}=> P') ∧ {{ P' }} e @ s; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
+  ⊢ {{ P }} e @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic' _ _ E2); auto.
   iMod ("Hvs" with "HP") as "HP". iModIntro.
@@ -87,10 +87,10 @@ Proof.
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
-Lemma ht_strong_atomic p E1 E2 P P' Φ Φ' e :
+Lemma ht_strong_atomic s E1 E2 P P' Φ Φ' e :
   StronglyAtomic e →
-  (P ={E1,E2}=> P') ∧ {{ P' }} e @ p; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
-  ⊢ {{ P }} e @ p; E1 {{ Φ }}.
+  (P ={E1,E2}=> P') ∧ {{ P' }} e @ s; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
+  ⊢ {{ P }} e @ s; E1 {{ Φ }}.
 Proof. by eauto using ht_atomic'. Qed.
 
 Lemma ht_atomic E1 E2 P P' Φ Φ' e :
@@ -99,67 +99,67 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
   ⊢ {{ P }} e @ E1 {{ Φ }}.
 Proof. by eauto using ht_atomic'. Qed.
 
-Lemma ht_bind `{LanguageCtx Λ K} p E P Φ Φ' e :
-  {{ P }} e @ p; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ p; E {{ Φ' }})
-  ⊢ {{ P }} K e @ p; E {{ Φ' }}.
+Lemma ht_bind `{LanguageCtx Λ K} s E P Φ Φ' e :
+  {{ P }} e @ s; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
+  ⊢ {{ P }} K e @ s; E {{ Φ' }}.
 Proof.
   iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
   iApply (wp_wand with "[HP]"); [by iApply "Hwpe"|].
   iIntros (v) "Hv". by iApply "HwpK".
 Qed.
 
-Lemma ht_forget_progress p E P Φ e :
-  {{ P }} e @ p; E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
+Lemma ht_forget_not_stuck s E P Φ e :
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
 Proof.
-  by iIntros "#Hwp !# ?"; iApply wp_forget_progress; iApply "Hwp".
+  by iIntros "#Hwp !# ?"; iApply wp_forget_not_stuck; iApply "Hwp".
 Qed.
 
-Lemma ht_mask_weaken p E1 E2 P Φ e :
-  E1 ⊆ E2 → {{ P }} e @ p; E1 {{ Φ }} ⊢ {{ P }} e @ p; E2 {{ Φ }}.
+Lemma ht_mask_weaken s E1 E2 P Φ e :
+  E1 ⊆ E2 → {{ P }} e @ s; E1 {{ Φ }} ⊢ {{ P }} e @ s; E2 {{ Φ }}.
 Proof.
   iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono _ E1 E2); try done.
   by iApply "Hwp".
 Qed.
 
-Lemma ht_frame_l p E P Φ R e :
-  {{ P }} e @ p; E {{ Φ }} ⊢ {{ R ∗ P }} e @ p; E {{ v, R ∗ Φ v }}.
+Lemma ht_frame_l s E P Φ R e :
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ R ∗ P }} e @ s; E {{ v, R ∗ Φ v }}.
 Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.
 
-Lemma ht_frame_r p E P Φ R e :
-  {{ P }} e @ p; E {{ Φ }} ⊢ {{ P ∗ R }} e @ p; E {{ v, Φ v ∗ R }}.
+Lemma ht_frame_r s E P Φ R e :
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ R }} e @ s; E {{ v, Φ v ∗ R }}.
 Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
 
-Lemma ht_frame_step_l p E1 E2 P R1 R2 e Φ :
+Lemma ht_frame_step_l s E1 E2 P R1 R2 e Φ :
   to_val e = None → E2 ⊆ E1 →
-  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ p; E2 {{ Φ }}
-  ⊢ {{ R1 ∗ P }} e @ p; E1 {{ λ v, R2 ∗ Φ v }}.
+  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ s; E2 {{ Φ }}
+  ⊢ {{ R1 ∗ P }} e @ s; E1 {{ λ v, R2 ∗ Φ v }}.
 Proof.
   iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
   iApply (wp_frame_step_l _ E1 E2); try done.
   iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
 Qed.
 
-Lemma ht_frame_step_r p E1 E2 P R1 R2 e Φ :
+Lemma ht_frame_step_r s E1 E2 P R1 R2 e Φ :
   to_val e = None → E2 ⊆ E1 →
-  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ p; E2 {{ Φ }}
-  ⊢ {{ P ∗ R1 }} e @ p; E1 {{ λ v, Φ v ∗ R2 }}.
+  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ s; E2 {{ Φ }}
+  ⊢ {{ P ∗ R1 }} e @ s; E1 {{ λ v, Φ v ∗ R2 }}.
 Proof.
   iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
   iApply (wp_frame_step_r _ E1 E2); try done.
   iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
 Qed.
 
-Lemma ht_frame_step_l' p E P R e Φ :
+Lemma ht_frame_step_l' s E P R e Φ :
   to_val e = None →
-  {{ P }} e @ p; E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ p; E {{ v, R ∗ Φ v }}.
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ s; E {{ v, R ∗ Φ v }}.
 Proof.
   iIntros (?) "#Hwp !# [HR HP]".
   iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
 Qed.
 
-Lemma ht_frame_step_r' p E P Φ R e :
+Lemma ht_frame_step_r' s E P Φ R e :
   to_val e = None →
-  {{ P }} e @ p; E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ p; E {{ v, Φ v ∗ R }}.
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ s; E {{ v, Φ v ∗ R }}.
 Proof.
   iIntros (?) "#Hwp !# [HP HR]".
   iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index c78e841e57f91645411c25784ab8826d3af9b498..0bf6c5ee6e2d26d93691811bd8c3cbb505e7c04c 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -43,7 +43,7 @@ Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
 Instance language_ctx_id Λ : LanguageCtx Λ id.
 Proof. constructor; naive_solver. Qed.
 
-Variant pbit := progress | noprogress.
+Variant stuckness := not_stuck | maybe_stuck.
 
 Section language.
   Context {Λ : language}.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 1d4d09027118111ba246bb85bb021ba6a85c3eb9..f69906141067142a31e6665ef404504fe7406f1f 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -5,23 +5,23 @@ Set Default Proof Using "Type".
 
 Section lifting.
 Context `{irisG Λ Σ}.
-Implicit Types p : pbit.
+Implicit Types s : stuckness.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
-Lemma wp_lift_step p E Φ e1 :
+Lemma wp_lift_step s E Φ e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
-    ⌜if p then reducible e1 σ1 else True⌝ ∗
+    ⌜if s is not_stuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ p; E {{ Φ }}.
+      state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1) "Hσ".
-  iMod ("H" with "Hσ") as "(%&?)". iModIntro. iSplit. by destruct p. done.
+  iMod ("H" with "Hσ") as "(%&?)". iModIntro. iSplit. by destruct s. done.
 Qed.
 
 Lemma wp_lift_stuck E Φ e :
@@ -36,13 +36,13 @@ Proof.
 Qed.
 
 (** Derived lifting lemmas. *)
-Lemma wp_lift_pure_step `{Inhabited (state Λ)} p E E' Φ e1 :
+Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
   to_val e1 = None →
-  (∀ σ1, if p then reducible e1 σ1 else True) →
+  (∀ σ1, if s is not_stuck then reducible e1 σ1 else True) →
   (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
   (|={E,E'}▷=> ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
-    WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ p; E {{ Φ }}.
+    WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (? Hsafe Hstep) "H". iApply wp_lift_step; first done.
   iIntros (σ1) "Hσ". iMod "H".
@@ -65,16 +65,16 @@ Qed.
 
 (* Atomic steps don't need any mask-changing business here, one can
    use the generic lemmas here. *)
-Lemma wp_lift_atomic_step {p E Φ} e1 :
+Lemma wp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
-    ⌜if p then reducible e1 σ1 else True⌝ ∗
+    ⌜if s is not_stuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ p; E {{ Φ }}.
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step p E _ e1)=>//; iIntros (σ1) "Hσ1".
+  iIntros (?) "H". iApply (wp_lift_step s E _ e1)=>//; iIntros (σ1) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
   iModIntro; iNext; iIntros (e2 σ2 efs) "%". iMod "Hclose" as "_".
@@ -83,36 +83,36 @@ Proof.
   by iApply wp_value.
 Qed.
 
-Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {p E E' Φ} e1 e2 efs :
+Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
   to_val e1 = None →
-  (∀ σ1, if p then reducible e1 σ1 else true) →
+  (∀ σ1, if s is not_stuck then reducible e1 σ1 else true) →
   (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-  (|={E,E'}▷=> WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ p; E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?? Hpuredet) "H". iApply (wp_lift_pure_step p E E'); try done.
+  iIntros (?? Hpuredet) "H". iApply (wp_lift_pure_step s E E'); try done.
   { by intros; eapply Hpuredet. }
   iApply (step_fupd_wand with "H"); iIntros "H".
   by iIntros (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 
-Lemma wp_pure_step_fupd `{Inhabited (state Λ)} p E E' e1 e2 φ Φ :
+Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
-  (|={E,E'}▷=> WP e2 @ p; E {{ Φ }}) ⊢ WP e1 @ p; E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros ([??] Hφ) "HWP".
   iApply (wp_lift_pure_det_step with "[HWP]").
   - apply (reducible_not_val _ inhabitant). by auto.
-  - destruct p; naive_solver.
+  - destruct s; naive_solver.
   - naive_solver.
   - by rewrite big_sepL_nil right_id.
 Qed.
 
-Lemma wp_pure_step_later `{Inhabited (state Λ)} p E e1 e2 φ Φ :
+Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
-  ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
+  ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //.
 Qed.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 8500869f3345e9635f0724d9ed3ef930c3d8c361..a7c51e14eaeb3c3d53b11f40b21ac72bb55e2e95 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -39,9 +39,9 @@ Instance: Params (@ownP) 3.
 
 
 (* Adequacy *)
-Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} p e σ φ :
-  (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e @ p; ⊤ {{ v, ⌜φ v⌝ }}) →
-  adequate p e σ φ.
+Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ :
+  (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+  adequate s e σ φ.
 Proof.
   intros Hwp. apply (wp_adequacy Σ _).
   iIntros (?) "". iMod (own_alloc (● (Excl' (σ : leibnizC _)) ⋅ ◯ (Excl' σ)))
@@ -50,13 +50,13 @@ Proof.
   iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP.
 Qed.
 
-Theorem ownP_invariance Σ `{ownPPreG Λ Σ} p e σ1 t2 σ2 φ :
+Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
   (∀ `{ownPG Λ Σ},
-    ownP σ1 ={⊤}=∗ WP e @ p; ⊤ {{ _, True }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
+    ownP σ1 ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
   rtc step ([e], σ1) (t2, σ2) →
   φ σ2.
 Proof.
-  intros Hwp Hsteps. eapply (wp_invariance Σ Λ p e σ1 t2 σ2 _)=> //.
+  intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
   iIntros (?) "". iMod (own_alloc (● (Excl' (σ1 : leibnizC _)) ⋅ ◯ (Excl' σ1)))
     as (γσ) "[Hσ Hσf]"; first done.
   iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))). iFrame "Hσ".
@@ -70,7 +70,7 @@ Qed.
 (** Lifting *)
 Section lifting.
   Context `{ownPG Λ Σ}.
-  Implicit Types p : pbit.
+  Implicit Types s : stuckness.
   Implicit Types e : expr Λ.
   Implicit Types Φ : val Λ → iProp Σ.
 
@@ -85,12 +85,12 @@ Section lifting.
   Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) Σ _ σ).
   Proof. rewrite /ownP; apply _. Qed.
 
-  Lemma ownP_lift_step p E Φ e1 :
+  Lemma ownP_lift_step s E Φ e1 :
     to_val e1 = None →
-    (|={E,∅}=> ∃ σ1, ⌜if p then reducible e1 σ1 else True⌝ ∗ ▷ ownP σ1 ∗
+    (|={E,∅}=> ∃ σ1, ⌜if s is not_stuck then reducible e1 σ1 else True⌝ ∗ ▷ ownP σ1 ∗
       ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-            ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+            ={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (?) "H". iApply wp_lift_step; first done.
     iIntros (σ1) "Hσ"; iMod "H" as (σ1') "(% & >Hσf & H)".
@@ -115,79 +115,79 @@ Section lifting.
       by iDestruct (ownP_eq with "Hσ Hσf") as %->.
   Qed.
 
-  Lemma ownP_lift_pure_step p E Φ e1 :
+  Lemma ownP_lift_pure_step s E Φ e1 :
     to_val e1 = None →
-    (∀ σ1, if p then reducible e1 σ1 else True) →
+    (∀ σ1, if s is not_stuck then reducible e1 σ1 else True) →
     (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
     (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
-      WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+      WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (? Hsafe Hstep) "H"; iApply wp_lift_step; first done.
     iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-    iModIntro; iSplit; [by destruct p|]; iNext; iIntros (e2 σ2 efs ?).
+    iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
     destruct (Hstep σ1 e2 σ2 efs); auto; subst.
     by iMod "Hclose"; iModIntro; iFrame; iApply "H".
   Qed.
 
   (** Derived lifting lemmas. *)
-  Lemma ownP_lift_atomic_step {p E Φ} e1 σ1 :
+  Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
     to_val e1 = None →
-    (if p then reducible e1 σ1 else True) →
+    (if s is not_stuck then reducible e1 σ1 else True) →
     (▷ ownP σ1 ∗ ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (??) "[Hσ H]"; iApply ownP_lift_step; first done.
     iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-    iModIntro; iExists σ1; iFrame; iSplit; first by destruct p.
+    iModIntro; iExists σ1; iFrame; iSplit; first by destruct s.
     iNext; iIntros (e2 σ2 efs) "% Hσ".
     iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
     destruct (to_val e2) eqn:?; last by iExFalso.
     by iMod "Hclose"; iApply wp_value; auto using to_of_val.
   Qed.
 
-  Lemma ownP_lift_atomic_det_step {p E Φ e1} σ1 v2 σ2 efs :
+  Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :
     to_val e1 = None →
-    (if p then reducible e1 σ1 else True) →
+    (if s is not_stuck then reducible e1 σ1 else True) →
     (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
                      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
     ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
-      Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+      Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (?? Hdet) "[Hσ1 Hσ2]"; iApply ownP_lift_atomic_step; try done.
     iFrame; iNext; iIntros (e2' σ2' efs') "% Hσ2'".
     edestruct Hdet as (->&Hval&->). done. by rewrite Hval; iApply "Hσ2".
   Qed.
 
-  Lemma ownP_lift_atomic_det_step_no_fork {p E e1} σ1 v2 σ2 :
+  Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
     to_val e1 = None →
-    (if p then reducible e1 σ1 else True) →
+    (if s is not_stuck then reducible e1 σ1 else True) →
     (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
       σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
-    {{{ ▷ ownP σ1 }}} e1 @ p; E {{{ RET v2; ownP σ2 }}}.
+    {{{ ▷ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
   Proof.
     intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
     rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
   Qed.
 
-  Lemma ownP_lift_pure_det_step {p E Φ} e1 e2 efs :
+  Lemma ownP_lift_pure_det_step {s E Φ} e1 e2 efs :
     to_val e1 = None →
-    (∀ σ1, if p then reducible e1 σ1 else True) →
+    (∀ σ1, if s is not_stuck then reducible e1 σ1 else True) →
     (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-    ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+    ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤{{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (?? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
     by apply Hpuredet. by iNext; iIntros (e' efs' σ (_&->&->)%Hpuredet).
   Qed.
 
-  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {p E Φ} e1 e2 :
+  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
     to_val e1 = None →
-    (∀ σ1, if p then reducible e1 σ1 else True) →
+    (∀ σ1, if s is not_stuck then reducible e1 σ1 else True) →
     (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
-    ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
+    ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
   Qed.
@@ -197,23 +197,23 @@ Section ectx_lifting.
   Import ectx_language.
   Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
   Context `{ownPG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
-  Implicit Types p : pbit.
+  Implicit Types s : stuckness.
   Implicit Types Φ : val → iProp Σ.
   Implicit Types e : expr.
   Hint Resolve head_prim_reducible head_reducible_prim_step.
   Hint Resolve (reducible_not_val _ inhabitant).
   Hint Resolve progressive_head_progressive.
 
-  Lemma ownP_lift_head_step p E Φ e1 :
+  Lemma ownP_lift_head_step s E Φ e1 :
     to_val e1 = None →
     (|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
       ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-            ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+            ={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (?) "H". iApply ownP_lift_step; first done.
     iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1.
-    iSplit; first by destruct p; eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
+    iSplit; first by destruct s; eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
     iApply ("Hwp" with "[]"); eauto.
   Qed.
 
@@ -225,72 +225,72 @@ Section ectx_lifting.
     iModIntro. iExists σ. iFrame "Hσ". by eauto.
   Qed.
 
-  Lemma ownP_lift_pure_head_step p E Φ e1 :
+  Lemma ownP_lift_pure_head_step s E Φ e1 :
     to_val e1 = None →
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
     (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
-      WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+      WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
     iIntros (???) "H".  iApply ownP_lift_pure_step; eauto.
-    { by destruct p; auto. }
+    { by destruct s; auto. }
     iNext. iIntros (????). iApply "H"; eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_head_step {p E Φ} e1 σ1 :
+  Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 :
     to_val e1 = None →
     head_reducible e1 σ1 →
     ▷ ownP σ1 ∗ ▷ (∀ e2 σ2 efs,
     ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (??) "[? H]". iApply ownP_lift_atomic_step; eauto.
-    { by destruct p; eauto. }
+    { by destruct s; eauto. }
     iFrame. iNext. iIntros (???) "% ?". iApply ("H" with "[]"); eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_det_head_step {p E Φ e1} σ1 v2 σ2 efs :
+  Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 v2 σ2 efs :
     to_val e1 = None →
     head_reducible e1 σ1 →
     (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
       σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
-    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    by destruct p; eauto 10 using ownP_lift_atomic_det_step.
+    by destruct s; eauto 10 using ownP_lift_atomic_det_step.
   Qed.
 
-  Lemma ownP_lift_atomic_det_head_step_no_fork {p E e1} σ1 v2 σ2 :
+  Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 v2 σ2 :
     to_val e1 = None →
     head_reducible e1 σ1 →
     (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
       σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
-    {{{ ▷ ownP σ1 }}} e1 @ p; E {{{ RET v2; ownP σ2 }}}.
+    {{{ ▷ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
   Proof.
     intros ???; apply ownP_lift_atomic_det_step_no_fork; eauto.
-    by destruct p; eauto.
+    by destruct s; eauto.
   Qed.
 
-  Lemma ownP_lift_pure_det_head_step {p E Φ} e1 e2 efs :
+  Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
     to_val e1 = None →
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-    ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+    ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
     iIntros (???) "H"; iApply wp_lift_pure_det_step; eauto.
-    by destruct p; eauto.
+    by destruct s; eauto.
   Qed.
 
-  Lemma ownP_lift_pure_det_head_step_no_fork {p E Φ} e1 e2 :
+  Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
     to_val e1 = None →
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
-    ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
+    ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
     iIntros (???) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
-    by destruct p; eauto.
+    by destruct s; eauto.
   Qed.
 End ectx_lifting.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 16154c0b56fd9de35d30fe7d4c68c3426ec6a80d..8be71d97bc3cf06e5f6aa74bf906887727c00ba8 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -11,26 +11,26 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
-Definition wp_pre `{irisG Λ Σ} (p : pbit)
+Definition wp_pre `{irisG Λ Σ} (s : stuckness)
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
   | None => ∀ σ1,
-     state_interp σ1 ={E,∅}=∗ ⌜if p then reducible e1 σ1 else True⌝ ∗
+     state_interp σ1 ={E,∅}=∗ ⌜if s is not_stuck then reducible e1 σ1 else True⌝ ∗
      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
        state_interp σ2 ∗ wp E e2 Φ ∗
        [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
   end%I.
 
-Local Instance wp_pre_contractive `{irisG Λ Σ} p : Contractive (wp_pre p).
+Local Instance wp_pre_contractive `{irisG Λ Σ} s : Contractive (wp_pre s).
 Proof.
   rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
-Definition wp_def `{irisG Λ Σ} p :
-  coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre p).
+Definition wp_def `{irisG Λ Σ} s :
+  coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
 Definition wp_aux : seal (@wp_def). by eexists. Qed.
 Definition wp := unseal wp_aux.
 Definition wp_eq : @wp = @wp_def := seal_eq wp_aux.
@@ -38,44 +38,44 @@ Definition wp_eq : @wp = @wp_def := seal_eq wp_aux.
 Arguments wp {_ _ _} _ _ _%E _.
 Instance: Params (@wp) 6.
 
-Notation "'WP' e @ p ; E {{ Φ } }" := (wp p E e%E Φ)
+Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
   (at level 20, e, Φ at level 200,
-   format "'[' 'WP'  e  '/' @  p ;  E  {{  Φ  } } ']'") : uPred_scope.
-Notation "'WP' e @ E {{ Φ } }" := (wp progress E e%E Φ)
+   format "'[' 'WP'  e  '/' @  s ;  E  {{  Φ  } } ']'") : uPred_scope.
+Notation "'WP' e @ E {{ Φ } }" := (wp not_stuck E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' @  E  {{  Φ  } } ']'") : uPred_scope.
-Notation "'WP' e @ E ? {{ Φ } }" := (wp noprogress E e%E Φ)
+Notation "'WP' e @ E ? {{ Φ } }" := (wp maybe_stuck E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' @  E  ? {{  Φ  } } ']'") : uPred_scope.
-Notation "'WP' e {{ Φ } }" := (wp progress ⊤ e%E Φ)
+Notation "'WP' e {{ Φ } }" := (wp not_stuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : uPred_scope.
-Notation "'WP' e ? {{ Φ } }" := (wp noprogress ⊤ e%E Φ)
+Notation "'WP' e ? {{ Φ } }" := (wp maybe_stuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' ? {{  Φ  } } ']'") : uPred_scope.
 
-Notation "'WP' e @ p ; E {{ v , Q } }" := (wp p E e%E (λ v, Q))
+Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
-   format "'[' 'WP'  e  '/' @  p ;  E  {{  v ,  Q  } } ']'") : uPred_scope.
-Notation "'WP' e @ E {{ v , Q } }" := (wp progress E e%E (λ v, Q))
+   format "'[' 'WP'  e  '/' @  s ;  E  {{  v ,  Q  } } ']'") : uPred_scope.
+Notation "'WP' e @ E {{ v , Q } }" := (wp not_stuck E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' @  E  {{  v ,  Q  } } ']'") : uPred_scope.
-Notation "'WP' e @ E ? {{ v , Q } }" := (wp noprogress E e%E (λ v, Q))
+Notation "'WP' e @ E ? {{ v , Q } }" := (wp maybe_stuck E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' @  E  ? {{  v ,  Q  } } ']'") : uPred_scope.
-Notation "'WP' e {{ v , Q } }" := (wp progress ⊤ e%E (λ v, Q))
+Notation "'WP' e {{ v , Q } }" := (wp not_stuck ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' {{  v ,  Q  } } ']'") : uPred_scope.
-Notation "'WP' e ? {{ v , Q } }" := (wp noprogress ⊤ e%E (λ v, Q))
+Notation "'WP' e ? {{ v , Q } }" := (wp maybe_stuck ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' ? {{  v ,  Q  } } ']'") : uPred_scope.
 
 (* Texan triples *)
-Notation "'{{{' P } } } e @ p ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
+Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ p; E {{ Φ }})%I
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  p ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : uPred_scope.
+     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : uPred_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
@@ -96,10 +96,10 @@ Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  ? {{{  x .. y ,   RET  pat ;  Q } } }") : uPred_scope.
-Notation "'{{{' P } } } e @ p ; E {{{ 'RET' pat ; Q } } }" :=
-  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ p; E {{ Φ }})%I
+Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  p ;  E  {{{  RET  pat ;  Q } } }") : uPred_scope.
+     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q } } }") : uPred_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
     (at level 20,
@@ -117,11 +117,11 @@ Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
     (at level 20,
      format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q } } }") : uPred_scope.
 
-Notation "'{{{' P } } } e @ p ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
+Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ p; E {{ Φ }})
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  p ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
+     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})
@@ -142,10 +142,10 @@ Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  ? {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
-Notation "'{{{' P } } } e @ p ; E {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ p; E {{ Φ }})
+Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})
     (at level 20,
-     format "{{{  P  } } }  e  @  p ;  E  {{{  RET  pat ;  Q } } }") : C_scope.
+     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q } } }") : C_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})
     (at level 20,
@@ -165,18 +165,18 @@ Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
 
 Section wp.
 Context `{irisG Λ Σ}.
-Implicit Types p : pbit.
+Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 
 (* Weakest pre *)
-Lemma wp_unfold p E e Φ : WP e @ p; E {{ Φ }} ⊣⊢ wp_pre p (wp p) E e Φ.
-Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre p)). Qed.
+Lemma wp_unfold s E e Φ : WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp s) E e Φ.
+Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
 
-Global Instance wp_ne p E e n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ p E e).
+Global Instance wp_ne s E e n :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ s E e).
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
   rewrite !wp_unfold /wp_pre.
@@ -186,19 +186,19 @@ Proof.
   do 17 (f_contractive || f_equiv). apply IH; first lia.
   intros v. eapply dist_le; eauto with omega.
 Qed.
-Global Instance wp_proper p E e :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ _ p E e).
+Global Instance wp_proper s E e :
+  Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ _ s E e).
 Proof.
   by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
 
-Lemma wp_value' p E Φ v : Φ v ⊢ WP of_val v @ p; E {{ Φ }}.
+Lemma wp_value' s E Φ v : Φ v ⊢ WP of_val v @ s; E {{ Φ }}.
 Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
-Lemma wp_value_inv p E Φ v : WP of_val v @ p; E {{ Φ }} ={E}=∗ Φ v.
+Lemma wp_value_inv s E Φ v : WP of_val v @ s; E {{ Φ }} ={E}=∗ Φ v.
 Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
 
-Lemma wp_strong_mono p E1 E2 e Φ Ψ :
-  E1 ⊆ E2 → (∀ v, Φ v ={E2}=∗ Ψ v) ∗ WP e @ p; E1 {{ Φ }} ⊢ WP e @ p; E2 {{ Ψ }}.
+Lemma wp_strong_mono s E1 E2 e Φ Ψ :
+  E1 ⊆ E2 → (∀ v, Φ v ={E2}=∗ Ψ v) ∗ WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Ψ }}.
 Proof.
   iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
@@ -210,8 +210,8 @@ Proof.
   iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
 Qed.
 
-Lemma wp_forget_progress p E e Φ :
-  WP e @ p; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
+Lemma wp_forget_not_stuck s E e Φ :
+  WP e @ s; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|]; first iExact "H".
@@ -224,18 +224,18 @@ Proof.
   iSplitL "Hef". by iApply ("IH" with "Hef"). exact: IH. 
 Qed.
 
-Lemma fupd_wp p E e Φ : (|={E}=> WP e @ p; E {{ Φ }}) ⊢ WP e @ p; E {{ Φ }}.
+Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ }}.
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
   iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
 Qed.
-Lemma wp_fupd p E e Φ : WP e @ p; E {{ v, |={E}=> Φ v }} ⊢ WP e @ p; E {{ Φ }}.
-Proof. iIntros "H". iApply (wp_strong_mono p E); try iFrame; auto. Qed.
+Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
+Proof. iIntros "H". iApply (wp_strong_mono s E); try iFrame; auto. Qed.
 
-Lemma wp_atomic' p E1 E2 e Φ :
-  StronglyAtomic e ∨ p = progress ∧ Atomic e →
-  (|={E1,E2}=> WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ p; E1 {{ Φ }}.
+Lemma wp_atomic' s E1 E2 e Φ :
+  StronglyAtomic e ∨ s = not_stuck ∧ Atomic e →
+  (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
 Proof.
   iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|].
@@ -246,34 +246,34 @@ Proof.
   - destruct (Hstrong _ _ _ _ Hstep) as [v <-%of_to_val].
     iMod ("H" with "[#]") as "($ & H & $)"; first done.
     iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
-  - destruct p; last done. iMod ("H" with "[//]") as "(Hphy & H & $)".
+  - destruct s; last done. iMod ("H" with "[//]") as "(Hphy & H & $)".
     rewrite !wp_unfold /wp_pre. destruct (to_val e2).
     + iDestruct "H" as ">> $". by iFrame.
     + iMod ("H" with "[$]") as "[H _]".
       iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hweak _ _ _ _ Hstep).
 Qed.
 
-Lemma wp_step_fupd p E1 E2 e P Φ :
+Lemma wp_step_fupd s E1 E2 e P Φ :
   to_val e = None → E2 ⊆ E1 →
-  (|={E1,E2}▷=> P) -∗ WP e @ p; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ p; E1 {{ Φ }}.
+  (|={E1,E2}▷=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; E1 {{ Φ }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
   iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
   iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
-  iMod "HR". iModIntro. iApply (wp_strong_mono p E2); first done.
+  iMod "HR". iModIntro. iApply (wp_strong_mono s E2); first done.
   iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
 Qed.
 
-Lemma wp_bind K `{!LanguageCtx Λ K} p E e Φ :
-  WP e @ p; E {{ v, WP K (of_val v) @ p; E {{ Φ }} }} ⊢ WP K e @ p; E {{ Φ }}.
+Lemma wp_bind K `{!LanguageCtx Λ K} s E e Φ :
+  WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }} ⊢ WP K e @ s; E {{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by iApply fupd_wp. }
   rewrite wp_unfold /wp_pre fill_not_val //.
   iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
-  { iPureIntro. destruct p; last done.
+  { iPureIntro. destruct s; last done.
     unfold reducible in *. naive_solver eauto using fill_step. }
   iNext; iIntros (e2 σ2 efs Hstep).
   destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
@@ -281,86 +281,86 @@ Proof.
   by iApply "IH".
 Qed.
 
-Lemma wp_bind_inv K `{!LanguageCtx Λ K} p E e Φ :
-  WP K e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, WP K (of_val v) @ p; E {{ Φ }} }}.
+Lemma wp_bind_inv K `{!LanguageCtx Λ K} s E e Φ :
+  WP K e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
   rewrite fill_not_val //.
   iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
-  { destruct p; eauto using reducible_fill. }
+  { destruct s; eauto using reducible_fill. }
   iNext; iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! (K e2) σ2 efs with "[]") as "($ & H & $)"; eauto using fill_step.
   by iApply "IH".
 Qed.
 
 (** * Derived rules *)
-Lemma wp_mono p E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ Ψ }}.
+Lemma wp_mono s E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ Ψ }}.
 Proof.
-  iIntros (HΦ) "H"; iApply (wp_strong_mono p E E); auto.
+  iIntros (HΦ) "H"; iApply (wp_strong_mono s E E); auto.
   iIntros "{$H}" (v) "?". by iApply HΦ.
 Qed.
-Lemma wp_mask_mono p E1 E2 e Φ : E1 ⊆ E2 → WP e @ p; E1 {{ Φ }} ⊢ WP e @ p; E2 {{ Φ }}.
-Proof. iIntros (?) "H"; iApply (wp_strong_mono p E1 E2); auto. iFrame; eauto. Qed.
-Global Instance wp_mono' p E e :
-  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ p E e).
+Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
+Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. Qed.
+Global Instance wp_mono' s E e :
+  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ s E e).
 Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
 
-Lemma wp_value p E Φ e v `{!IntoVal e v} : Φ v ⊢ WP e @ p; E {{ Φ }}.
+Lemma wp_value s E Φ e v `{!IntoVal e v} : Φ v ⊢ WP e @ s; E {{ Φ }}.
 Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
-Lemma wp_value_fupd' p E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ p; E {{ Φ }}.
+Lemma wp_value_fupd' s E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ s; E {{ Φ }}.
 Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
-Lemma wp_value_fupd p E Φ e v `{!IntoVal e v} :
-  (|={E}=> Φ v) ⊢ WP e @ p; E {{ Φ }}.
+Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
+  (|={E}=> Φ v) ⊢ WP e @ s; E {{ Φ }}.
 Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
 
-Lemma wp_strong_atomic p E1 E2 e Φ :
+Lemma wp_strong_atomic s E1 E2 e Φ :
   StronglyAtomic e →
-  (|={E1,E2}=> WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ p; E1 {{ Φ }}.
+  (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
 Proof. by eauto using wp_atomic'. Qed.
 Lemma wp_atomic E1 E2 e Φ :
   Atomic e →
   (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
 Proof. by eauto using wp_atomic'. Qed.
 
-Lemma wp_frame_l p E e Φ R : R ∗ WP e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, R ∗ Φ v }}.
-Proof. iIntros "[??]". iApply (wp_strong_mono p E E _ Φ); try iFrame; eauto. Qed.
-Lemma wp_frame_r p E e Φ R : WP e @ p; E {{ Φ }} ∗ R ⊢ WP e @ p; E {{ v, Φ v ∗ R }}.
-Proof. iIntros "[??]". iApply (wp_strong_mono p E E _ Φ); try iFrame; eauto. Qed.
+Lemma wp_frame_l s E e Φ R : R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
+Proof. iIntros "[??]". iApply (wp_strong_mono s E E _ Φ); try iFrame; eauto. Qed.
+Lemma wp_frame_r s E e Φ R : WP e @ s; E {{ Φ }} ∗ R ⊢ WP e @ s; E {{ v, Φ v ∗ R }}.
+Proof. iIntros "[??]". iApply (wp_strong_mono s E E _ Φ); try iFrame; eauto. Qed.
 
-Lemma wp_frame_step_l p E1 E2 e Φ R :
+Lemma wp_frame_step_l s E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
-  (|={E1,E2}▷=> R) ∗ WP e @ p; E2 {{ Φ }} ⊢ WP e @ p; E1 {{ v, R ∗ Φ v }}.
+  (|={E1,E2}▷=> R) ∗ WP e @ s; E2 {{ Φ }} ⊢ WP e @ s; E1 {{ v, R ∗ Φ v }}.
 Proof.
   iIntros (??) "[Hu Hwp]". iApply (wp_step_fupd with "Hu"); try done.
   iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
 Qed.
-Lemma wp_frame_step_r p E1 E2 e Φ R :
+Lemma wp_frame_step_r s E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
-  WP e @ p; E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ WP e @ p; E1 {{ v, Φ v ∗ R }}.
+  WP e @ s; E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ WP e @ s; E1 {{ v, Φ v ∗ R }}.
 Proof.
   rewrite [(WP _ @ _; _ {{ _ }} ∗ _)%I]comm; setoid_rewrite (comm _ _ R).
   apply wp_frame_step_l.
 Qed.
-Lemma wp_frame_step_l' p E e Φ R :
-  to_val e = None → ▷ R ∗ WP e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, R ∗ Φ v }}.
-Proof. iIntros (?) "[??]". iApply (wp_frame_step_l p E E); try iFrame; eauto. Qed.
-Lemma wp_frame_step_r' p E e Φ R :
-  to_val e = None → WP e @ p; E {{ Φ }} ∗ ▷ R ⊢ WP e @ p; E {{ v, Φ v ∗ R }}.
-Proof. iIntros (?) "[??]". iApply (wp_frame_step_r p E E); try iFrame; eauto. Qed.
-
-Lemma wp_wand p E e Φ Ψ :
-  WP e @ p; E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ p; E {{ Ψ }}.
+Lemma wp_frame_step_l' s E e Φ R :
+  to_val e = None → ▷ R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
+Proof. iIntros (?) "[??]". iApply (wp_frame_step_l s E E); try iFrame; eauto. Qed.
+Lemma wp_frame_step_r' s E e Φ R :
+  to_val e = None → WP e @ s; E {{ Φ }} ∗ ▷ R ⊢ WP e @ s; E {{ v, Φ v ∗ R }}.
+Proof. iIntros (?) "[??]". iApply (wp_frame_step_r s E E); try iFrame; eauto. Qed.
+
+Lemma wp_wand s E e Φ Ψ :
+  WP e @ s; E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E {{ Ψ }}.
 Proof.
-  iIntros "Hwp H". iApply (wp_strong_mono p E); auto.
+  iIntros "Hwp H". iApply (wp_strong_mono s E); auto.
   iIntros "{$Hwp}" (?) "?". by iApply "H".
 Qed.
-Lemma wp_wand_l p E e Φ Ψ :
-  (∀ v, Φ v -∗ Ψ v) ∗ WP e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ Ψ }}.
+Lemma wp_wand_l s E e Φ Ψ :
+  (∀ v, Φ v -∗ Ψ v) ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ Ψ }}.
 Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
-Lemma wp_wand_r p E e Φ Ψ :
-  WP e @ p; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ p; E {{ Ψ }}.
+Lemma wp_wand_r s E e Φ Ψ :
+  WP e @ s; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ s; E {{ Ψ }}.
 Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
 End wp.
 
@@ -370,26 +370,26 @@ Section proofmode_classes.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.
 
-  Global Instance frame_wp p p' E e R Φ Ψ :
-    (∀ v, Frame p' R (Φ v) (Ψ v)) → Frame p' R (WP e @ p; E {{ Φ }}) (WP e @ p; E {{ Ψ }}).
+  Global Instance frame_wp p s E e R Φ Ψ :
+    (∀ v, Frame p R (Φ v) (Ψ v)) → Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
   Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 
-  Global Instance is_except_0_wp p E e Φ : IsExcept0 (WP e @ p; E {{ Φ }}).
+  Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
 
-  Global Instance elim_modal_bupd_wp p E e P Φ :
-    ElimModal (|==> P) P (WP e @ p; E {{ Φ }}) (WP e @ p; E {{ Φ }}).
+  Global Instance elim_modal_bupd_wp s E e P Φ :
+    ElimModal (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
 
-  Global Instance elim_modal_fupd_wp p E e P Φ :
-    ElimModal (|={E}=> P) P (WP e @ p; E {{ Φ }}) (WP e @ p; E {{ Φ }}).
+  Global Instance elim_modal_fupd_wp s E e P Φ :
+    ElimModal (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
   (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
   Global Instance elim_modal_fupd_wp_strong_atomic E1 E2 e P Φ :
     StronglyAtomic e →
     ElimModal (|={E1,E2}=> P) P
-            (WP e @ p; E1 {{ Φ }}) (WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
+            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_strong_atomic. Qed.
 
   (* lower precedence than elim_modal_fupd_wp_strong_atomic (for no good reason) *)
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 256a93e2f9e82d3cdf810cccbd00b882821cca4f..2771e3101b45f042b7d9a192688028b0fca54c30 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -86,5 +86,5 @@ Section LiftingTests.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
-Lemma heap_e_adequate σ : adequate progress heap_e σ (= #2).
+Lemma heap_e_adequate σ : adequate not_stuck heap_e σ (= #2).
 Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.