diff --git a/_CoqProject b/_CoqProject
index bdd1e49cef0bf97b722e2eb78b4bc6073f521fe1..e85ee72a66801eacbffcbde49139561c66d03e8c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -76,7 +76,7 @@ theories/program_logic/language.v
 theories/program_logic/ectx_language.v
 theories/program_logic/ectxi_language.v
 theories/program_logic/ectx_lifting.v
-theories/program_logic/ownp.v
+#theories/program_logic/ownp.v
 theories/program_logic/total_lifting.v
 theories/program_logic/total_ectx_lifting.v
 theories/program_logic/atomic.v
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 1b7dfabb92db6399fb7d7ba33ffcecb1a42d5e7e..d477c462f601cfb92af3c3e36288f0c5ec840d53 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -17,8 +17,8 @@ Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
   (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) →
   adequate s e σ (λ v _, φ v).
 Proof.
-  intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
+  intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
   iMod (gen_heap_init σ) as (?) "Hh".
-  iModIntro. iExists gen_heap_ctx. iFrame "Hh".
+  iModIntro. iExists (fun σ _ => gen_heap_ctx σ). iFrame "Hh".
   iApply (Hwp (HeapG _ _ _)).
 Qed.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index ad92c97cec6a727775f2c4bd1299c7c63bc02aca..a5ae44a3b3b8fcb17690cf31235c0bf06cad1648 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -108,7 +108,7 @@ Inductive val :=
 
 Bind Scope val_scope with val.
 
-Inductive observation := prophecy_observation_todo.
+Definition observation := Empty val.
 
 Fixpoint of_val (v : val) : expr :=
   match v with
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index aed8e60024a740b94c971ce5f1b30394ba83d61a..3f2f29dd41b0d57004978d8b11a8768a7adc3a05 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -14,7 +14,7 @@ Class heapG Σ := HeapG {
 
 Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
   iris_invG := heapG_invG;
-  state_interp := gen_heap_ctx
+  state_interp σ κs := gen_heap_ctx σ
 }.
 
 (** Override the notations so that scopes and coercions work out *)
@@ -112,6 +112,7 @@ Proof.
   iApply wp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
   iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
 Qed.
+
 Lemma twp_fork s E e Φ :
   WP e @ s; ⊤ [{ _, True }] -∗ Φ (LitV LitUnit) -∗ WP Fork e @ s; E [{ Φ }].
 Proof.
@@ -126,8 +127,8 @@ Lemma wp_alloc s E e v :
   {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
   iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>"; iSplit; first by eauto.
-  iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs) "Hσ !>"; iSplit; first by eauto.
+  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
@@ -136,8 +137,8 @@ Lemma twp_alloc s E e v :
   [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
 Proof.
   iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>"; iSplit; first by eauto.
-  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs) "Hσ !>"; iSplit; first by eauto.
+  iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
@@ -146,18 +147,18 @@ 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 %?.
+  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto.
-  iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_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 twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto.
-  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
@@ -167,8 +168,8 @@ Lemma wp_store s E l v' e 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 %?.
-  iSplit; first by eauto 6. iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto 6. iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
@@ -178,8 +179,8 @@ Lemma twp_store s E l v' e v :
 Proof.
   iIntros (<- Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto 6. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto 6. iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
@@ -191,8 +192,8 @@ Lemma wp_cas_fail s E l q v' e1 v1 e2 :
 Proof.
   iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_cas_fail s E l q v' e1 v1 e2 :
@@ -202,8 +203,8 @@ Lemma twp_cas_fail s E l q v' e1 v1 e2 :
 Proof.
   iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
@@ -214,8 +215,8 @@ Lemma wp_cas_suc s E l e1 v1 e2 v2 :
 Proof.
   iIntros (<- <- ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
@@ -226,8 +227,8 @@ Lemma twp_cas_suc s E l e1 v1 e2 v2 :
 Proof.
   iIntros (<- <- ? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
@@ -239,8 +240,8 @@ Lemma wp_faa s E l i1 e2 i2 :
 Proof.
   iIntros (<- Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
@@ -251,8 +252,8 @@ Lemma twp_faa s E l i1 e2 i2 :
 Proof.
   iIntros (<- Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index e2324fd403309de1cc3c35b452bb0fdd9f2d83ba..de11f87f6cfecfa5a34e78de0a0b728908c71dae 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -40,6 +40,7 @@ Proof.
   rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite HΔ' -lifting.wp_pure_step_later //.
 Qed.
+
 Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 838357376916c83fcea20449fd99a06af8436533..7cb9e7932a783d75a3eee270efce3a174f327e24 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -4,12 +4,15 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
+(* TODO (MR) re-introduce lemma after we prove twp_total *)
+(*
 Definition heap_total Σ `{heapPreG Σ} s e σ φ :
   (∀ `{heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]%I) →
   sn erased_step ([e], σ).
 Proof.
-  intros Hwp; eapply (twp_total _ _); iIntros (?) "".
+  intros Hwp; eapply (twp_total _ _) with (κs := []); iIntros (?) "".
   iMod (gen_heap_init σ) as (?) "Hh".
-  iModIntro. iExists gen_heap_ctx; iFrame.
+  iModIntro. iExists (fun σ _ => gen_heap_ctx σ); iFrame.
   iApply (Hwp (HeapG _ _ _)).
 Qed.
+*)
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 43d9dddf2d1a688783e219fc38724bcfde9e2d2e..b5e3cf8569a52fac3e231493bcff9b2bcdb1ac5e 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -66,50 +66,50 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
 
-Notation world' E σ := (wsat ∗ ownE E ∗ state_interp σ)%I (only parsing).
-Notation world σ := (world' ⊤ σ) (only parsing).
+Notation world' E σ κs := (wsat ∗ ownE E ∗ state_interp σ κs)%I (only parsing).
+Notation world σ κs := (world' ⊤ σ κs) (only parsing).
 
 Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
 
-Lemma wp_step s E e1 σ1 κ e2 σ2 efs Φ :
+Lemma wp_step s E e1 σ1 κ κs e2 σ2 efs Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
-  world' E σ1 ∗ WP e1 @ s; E {{ Φ }}
-  ==∗ ▷ |==> ◇ (world' E σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs).
+  world' E σ1 (cons_obs κ κs) ∗ WP e1 @ s; E {{ Φ }}
+  ==∗  ▷ |==> ◇ (world' E σ2 κs ∗ 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) // uPred_fupd_eq.
-  iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
-  iMod ("H" $! κ e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
+  iMod ("H" $! σ1 _ with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
+  iMod ("H" $! κ κs e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
   iIntros "!> !>". by iMod ("H" with "[$Hw $HE]") as ">($ & $ & $)".
 Qed.
 
-(* should we be able to say that κs = κ :: κs'? *)
-Lemma wptp_step s e1 t1 t2 κ σ1 σ2 Φ :
+Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
   step (e1 :: t1,σ1) κ (t2, σ2) →
-  world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
+  world σ1 (cons_obs κ κs) ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
   ==∗ ∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
+    ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 κs ∗ 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/=.
-  - iExists e2', (t2' ++ efs); iSplitR; first by eauto.
+  - iExists e2', (t2' ++ efs). iSplitR; first by eauto.
     iFrame "Ht". iApply wp_step; eauto with iFrame.
   - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
     iDestruct "Ht" as "($ & He' & $)". iFrame "He".
     iApply wp_step; eauto with iFrame.
 Qed.
 
-Lemma wptp_steps s n e1 t1 κs t2 σ1 σ2 Φ :
+Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
-  world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢
+  world σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢
   Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
+    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 κs' ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
-  revert e1 t1 κs t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs t2 σ1 σ2 /=.
+  revert e1 t1 κs κs' t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
   { inversion_clear 1; iIntros "?"; eauto 10. }
   iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
-  iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
-  iModIntro; iNext; iMod "H" as ">?". by iApply IH.
+  rewrite /cons_obs. rewrite <- app_assoc.
+  iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first by eauto; simplify_eq.
+  subst. iModIntro; iNext; iMod "H" as ">H". by iApply IH.
 Qed.
 
 Lemma bupd_iter_laterN_mono n P Q `{!Plain Q} :
@@ -125,9 +125,11 @@ Proof.
   by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
 Qed.
 
-Lemma wptp_result s n e1 t1 κs v2 t2 σ1 σ2 φ :
+Lemma wptp_result s n e1 t1 κs κs' v2 t2 σ1 σ2 φ :
   nsteps n (e1 :: t1, σ1) κs (of_val v2 :: t2, σ2) →
-  world σ1 ∗ WP e1 @ s; ⊤ {{ v, ∀ σ, state_interp σ ={⊤,∅}=∗ ⌜φ v σ⌝ }} ∗ wptp s t1
+  world σ1 (κs ++ κs') ∗
+  WP e1 @ s; ⊤ {{ v, ∀ σ, state_interp σ κs' ={⊤,∅}=∗ ⌜φ v σ⌝ }} ∗
+  wptp s t1
   ⊢ ▷^(S (S n)) ⌜φ v2 σ2⌝.
 Proof.
   intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
@@ -137,8 +139,8 @@ Proof.
   iMod ("H" with "Hσ [$]") as ">(_ & _ & $)".
 Qed.
 
-Lemma wp_safe E e σ Φ :
-  world' E σ -∗ WP e @ E {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
+Lemma wp_safe E e σ κs Φ :
+  world' E σ κs -∗ WP e @ E {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
   destruct (to_val e) as [v|] eqn:?.
@@ -147,9 +149,9 @@ Proof.
   iIntros "!> !> !%". by right.
 Qed.
 
-Lemma wptp_safe n e1 κs e2 t1 t2 σ1 σ2 Φ :
+Lemma wptp_safe n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) → e2 ∈ t2 →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp NotStuck t1
+  world σ1 (κs ++ κs') ∗ WP e1 {{ Φ }} ∗ wptp NotStuck t1
   ⊢ ▷^(S (S n)) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
 Proof.
   intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
@@ -159,9 +161,9 @@ Proof.
   - iMod (wp_safe with "Hw [Htp]") as "$". by iApply (big_sepL_elem_of with "Htp").
 Qed.
 
-Lemma wptp_invariance s n e1 κs e2 t1 t2 σ1 σ2 φ Φ :
+Lemma wptp_invariance s n e1 κs κs' e2 t1 t2 σ1 σ2 φ Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
-  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
+  (state_interp σ2 κs' ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
   ⊢ ▷^(S (S n)) ⌜φ⌝.
 Proof.
   intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
@@ -173,68 +175,70 @@ Qed.
 End adequacy.
 
 Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
-  (∀ `{Hinv : invG Σ},
-     (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ ∗ WP e @ s; ⊤ {{ v, ∀ σ, stateI σ ={⊤,∅}=∗ ⌜φ v σ⌝ }})%I) →
+  (∀ `{Hinv : invG Σ} κs,
+     (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
+       stateI σ κs ∗ WP e @ s; ⊤ {{ v, ∀ σ, stateI σ [] ={⊤,∅}=∗ ⌜φ v σ⌝ }})%I) →
   adequate s e σ φ.
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n [κs ?]]%erased_steps_nsteps.
     eapply (soundness (M:=iResUR Σ) _ (S (S n))).
-    iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
+    iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs).
     rewrite {1}uPred_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.
+    iApply (@wptp_result _ _ (IrisG _ _ _ Hinv Istate) _ _ _ _ _ []); last first.
+    rewrite app_nil_r. all: eauto with iFrame.
   - destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?.
     eapply (soundness (M:=iResUR Σ) _ (S (S n))).
-    iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
+    iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs).
     rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
     iDestruct "Hwp" as (Istate) "[HI Hwp]".
-    iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
+    iApply (@wptp_safe _ _ (IrisG _ _ _ Hinv Istate) _ _ _ []); last first.
+    rewrite app_nil_r. all: eauto with iFrame.
 Qed.
 
 Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
-  (∀ `{Hinv : invG Σ},
-     (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) →
+  (∀ `{Hinv : invG Σ} κs,
+     (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
+       stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) →
   adequate s e σ (λ v _, φ v).
 Proof.
-  intros Hwp. apply (wp_strong_adequacy Σ _)=> Hinv.
+  intros Hwp. apply (wp_strong_adequacy Σ _)=> Hinv κs.
   iMod Hwp as (stateI) "[Hσ H]". iExists stateI. iIntros "{$Hσ} !>".
   iApply (wp_wand with "H"). iIntros (v ? σ') "_".
   iMod (fupd_intro_mask' ⊤ ∅) as "_"; auto.
 Qed.
 
 Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
-  (∀ `{Hinv : invG Σ},
-     (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ1 ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) →
+  (∀ `{Hinv : invG Σ} κs κs',
+     (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
+       stateI σ1 (κs ++ κs') ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 κs' ={⊤,∅}=∗ ⌜φ⌝))%I) →
   rtc erased_step ([e], σ1) (t2, σ2) →
   φ.
 Proof.
   intros Hwp [n [κs ?]]%erased_steps_nsteps.
   eapply (soundness (M:=iResUR Σ) _ (S (S n))).
-  iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
+  iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs []).
   rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
   iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
-  iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
+  iApply (@wptp_invariance _ _ (IrisG _ _ _ Hinv Istate)); eauto with iFrame.
 Qed.
 
 (* An equivalent version that does not require finding [fupd_intro_mask'], but
 can be confusing to use. *)
 Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
-  (∀ `{Hinv : invG Σ},
-     (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ1 ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 -∗ ∃ E, |={⊤,E}=> ⌜φ⌝))%I) →
+  (∀ `{Hinv : invG Σ} κs κs',
+     (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
+       stateI σ1 κs ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 κs' -∗ ∃ E, |={⊤,E}=> ⌜φ⌝))%I) →
   rtc erased_step ([e], σ1) (t2, σ2) →
   φ.
 Proof.
   intros Hwp. eapply wp_invariance; first done.
-  intros Hinv. iMod (Hwp Hinv) as (stateI) "(? & ? & Hφ)".
+  intros Hinv κs κs'. iMod (Hwp Hinv) as (stateI) "(? & ? & Hφ)".
   iModIntro. iExists stateI. iFrame. iIntros "Hσ".
   iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
   iMod (fupd_intro_mask') as "_"; last by iModIntro. solve_ndisj.
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 45741b260416bab5bbf0a5fc4903b51273de674e..475b7836d13cc305dfa2d300a5f710dd277ba6e3 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -16,7 +16,7 @@ Section ectx_language_mixin.
   Context (empty_ectx : ectx).
   Context (comp_ectx : ectx → ectx → ectx).
   Context (fill : ectx → expr → expr).
-  Context (head_step : expr → state → option observation -> expr → state → list expr → Prop).
+  Context (head_step : expr → state → option observation → expr → state → list expr → Prop).
 
   Record EctxLanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
@@ -55,7 +55,7 @@ Structure ectxLanguage := EctxLanguage {
   empty_ectx : ectx;
   comp_ectx : ectx → ectx → ectx;
   fill : ectx → expr → expr;
-  head_step : expr → state → option observation -> expr → state → list expr → Prop;
+  head_step : expr → state → option observation → expr → state → list expr → Prop;
 
   ectx_language_mixin :
     EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
@@ -210,7 +210,7 @@ Section ectx_language.
   Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
     (∀ σ, P → head_reducible e1 σ) →
     (∀ σ1 κ e2' σ2 efs,
-      P → head_step e1 σ1 κ e2' σ2 efs → κ = None /\ σ1 = σ2 ∧ e2=e2' ∧ efs = []) →
+      P → head_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2=e2' ∧ efs = []) →
     PureExec P e1 e2.
   Proof.
     intros Hp1 Hp2. split.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 524741d60b6857a26d1d6bd8fafbe65e839ae86c..f1d2cdb2434ee19579335edb6e43152ce0d51dcc 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -16,43 +16,43 @@ Hint Resolve head_stuck_stuck.
 
 Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E,∅}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
-      state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,∅,E}▷=∗
+      state_interp σ2 κs' ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1) "Hσ".
+  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κs) "Hσ".
   iMod ("H" with "Hσ") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; eauto. iIntros (κ e2 σ2 efs) "%".
+  iSplit; first by destruct s; eauto. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
   iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E,∅}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ▷ ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
+      state_interp σ2 κs' ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (?) "?".
-  iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (κ e2 σ2 efs ?) "!> !>". by iApply "H".
+  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (??) "?".
+  iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (κ κs' e2 σ2 efs ?) "!> !>". by iApply "H".
 Qed.
 
 Lemma wp_lift_head_stuck E Φ e :
   to_val e = None →
   sub_redexes_are_values e →
-  (∀ σ, state_interp σ ={E,∅}=∗ ⌜head_stuck e σ⌝)
+  (∀ σ κs, state_interp σ κs ={E,∅}=∗ ⌜head_stuck e σ⌝)
   ⊢ WP e @ E ?{{ Φ }}.
 Proof.
   iIntros (??) "H". iApply wp_lift_stuck; first done.
-  iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
+  iIntros (σ κs) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
 Qed.
 
 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 → κ = None /\ σ1 = σ2) →
+  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
   (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
     WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
@@ -70,72 +70,73 @@ Lemma wp_lift_pure_head_stuck E Φ e :
   WP e @ E ?{{ Φ }}%I.
 Proof using Hinh.
   iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
-  iIntros (σ) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
+  iIntros (σ κs) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
   by auto.
 Qed.
 
 Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E1}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
-      state_interp σ2 ∗
+    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E1,E2}▷=∗
+      state_interp σ2 κs' ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
-  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; auto. iIntros (κ e2 σ2 efs) "%".
+  iIntros (σ1 κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct s; auto. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
   iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ▷ ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      state_interp σ2 ∗
+    ▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
+      state_interp σ2 κs' ∗
       from_option Φ 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 s; auto. iNext. iIntros (κ e2 σ2 efs) "%".
+  iIntros (σ1 κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct s; auto. iNext. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
   iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E1}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 ∗ from_option Φ False (to_val e2))
+    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E1,E2}▷=∗
+      ⌜efs = []⌝ ∗ state_interp σ2 κs' ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step_fupd; [done|].
-  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
-  iIntros (κ v2 σ2 efs) "%". iMod ("H" $! κ v2 σ2 efs with "[# //]") as "H".
+  iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 κs with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (κ κs' v2 σ2 efs [Hstep ->]).
+  iMod ("H" $! κ κs' v2 σ2 efs with "[# //]") as "H".
   iIntros "!> !>". iMod "H" as "(% & $ & $)"; subst; auto.
 Qed.
 
 Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ▷ ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 ∗ from_option Φ False (to_val e2))
+    ▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
+      ⌜efs = []⌝ ∗ state_interp σ2 κs' ∗ from_option Φ False (to_val e2))
   ⊢ 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.
-  iNext; iIntros (κ v2 σ2 efs) "%".
-  iMod ("H" $! κ v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
+  iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iNext; iIntros (κ κs' v2 σ2 efs Hstep).
+  iMod ("H" $! κ κs' v2 σ2 efs with "[# //]") as "(% & $ & $)". subst; auto.
 Qed.
 
 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' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
@@ -147,7 +148,7 @@ 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' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   (|={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.
@@ -158,7 +159,7 @@ 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',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = None /\  σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧  σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index fb932b863dd64eb353f8bc6e9cc775c17d3aa18a..727425b119a2a1ec304bc2203132f4a9e5d64828 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -31,7 +31,7 @@ Section ectxi_language_mixin.
   Context (of_val : val → expr).
   Context (to_val : expr → option val).
   Context (fill_item : ectx_item → expr → expr).
-  Context (head_step : expr → state → option observation -> expr → state → list expr → Prop).
+  Context (head_step : expr → state → option observation → expr → state → list expr → Prop).
 
   Record EctxiLanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
@@ -59,7 +59,7 @@ Structure ectxiLanguage := EctxiLanguage {
   of_val : val → expr;
   to_val : expr → option val;
   fill_item : ectx_item → expr → expr;
-  head_step : expr → state → option observation -> expr → state → list expr → Prop;
+  head_step : expr → state → option observation → expr → state → list expr → Prop;
 
   ectxi_language_mixin :
     EctxiLanguageMixin of_val to_val fill_item head_step
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index e08663e64df2fd1105aefc34f1e9e7d1394a64e1..0f575b4bff92cef2e9757a86c3f951547adc092b 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -5,7 +5,7 @@ Section language_mixin.
   Context {expr val state observation : Type}.
   Context (of_val : val → expr).
   Context (to_val : expr → option val).
-  (** We annotate the reduction relation with observations [k], which we will use in the definition
+  (** We annotate the reduction relation with observations [κ], which we will use in the definition
      of weakest preconditions to keep track of creating and resolving prophecy variables. *)
   Context (prim_step : expr → state → option observation → expr → state → list expr → Prop).
 
@@ -100,28 +100,24 @@ Section language.
        prim_step e1 σ1 κ e2 σ2 efs →
        step ρ1 κ ρ2.
 
-  Inductive nsteps : nat -> cfg Λ → list (observation Λ) → cfg Λ → Prop :=
+  (* TODO (MR) introduce notation ::? for cons_obs and suggest for inclusion to stdpp? *)
+  Definition cons_obs {A} (x : option A) (xs : list A) :=
+    option_list x ++ xs.
+
+  Inductive nsteps : nat → cfg Λ → list (observation Λ) → cfg Λ → Prop :=
   | nsteps_refl ρ :
       nsteps 0 ρ [] ρ
   | nsteps_l n ρ1 ρ2 ρ3 κ κs :
       step ρ1 κ ρ2 →
       nsteps n ρ2 κs ρ3 →
-      nsteps (S n) ρ1 (option_list κ ++ κs) ρ3.
-
- (* Inductive steps : cfg Λ → list (observation Λ) → cfg Λ → Prop :=
-  | steps_refl ρ :
-      steps ρ [] ρ
-  | steps_l ρ1 ρ2 ρ3 κ κs :
-      step ρ1 κ ρ2 →
-      steps ρ2 κs ρ3 →
-      steps ρ1 (option_list κ ++ κs) ρ3. *)
+      nsteps (S n) ρ1 (cons_obs κ κs) ρ3.
 
   Definition erased_step (ρ1 ρ2 : cfg Λ) := exists κ, step ρ1 κ ρ2.
 
   Hint Constructors step nsteps.
 
   Lemma erased_steps_nsteps ρ1 ρ2 :
-    rtc erased_step ρ1 ρ2 ->
+    rtc erased_step ρ1 ρ2 →
     ∃ n κs, nsteps n ρ1 κs ρ2.
   Proof.
     induction 1; firstorder; eauto.
@@ -173,7 +169,7 @@ Section language.
     pure_exec_safe σ :
       P → reducible e1 σ;
     pure_exec_puredet σ1 κ e2' σ2 efs :
-      P → prim_step e1 σ1 κ e2' σ2 efs → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = [];
+      P → prim_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = [];
   }.
 
   Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 58595f0bfcfcadb4e6fc9c0f732b16093d843b36..9cb243ed0dd5f44c36ed2957e104c172b2a91fed 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -13,42 +13,43 @@ Implicit Types Φ : val Λ → iProp Σ.
 
 Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E,∅}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
-      state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,∅,E}▷=∗
+      state_interp σ2 κs' ∗ 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 "(%&H)". iModIntro. iSplit. by destruct s. done.
+  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κs) "Hσ".
+  iMod ("H" with "Hσ") as "(%&H)". iModIntro. iSplit. by destruct s.
+  iIntros (????? [? ->]). iApply "H". eauto.
 Qed.
 
 Lemma wp_lift_stuck E Φ e :
   to_val e = None →
-  (∀ σ, state_interp σ ={E,∅}=∗ ⌜stuck e σ⌝)
+  (∀ σ κs, state_interp σ κs ={E,∅}=∗ ⌜stuck e σ⌝)
   ⊢ WP e @ E ?{{ Φ }}.
 Proof.
-  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1) "Hσ".
+  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κs) "Hσ".
   iMod ("H" with "Hσ") as %[? Hirr]. iModIntro. iSplit; first done.
-  iIntros (κ e2 σ2 efs) "% !> !>". by case: (Hirr κ e2 σ2 efs).
+  iIntros (κ ? e2 σ2 efs [? ->]). by case: (Hirr κ e2 σ2 efs).
 Qed.
 
 (** Derived lifting lemmas. *)
 Lemma wp_lift_step s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E,∅}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ▷ ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
+      state_interp σ2 κs' ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (?) "Hσ".
+  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (??) "Hσ".
   iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % !>". by iApply "H".
 Qed.
 
 Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-  (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+  (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
   (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
     WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
@@ -56,11 +57,11 @@ Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
   { specialize (Hsafe inhabitant). destruct s; last done.
       by eapply reducible_not_val. }
-  iIntros (σ1) "Hσ". iMod "H".
+  iIntros (σ1 κs) "Hσ". iMod "H".
   iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
   { iPureIntro. destruct s; done. }
-  iNext. iIntros (κ e2 σ2 efs ?).
-  destruct (Hstep κ σ1 e2 σ2 efs); auto; subst.
+  iNext. iIntros (κ κs' e2 σ2 efs [Hstep' ->]).
+  destruct (Hstep κ σ1 e2 σ2 efs); auto; subst; clear Hstep.
   iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
 Qed.
 
@@ -71,7 +72,7 @@ Proof.
   iIntros (Hstuck) "_". iApply wp_lift_stuck.
   - destruct(to_val e) as [v|] eqn:He; last done.
     rewrite -He. by case: (Hstuck inhabitant).
-  - iIntros (σ) "_". iMod (fupd_intro_mask' E ∅) as "_".
+  - iIntros (σ κs) "_". iMod (fupd_intro_mask' E ∅) as "_".
     by set_solver. by auto.
 Qed.
 
@@ -79,18 +80,18 @@ Qed.
    use the generic lemmas here. *)
 Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E1}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E1}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
-      state_interp σ2 ∗
+    ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E1,E2}▷=∗
+      state_interp σ2 κs' ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1) "Hσ1".
+  iIntros (?) "H". iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 κs) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iMod (fupd_intro_mask' E1 ∅) as "Hclose"; first set_solver.
-  iIntros "!>" (κ e2 σ2 efs ?). iMod "Hclose" as "_".
-  iMod ("H" $! κ e2 σ2 efs with "[#]") as "H"; [done|].
+  iIntros "!>" (κ  κs' e2 σ2 efs ?). iMod "Hclose" as "_".
+  iMod ("H" $! κ κs' e2 σ2 efs with "[#]") as "H"; [done|].
   iMod (fupd_intro_mask' E2 ∅) as "Hclose"; [set_solver|]. iIntros "!> !>".
   iMod "Hclose" as "_". iMod "H" as "($ & HΦ & $)".
   destruct (to_val e2) eqn:?; last by iExFalso.
@@ -99,21 +100,22 @@ Qed.
 
 Lemma wp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ▷ ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      state_interp σ2 ∗
+    ▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
+      state_interp σ2 κs' ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
-  iIntros (?) "?". iMod ("H" with "[$]") as "[$ H]". iIntros "!> * % !> !>".
+  iIntros (??) "?". iMod ("H" with "[$]") as "[$ H]".
+  iIntros "!> *". iIntros ([Hstep ->]) "!> !>".
   by iApply "H".
 Qed.
 
 Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
+  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
   (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index a87b07f1d8215a4d962b4d4b52b6a06611176007..ed98eccfa4c09e30eaac82698ed0a42198bf6fe2 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -5,65 +5,67 @@ From iris.algebra Require Import auth.
 From iris.proofmode Require Import tactics classes.
 Set Default Proof Using "Type".
 
-Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG {
+Class ownPG' (Λstate Λobservation: Type) (Σ : gFunctors) := OwnPG {
   ownP_invG : invG Σ;
-  ownP_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
+  ownP_inG :> inG Σ (authR (optionUR (exclR (prodC (leibnizC Λstate) (leibnizC (list Λobservation))))));
   ownP_name : gname;
 }.
-Notation ownPG Λ Σ := (ownPG' (state Λ) Σ).
+Notation ownPG Λ Σ := (ownPG' (state Λ) (observation Λ) Σ).
 
-Instance ownPG_irisG `{ownPG' Λstate Σ} : irisG' Λstate Σ := {
+Instance ownPG_irisG `{ownPG' Λstate Λobservation Σ} : irisG' Λstate Λobservation Σ := {
   iris_invG := ownP_invG;
-  state_interp σ := own ownP_name (● (Excl' (σ:leibnizC Λstate)))
+  state_interp σ κs := own ownP_name (● (Excl' ((σ:leibnizC Λstate), (κs:leibnizC (list Λobservation)))))
 }.
 Global Opaque iris_invG.
 
-Definition ownPΣ (Λstate : Type) : gFunctors :=
+Definition ownPΣ (Λstate Λobservation : Type) : gFunctors :=
   #[invΣ;
-    GFunctor (authUR (optionUR (exclR (leibnizC Λstate))))].
+    GFunctor (authUR (optionUR (exclR (prodC (leibnizC Λstate) (leibnizC (list Λobservation))))))].
 
-Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
+Class ownPPreG' (Λstate Λobservation : Type) (Σ : gFunctors) : Set := IrisPreG {
   ownPPre_invG :> invPreG Σ;
-  ownPPre_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))))
+  ownPPre_inG :> inG Σ (authR (optionUR (exclR (prodC (leibnizC Λstate) (leibnizC (list Λobservation))))))
 }.
-Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).
+Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) (observation Λ) Σ).
 
-Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ → ownPPreG' Λstate Σ.
+Instance subG_ownPΣ {Λstate Λobservation Σ} : subG (ownPΣ Λstate Λobservation) Σ → ownPPreG' Λstate Λobservation Σ.
 Proof. solve_inG. Qed.
 
 (** Ownership *)
-Definition ownP `{ownPG' Λstate Σ} (σ : Λstate) : iProp Σ :=
-  own ownP_name (◯ (Excl' σ)).
+Definition ownP `{ownPG' Λstate Λobservation Σ} (σ : Λstate) (κs : list Λobservation) : iProp Σ :=
+  own ownP_name (◯ (Excl' (σ, κs))).
 Typeclasses Opaque ownP.
 Instance: Params (@ownP) 3.
 
 
 (* Adequacy *)
 Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ :
-  (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+  (∀ `{ownPG Λ Σ} κs, ownP σ κs ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply (wp_adequacy Σ _).
-  iIntros (?). iMod (own_alloc (● (Excl' (σ : leibnizC _)) ⋅ ◯ (Excl' σ)))
+  iIntros (? κs). iMod (own_alloc (● (Excl' (σ : leibnizC _, κs : leibnizC _)) ⋅ ◯ (Excl' (σ, κs))))
     as (γσ) "[Hσ Hσf]"; first done.
-  iModIntro. iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))). iFrame "Hσ".
-  iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP.
+  iModIntro. iExists (λ σ κs, own γσ (● (Excl' (σ:leibnizC _, κs:leibnizC _)))). iFrame "Hσ".
+  iApply (Hwp (OwnPG _ _ _ _ _ γσ)). by rewrite /ownP.
 Qed.
 
 Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
-  (∀ `{ownPG Λ Σ},
-    ownP σ1 ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
+  (∀ `{ownPG Λ Σ} κs,
+    ownP σ1 κs ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗ |={⊤,∅}=> ∃ σ' κs', ownP σ' κs' ∧ ⌜φ σ'⌝) →
   rtc erased_step ([e], σ1) (t2, σ2) →
   φ σ2.
 Proof.
   intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
-  iIntros (?). iMod (own_alloc (● (Excl' (σ1 : leibnizC _)) ⋅ ◯ (Excl' σ1)))
+  iIntros (? κs κs').
+  iMod (own_alloc (● (Excl' ((σ1 : leibnizC _, κs ++ κs' : leibnizC _))) ⋅ ◯ (Excl' (σ1, κs ++ κs'))))
     as (γσ) "[Hσ Hσf]"; first done.
-  iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))). iFrame "Hσ".
-  iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]"; first by rewrite /ownP.
-  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite/ownP.
-  iDestruct (own_valid_2 with "Hσ Hσf")
-    as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2; auto.
+  iExists (λ σ κs', own γσ (● (Excl' (σ:leibnizC _, κs':leibnizC _)))). iFrame "Hσ".
+  iMod (Hwp (OwnPG _ _ _ _ _ γσ) with "[Hσf]") as "[$ H]"; first by rewrite /ownP.
+  iIntros "!> Hσ". iMod "H" as (σ2' κs'') "[Hσf %]". rewrite/ownP.
+  iDestruct (own_valid_2 with "Hσ Hσf") as %[Hp _]%auth_valid_discrete_2.
+  pose proof (Excl_included _ _ Hp) as Hp'. apply leibniz_equiv in Hp'. inversion Hp'; subst. auto.
+  (* TODO (MR) inline this proof in introduction pattern? *)
 Qed.
 
 
@@ -74,34 +76,36 @@ Section lifting.
   Implicit Types e : expr Λ.
   Implicit Types Φ : val Λ → iProp Σ.
 
-  Lemma ownP_eq σ1 σ2 : state_interp σ1 -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
+  Lemma ownP_eq σ1 σ2 κs1 κs2 : state_interp σ1 κs1 -∗ ownP σ2 κs2 -∗ ⌜σ1 = σ2 ∧ κs1 = κs2⌝.
   Proof.
     iIntros "Hσ1 Hσ2"; rewrite/ownP.
-    by iDestruct (own_valid_2 with "Hσ1 Hσ2")
-      as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "Hσ1 Hσ2")
+      as %[Hp _]%auth_valid_discrete_2.
+    pose proof (Excl_included _ _ Hp) as Hp'. apply leibniz_equiv in Hp'. inversion Hp'; subst. auto.
+  (* TODO (MR) inline this proof in introduction pattern? *)
   Qed.
-  Lemma ownP_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
+  Lemma ownP_twice σ1 σ2 κs1 κs2 : ownP σ1 κs1 ∗ ownP σ2 κs2 ⊢ False.
   Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
-  Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) Σ _ σ).
+  Global Instance ownP_timeless σ κs : Timeless (@ownP (state Λ) (observation Λ) Σ _ σ κs).
   Proof. rewrite /ownP; apply _. Qed.
 
   Lemma ownP_lift_step s E Φ e1 :
-    (|={E,∅}=> ∃ σ1, ⌜if s is NotStuck then reducible e1 σ1 else to_val e1 = None⌝ ∗ ▷ ownP σ1 ∗
-      ▷ ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ ownP σ2
+    (|={E,∅}=> ∃ σ1 κs, ⌜if s is NotStuck then reducible e1 σ1 else to_val e1 = None⌝ ∗ ▷ ownP σ1 κs ∗
+      ▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗ ownP σ2 κs'
             ={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
     - apply of_to_val in EQe1 as <-. iApply fupd_wp.
-      iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred.
+      iMod "H" as (σ1 κs) "[Hred _]"; iDestruct "Hred" as %Hred.
       destruct s; last done. apply reducible_not_val in Hred.
       move: Hred; by rewrite to_of_val.
-    - iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ".
-      iMod "H" as (σ1' ?) "[>Hσf H]". iDestruct (ownP_eq with "Hσ Hσf") as %->.
-      iModIntro; iSplit; [by destruct s|]; iNext; iIntros (κ e2 σ2 efs Hstep).
+    - iApply wp_lift_step; [done|]; iIntros (σ1 κs) "Hσ".
+      iMod "H" as (σ1' κs' ?) "[>Hσf H]". iDestruct (ownP_eq with "Hσ Hσf") as %[-> ->].
+      iModIntro; iSplit; [by destruct s|]; iNext; iIntros (κ κs'' e2 σ2 efs [Hstep ->]).
       rewrite /ownP; iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
-      { by apply auth_update, option_local_update,
-          (exclusive_local_update _ (Excl σ2)). }
+      { apply auth_update. apply option_local_update.
+          (exclusive_local_update _ (Excl (σ2, _))). }
       iFrame "Hσ". iApply ("H" with "[]"); eauto.
   Qed.
 
@@ -115,12 +119,12 @@ Section lifting.
       by rewrite to_of_val in Hnv.
     - iApply wp_lift_stuck; [done|]. iIntros (σ1) "Hσ".
       iMod "H" as (σ1') "(% & >Hσf)".
-      by iDestruct (ownP_eq with "Hσ Hσf") as %->.
+      by iDestruct (ownP_eq with "Hσ Hσf") as %→.
   Qed.
 
   Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
     (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+    (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
     (▷ ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
       WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
@@ -160,7 +164,7 @@ Section lifting.
   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".
+    edestruct Hdet as (→&Hval&→). done. by rewrite Hval; iApply "Hσ2".
   Qed.
 
   Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
@@ -175,17 +179,17 @@ Section lifting.
 
   Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
     (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
+    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
     ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤{{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
-    naive_solver. by iNext; iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
+    naive_solver. by iNext; iIntros (κ e' efs' σ (→&_&→&→)%Hpuredet).
   Qed.
 
   Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
     (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
@@ -226,7 +230,7 @@ Section ectx_lifting.
 
   Lemma ownP_lift_pure_head_step s E Φ e1 :
     (∀ σ1, head_reducible e1 σ1) →
-    (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+    (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
     (▷ ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
       WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
@@ -271,7 +275,7 @@ Section ectx_lifting.
 
   Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
     (∀ σ1, head_reducible e1 σ1) →
-    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
     ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
@@ -281,7 +285,7 @@ Section ectx_lifting.
 
   Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
     (∀ σ1, head_reducible e1 σ1) →
-    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
     iIntros (??) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 3757b771e64b0e0e56fd32a8aab37a8bb166a5c0..5493688cfed2a497d7d148e7c0c06a0372311eac 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -12,15 +12,15 @@ Implicit Types e : expr Λ.
 
 Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
     (t1 : list (expr Λ)) : iProp Σ :=
-  (∀ t2 σ1 σ2, ⌜erased_step (t1,σ1) (t2,σ2)⌝ -∗
-    state_interp σ1 ={⊤}=∗ state_interp σ2 ∗ twptp t2)%I.
+  (∀ t2 σ1 κ κs κs' σ2, ⌜step (t1,σ1) κ (t2,σ2) ∧ κs = cons_obs κ κs'⌝ -∗
+    state_interp σ1 κs ={⊤}=∗ state_interp σ2 κs' ∗ twptp t2)%I.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
   (<pers> (∀ t, twptp1 t -∗ twptp2 t) →
   ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t)%I.
 Proof.
   iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
-  iIntros (t2 σ1 σ2) "Hstep Hσ". iMod ("Hwp" with "[$] [$]") as "[$ ?]".
+  iIntros (t2 σ1 κ κs κs' σ2) "Hstep Hσ". iMod ("Hwp" with "[$] [$]") as "[$ ?]".
   by iApply "H".
 Qed.
 
@@ -50,8 +50,8 @@ Instance twptp_Permutation : Proper ((≡ₚ) ==> (⊢)) twptp.
 Proof.
   iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
   iApply twptp_ind; iIntros "!#" (t1) "IH"; iIntros (t1' Ht).
-  rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 σ2 Hstep) "Hσ".
-  destruct (erased_step_Permutation t1' t1 t2 σ1 σ2) as (t2'&?&?); try done.
+  rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs κs' σ2 [Hstep ->]) "Hσ".
+  destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); try done.
   iMod ("IH" $! t2' with "[% //] Hσ") as "[$ [IH _]]". by iApply "IH".
 Qed.
 
@@ -61,21 +61,21 @@ Proof.
   iApply twptp_ind; iIntros "!#" (t1) "IH1". iIntros (t2) "H2".
   iRevert (t1) "IH1"; iRevert (t2) "H2".
   iApply twptp_ind; iIntros "!#" (t2) "IH2". iIntros (t1) "IH1".
-  rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 σ2 Hstep) "Hσ1".
-  destruct Hstep as [κ [e1 σ1' e2 σ2' efs' t1' t2' ?? Hstep]]; simplify_eq/=.
+  rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 κ κs κs' σ2 [Hstep ->]) "Hσ1".
+  destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' ?? Hstep]; simplify_eq/=.
   apply app_eq_inv in H as [(t&?&?)|(t&?&?)]; subst.
   - destruct t as [|e1' ?]; simplify_eq/=.
-    + iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]". eexists.
-      { by eapply step_atomic with (t1:=[]). }
+    + iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]".
+      { split. by eapply step_atomic with (t1:=[]). reflexivity. }
       iModIntro. rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
       by setoid_rewrite (right_id_L [] (++)).
-    + iMod ("IH1" with "[%] Hσ1") as "[$ [IH1 _]]"; first by eexists; econstructor.
+    + iMod ("IH1" with "[%] Hσ1") as "[$ [IH1 _]]"; first by split; econstructor.
       iAssert (twptp t2) with "[IH2]" as "Ht2".
       { rewrite twptp_unfold. iApply (twptp_pre_mono with "[] IH2").
         iIntros "!# * [_ ?] //". }
       iModIntro. rewrite -assoc_L (comm _ t2) !cons_middle !assoc_L.
       by iApply "IH1".
-  - iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]"; first by eexists; econstructor.
+  - iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]"; first by split; econstructor.
     iModIntro. rewrite -assoc. by iApply "IH2".
 Qed.
 
@@ -84,8 +84,8 @@ Proof.
   iIntros "He". remember (⊤ : coPset) as E eqn:HE.
   iRevert (HE). iRevert (e E Φ) "He". iApply twp_ind.
   iIntros "!#" (e E Φ); iIntros "IH" (->).
-  rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' σ1' σ2' Hstep) "Hσ1".
-  destruct Hstep as [κ [e1 σ1 e2 σ2 efs [|? t1] t2 ?? Hstep]];
+  rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' σ1' κ κs κs' σ2' [Hstep ->]) "Hσ1".
+  destruct Hstep as [e1 σ1 e2 σ2 efs [|? t1] t2 ?? Hstep];
     simplify_eq/=; try discriminate_list.
   destruct (to_val e1) as [v|] eqn:He1.
   { apply val_stuck in Hstep; naive_solver. }
@@ -93,30 +93,35 @@ Proof.
   iMod ("IH" with "[% //]") as "[$ [[IH _] IHfork]]"; iModIntro.
   iApply (twptp_app [_] with "[IH]"); first by iApply "IH".
   clear. iInduction efs as [|e efs] "IH"; simpl.
-  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 σ2 [κ Hstep]).
+  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs κs' σ2 [Hstep ->]).
     destruct Hstep; simplify_eq/=; discriminate_list. }
   iDestruct "IHfork" as "[[IH' _] IHfork]".
   iApply (twptp_app [_] with "[IH']"); [by iApply "IH'"|by iApply "IH"].
 Qed.
 
-Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ)%I.
+Notation world σ κs := (wsat ∗ ownE ⊤ ∗ state_interp σ κs)%I.
 
-Lemma twptp_total σ t : world σ -∗ twptp t -∗ ▷ ⌜sn erased_step (t, σ)⌝.
+(* TODO (MR) prove twtp_total *)
+(*
+Lemma twptp_total σ κs t : world σ κs -∗ twptp t -∗ ▷ ⌜sn erased_step (t, σ)⌝.
 Proof.
-  iIntros "Hw Ht". iRevert (σ) "Hw". iRevert (t) "Ht".
-  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ) "(Hw&HE&Hσ)".
-  iApply (pure_mono _ _ (Acc_intro _)). iIntros ([t' σ'] Hstep).
+  iIntros "Hw Ht". iRevert (σ κs) "Hw". iRevert (t) "Ht".
+  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ κs) "(Hw&HE&Hσ)".
+  iApply (pure_mono _ _ (Acc_intro _)).
   rewrite /twptp_pre uPred_fupd_eq /uPred_fupd_def.
   iMod ("IH" with "[% //] Hσ [$Hw $HE]") as ">(Hw & HE & Hσ & [IH _])".
   iApply "IH". by iFrame.
 Qed.
+*)
 End adequacy.
 
-Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
+(* TODO (MR) prove twp_total *)
+(*
+Theorem twp_total Σ Λ `{invPreG Σ} s e σ κs Φ :
   (∀ `{Hinv : invG Σ},
-     (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ ∗ WP e @ s; ⊤ [{ Φ }])%I) →
+     (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) -> iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
+       stateI σ κs ∗ WP e @ s; ⊤ [{ Φ }])%I) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp.
@@ -124,6 +129,7 @@ Proof.
   iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp Hinv).
   rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
   iDestruct "Hwp" as (Istate) "[HI Hwp]".
-  iApply (@twptp_total _ _ (IrisG _ _ Hinv Istate) with "[$Hw $HE $HI]").
-  by iApply (@twp_twptp _ _ (IrisG _ _ Hinv Istate)).
+  iApply (@twptp_total _ _ (IrisG _ _ _ Hinv Istate) with "[$Hw $HE $HI]").
+  by iApply (@twp_twptp _ _ (IrisG _ _ _ Hinv Istate)).
 Qed.
+*)
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
index 7b8775d818965c8fa35b7e6684f3abb220d5a124..451a37657c24dfa945c207fff953486c4fa43b60 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -14,21 +14,21 @@ Hint Resolve head_prim_reducible head_reducible_prim_step.
 
 Lemma twp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E,∅}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
+      state_interp σ2 κs' ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
-  iIntros (?) "H". iApply (twp_lift_step _ E)=>//. iIntros (σ1) "Hσ".
+  iIntros (?) "H". iApply (twp_lift_step _ E)=>//. iIntros (σ1 κs) "Hσ".
   iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
-  iSplit; [destruct s; auto|]. iIntros (κ e2 σ2 efs) "%".
+  iSplit; [destruct s; auto|]. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
   iApply "H". by eauto.
 Qed.
 
 Lemma twp_lift_pure_head_step {s E Φ} e1 :
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
   (|={E}=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
     WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
@@ -39,36 +39,36 @@ Qed.
 
 Lemma twp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      state_interp σ2 ∗
+    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
+      state_interp σ2 κs'∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
-  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; auto. iIntros (κ e2 σ2 efs) "%". iApply "H"; eauto.
+  iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct s; auto. iIntros (κ κs' e2 σ2 efs [Hstep ->]). iApply "H"; eauto.
 Qed.
 
 Lemma twp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 ∗ from_option Φ False (to_val e2))
+    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
+      ⌜efs = []⌝ ∗ state_interp σ2 κs' ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_head_step; eauto.
-  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
-  iIntros (κ v2 σ2 efs) "%".
-  iMod ("H" $! κ v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
+  iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (κ κs' v2 σ2 efs [Hstep ->]).
+  iMod ("H" $! κ κs' v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
 Qed.
 
 Lemma twp_lift_pure_det_head_step {s E Φ} e1 e2 efs :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof using Hinh. eauto using twp_lift_pure_det_step. Qed.
@@ -77,7 +77,7 @@ Lemma twp_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' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
 Proof using Hinh.
   intros. rewrite -(twp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index ad5d3a86192f5b7b714d78fe98ae82277e814c83..628d92592331f64fdd544ab6e57bd62b638a295f 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -13,14 +13,15 @@ Implicit Types Φ : val Λ → iProp Σ.
 
 Lemma twp_lift_step s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E,∅}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+    ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
+      state_interp σ2 κs' ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
 
 (** Derived lifting lemmas. *)
+
 Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
@@ -30,9 +31,9 @@ Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
 Proof.
   iIntros (Hsafe Hstep) "H". iApply twp_lift_step.
   { eapply reducible_not_val, (Hsafe inhabitant). }
-  iIntros (σ1) "Hσ". iMod "H".
+  iIntros (σ1 κs) "Hσ". iMod "H".
   iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
-  iSplit; [by destruct s|]; iIntros (κ e2 σ2 efs ?).
+  iSplit; [by destruct s|]; iIntros (κ κs' e2 σ2 efs [Hstep' ->]).
   destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
   iMod "Hclose" as "_". iFrame "Hσ". iApply "H"; auto.
 Qed.
@@ -41,18 +42,18 @@ Qed.
    use the generic lemmas here. *)
 Lemma twp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E}=∗
+  (∀ σ1 κs, state_interp σ1 κs ={E}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      state_interp σ2 ∗
+    ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
+      state_interp σ2 κs' ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
-  iIntros (?) "H". iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1) "Hσ1".
+  iIntros (?) "H". iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1 κs) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-  iIntros "!>" (κ e2 σ2 efs) "%". iMod "Hclose" as "_".
-  iMod ("H" $! κ e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
+  iIntros "!>" (κ κs' e2 σ2 efs) "%". iMod "Hclose" as "_".
+  iMod ("H" $! κ κs' e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
   destruct (to_val e2) eqn:?; last by iExFalso.
   iApply twp_value; last done. by apply of_to_val.
 Qed.
@@ -76,4 +77,5 @@ Proof.
   iIntros ([??] Hφ) "HWP".
   iApply (twp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|auto].
 Qed.
+
 End lifting.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index fd96dd7373ef8fe637c5b806a1b2ba6262ace8b4..89e7a844ebe69f43735487ff641bb72e1fd384e7 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -9,10 +9,10 @@ Definition twp_pre `{irisG Λ Σ} (s : stuckness)
     coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
-  | None => ∀ σ1,
-     state_interp σ1 ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-     ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-       state_interp σ2 ∗ wp E e2 Φ ∗
+  | None => ∀ σ1 κs,
+     state_interp σ1 κs ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
+     ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
+       state_interp σ2 κs' ∗ wp E e2 Φ ∗
        [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
   end%I.
 
@@ -23,8 +23,8 @@ Lemma twp_pre_mono `{irisG Λ Σ} s
 Proof.
   iIntros "#H"; iIntros (E e1 Φ) "Hwp". rewrite /twp_pre.
   destruct (to_val e1) as [v|]; first done.
-  iIntros (σ1) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
-  iIntros (κ e2 σ2 efs) "Hstep".
+  iIntros (σ1 κs) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
+  iIntros (κ κs' e2 σ2 efs) "Hstep".
   iMod ("Hwp" with "Hstep") as "($ & Hwp & Hfork)"; iModIntro; iSplitL "Hwp".
   - by iApply "H".
   - iApply (@big_sepL_impl with "[$Hfork]"); iIntros "!#" (k e _) "Hwp".
@@ -44,7 +44,7 @@ Proof.
     iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" $! (E,e,Φ)).
   - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
-    rewrite /uncurry3 /twp_pre. do 18 (f_equiv || done). by apply Hwp, pair_ne.
+    rewrite /uncurry3 /twp_pre. do 22 (f_equiv || done). by apply Hwp, pair_ne.
 Qed.
 
 Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
@@ -105,9 +105,9 @@ Proof.
   iIntros "!#" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
   rewrite !twp_unfold /twp_pre. destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
+  iIntros (σ1 κs) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
   iMod ("IH" with "[$]") as "[% IH]".
-  iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
+  iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ κs' e2 σ2 efs Hstep).
   iMod ("IH" with "[//]") as "($ & IH & IHefs)"; auto.
   iMod "Hclose" as "_"; iModIntro. iSplitR "IHefs".
   - iDestruct "IH" as "[IH _]". iApply ("IH" with "[//] HΦ").
@@ -119,7 +119,7 @@ Lemma fupd_twp s E e Φ : (|={E}=> WP e @ s; E [{ Φ }]) -∗ WP e @ s; E [{ Φ
 Proof.
   rewrite twp_unfold /twp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
-  iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
+  iIntros (σ1 κs) "Hσ1". iMod "H". by iApply "H".
 Qed.
 Lemma twp_fupd s E e Φ : WP e @ s; E [{ v, |={E}=> Φ v }] -∗ WP e @ s; E [{ Φ }].
 Proof. iIntros "H". iApply (twp_strong_mono with "H"); auto. Qed.
@@ -130,8 +130,8 @@ Proof.
   iIntros "H". rewrite !twp_unfold /twp_pre /=.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
-  iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
-  iModIntro. iIntros (κ e2 σ2 efs Hstep).
+  iIntros (σ1 κs) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+  iModIntro. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
   iMod ("H" with "[//]") as "(Hphy & H & $)". destruct s.
   - rewrite !twp_unfold /twp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
@@ -152,12 +152,12 @@ Proof.
   rewrite /twp_pre. destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. iApply fupd_twp. by iApply "HΦ". }
   rewrite twp_unfold /twp_pre fill_not_val //.
-  iIntros (σ1) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
+  iIntros (σ1 κs) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
   { iPureIntro. unfold reducible in *.
     destruct s; naive_solver eauto using fill_step. }
-  iIntros (κ e2 σ2 efs Hstep).
+  iIntros (κ κs' e2 σ2 efs [Hstep ->]).
   destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
-  iMod ("IH" $! κ e2' σ2 efs with "[//]") as "($ & IH & IHfork)".
+  iMod ("IH" $! κ κs' e2' σ2 efs with "[//]") as "($ & IH & IHfork)".
   iModIntro; iSplitR "IHfork".
   - iDestruct "IH" as "[IH _]". by iApply "IH".
   - by setoid_rewrite and_elim_r.
@@ -173,10 +173,10 @@ Proof.
   { iModIntro. apply of_to_val in He as <-. rewrite !twp_unfold.
     iApply (twp_pre_mono with "[] IH"). by iIntros "!#" (E e Φ') "[_ ?]". }
   rewrite /twp_pre fill_not_val //.
-  iIntros (σ1) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
+  iIntros (σ1 κs) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
   { destruct s; eauto using reducible_fill. }
-  iIntros (κ e2 σ2 efs Hstep).
-  iMod ("IH" $! κ (K e2) σ2 efs with "[]") as "($ & IH & IHfork)"; eauto using fill_step.
+  iIntros (κ κs' e2 σ2 efs [Hstep ->]).
+  iMod ("IH" $! κ κs' (K e2) σ2 efs with "[]") as "($ & IH & IHfork)"; eauto using fill_step.
   iModIntro; iSplitR "IHfork".
   - iDestruct "IH" as "[IH _]". by iApply "IH".
   - by setoid_rewrite and_elim_r.
@@ -186,8 +186,8 @@ Lemma twp_wp s E e Φ : WP e @ s; E [{ Φ }] -∗ WP e @ s; E {{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ).
   rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//.
-  iIntros (σ1) "Hσ". iMod ("H" with "Hσ") as "[$ H]". iIntros "!>".
-  iIntros (κ e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as "($ & H & Hfork)".
+  iIntros (σ1 κs) "Hσ". iMod ("H" with "Hσ") as "[$ H]". iIntros "!>".
+  iIntros (κ κs' e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as "($ & H & Hfork)".
   iApply step_fupd_intro; [set_solver+|]. iNext.
   iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]").
   iIntros "!#" (k e' _) "H". by iApply "IH".
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 5bacf60b44c91528c17b9f1601f2fd75f1caf466..7370591dba8ec647a52825c4856d19c8da07fffb 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -5,11 +5,11 @@ From iris.proofmode Require Import base tactics classes.
 Set Default Proof Using "Type".
 Import uPred.
 
-Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
+Class irisG' (Λstate Λobservation : Type) (Σ : gFunctors) := IrisG {
   iris_invG :> invG Σ;
-  state_interp : Λstate -> (*list (option Λobservations) → *) iProp Σ;
+  state_interp : Λstate → list Λobservation → iProp Σ;
 }.
-Notation irisG Λ Σ := (irisG' (state Λ) Σ).
+Notation irisG Λ Σ := (irisG' (state Λ) (observation Λ) Σ).
 Global Opaque iris_invG.
 
 Definition wp_pre `{irisG Λ Σ} (s : stuckness)
@@ -17,11 +17,11 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
     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 s is NotStuck 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)
+  | None => ∀ σ1 κs,
+      state_interp σ1 κs ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
+      ∀ κ (κs' : list (observation Λ)) e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,∅,E}▷=∗
+      state_interp σ2 κs' ∗ wp E e2 Φ ∗
+      [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
   end%I.
 
 Local Instance wp_pre_contractive `{irisG Λ Σ} s : Contractive (wp_pre s).
@@ -57,7 +57,7 @@ Proof.
   (* FIXME: figure out a way to properly automate this proof *)
   (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
   is very slow here *)
-  do 20 (f_contractive || f_equiv). apply IH; first lia.
+  do 24 (f_contractive || f_equiv). apply IH; first lia.
   intros v. eapply dist_le; eauto with omega.
 Qed.
 Global Instance wp_proper s E e :
@@ -79,9 +79,9 @@ Proof.
   rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
+  iIntros (σ1 κs) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
   iMod ("H" with "[$]") as "[% H]".
-  iModIntro. iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
+  iModIntro. iSplit; [by destruct s1, s2|]. iIntros (κ κs' e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "H". iIntros "!> !>". iMod "H" as "($ & H & Hefs)".
   iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
   - iApply ("IH" with "[//] H HΦ").
@@ -93,7 +93,7 @@ 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".
+  iIntros (σ1 κs) "Hσ1". iMod "H". by iApply "H".
 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 s E with "H"); auto. Qed.
@@ -104,8 +104,8 @@ Proof.
   iIntros "H". rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
-  iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
-  iModIntro. iIntros (κ e2 σ2 efs Hstep).
+  iIntros (σ1 κs) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+  iModIntro. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
   iMod ("H" with "[//]") as "H". iIntros "!>!>". iMod "H" as "(Hphy & H & $)". destruct s.
   - rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
@@ -120,8 +120,8 @@ Lemma wp_step_fupd s E1 E2 e P Φ :
   (|={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]".
-  iIntros "!>" (κ e2 σ2 efs Hstep). iMod ("H" $! κ e2 σ2 efs with "[% //]") as "H".
+  iIntros (σ1 κs) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
+  iIntros "!>" (κ κs' e2 σ2 efs Hstep). iMod ("H" $! κ κs' e2 σ2 efs with "[% //]") as "H".
   iIntros "!>!>". iMod "H" as "($ & H & $)".
   iMod "HR". iModIntro. iApply (wp_strong_mono s s E2 with "H"); [done..|].
   iIntros (v) "H". by iApply "H".
@@ -134,12 +134,12 @@ Proof.
   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.
+  iIntros (σ1 κs) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
   { iPureIntro. destruct s; last done.
     unfold reducible in *. naive_solver eauto using fill_step. }
-  iIntros (κ e2 σ2 efs Hstep).
+  iIntros (κ κs' e2 σ2 efs [Hstep ->]).
   destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
-  iMod ("H" $! κ e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
+  iMod ("H" $! κ κs' e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
   iMod "H" as "($ & H & $)". by iApply "IH".
 Qed.
 
@@ -150,10 +150,10 @@ Proof.
   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.
+  iIntros (σ1 κs) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
   { destruct s; eauto using reducible_fill. }
-  iIntros (κ e2 σ2 efs Hstep).
-  iMod ("H" $! κ (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
+  iIntros (κ κs' e2 σ2 efs [Hstep ->]).
+  iMod ("H" $! κ κs' (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
   iIntros "!>!>". iMod "H" as "($ & H & $)". by iApply "IH".
 Qed.