diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4c5f34611e5fadb87ba50025cc99c96ec0c63ffb..6212f09f39d6119895d6284dc61b88630d0650d9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,11 @@ Changes in and extensions of the theory:
   experimental.
 * [#] The adequacy statement for weakest preconditions now also involves the
   final state.
+* [#] Add the notion of an "observation" to the language interface, so that
+  every reduction step can optionally be marked with an event, and an execution
+  trace has a matching list of events.  Change WP so that it is told the entire
+  future trace of observations from the beginning.  Use this in heap_lang to
+  implement prophecy variables.
 * [#] The LÃ¶b rule is now a derived rule; it follows from later-intro, later
   being contractive and the fact that we can take fixpoints of contractive
   functions.
diff --git a/_CoqProject b/_CoqProject
index 92fc6bd868e7653ba9dcbda026a271ce755ef9f5..e587aa9aaa5622b2a0ef7d38a31d2f61e8139e40 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -87,12 +87,14 @@ theories/heap_lang/notation.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v
 theories/heap_lang/total_adequacy.v
+theories/heap_lang/proph_map.v
 theories/heap_lang/lib/spawn.v
 theories/heap_lang/lib/par.v
 theories/heap_lang/lib/assert.v
 theories/heap_lang/lib/lock.v
 theories/heap_lang/lib/spin_lock.v
 theories/heap_lang/lib/ticket_lock.v
+theories/heap_lang/lib/coin_flip.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 1b7dfabb92db6399fb7d7ba33ffcecb1a42d5e7e..02301b8fb6d4d5a73dad9472e2f9234066a6b51d 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -1,15 +1,16 @@
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.algebra Require Import auth.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import proofmode notation proph_map.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Class heapPreG Î£ := HeapPreG {
   heap_preG_iris :> invPreG Î£;
-  heap_preG_heap :> gen_heapPreG loc val Î£
+  heap_preG_heap :> gen_heapPreG loc val Î£;
+  heap_preG_proph :> proph_mapPreG proph_id val Î£
 }.
 
-Definition heapÎ£ : gFunctors := #[invÎ£; gen_heapÎ£ loc val].
+Definition heapÎ£ : gFunctors := #[invÎ£; gen_heapÎ£ loc val; proph_mapÎ£ proph_id val].
 Instance subG_heapPreG {Î£} : subG heapÎ£ Î£ â†’ heapPreG Î£.
 Proof. solve_inG. Qed.
 
@@ -17,8 +18,10 @@ 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 (?) "".
-  iMod (gen_heap_init Ïƒ) as (?) "Hh".
-  iModIntro. iExists gen_heap_ctx. iFrame "Hh".
-  iApply (Hwp (HeapG _ _ _)).
+  intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
+  iMod (gen_heap_init Ïƒ.(heap)) as (?) "Hh".
+  iMod (proph_map_init Îºs Ïƒ.(used_proph_id)) as (?) "Hp".
+  iModIntro.
+  iExists (Î» Ïƒ Îºs, (gen_heap_ctx Ïƒ.(heap) âˆ— proph_map_ctx Îºs Ïƒ.(used_proph_id))%I). iFrame.
+  iApply (Hwp (HeapG _ _ _ _)).
 Qed.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 235fb97b4222bcb19fd8b7ab73f1eb33842ee52b..697a59f78ee1d5843057731dc7ade7088e25fca1 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -12,8 +12,14 @@ Set Default Proof Using "Type".
   [b] are evaluated.  With left-to-right evaluation, that triple is basically
   useless unless the user let-expands [b].
 
-*)
+- For prophecy variables, we annotate the reduction steps with an "observation"
+  and tweak adequacy such that WP knows all future observations.  There is
+  another possible choice: Use non-deterministic choice when creating a prophecy
+  variable ([NewProph]), and when resolving it ([ResolveProph]) make the
+  program diverge unless the variable matches.  That, however, requires an
+  erasure proof that this endless loop does not make specifications useless.
 
+*)
 
 Delimit Scope expr_scope with E.
 Delimit Scope val_scope with V.
@@ -23,9 +29,11 @@ Open Scope Z_scope.
 
 (** Expressions and vals. *)
 Definition loc := positive. (* Really, any countable type. *)
+Definition proph_id := positive.
 
 Inductive base_lit : Set :=
-  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
+  | LitInt (n : Z) | LitBool (b : bool) | LitUnit
+  | LitLoc (l : loc) | LitProphecy (p: proph_id).
 Inductive un_op : Set :=
   | NegOp | MinusUnOp.
 Inductive bin_op : Set :=
@@ -75,7 +83,10 @@ Inductive expr :=
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
   | CAS (e0 : expr) (e1 : expr) (e2 : expr)
-  | FAA (e1 : expr) (e2 : expr).
+  | FAA (e1 : expr) (e2 : expr)
+  (* Prophecy *)
+  | NewProph
+  | ResolveProph (e1 : expr) (e2 : expr).
 
 Bind Scope expr_scope with expr.
 
@@ -83,10 +94,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
   | Var x => bool_decide (x âˆˆ X)
   | Rec f x e => is_closed (f :b: x :b: X) e
-  | Lit _ => true
+  | Lit _ | NewProph => true
   | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
      is_closed X e
-  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | ResolveProph e1 e2 =>
      is_closed X e1 && is_closed X e2
   | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
      is_closed X e0 && is_closed X e1 && is_closed X e2
@@ -107,6 +118,8 @@ Inductive val :=
 
 Bind Scope val_scope with val.
 
+Definition observation : Set := proph_id * val.
+
 Fixpoint of_val (v : val) : expr :=
   match v with
   | RecV f x e => Rec f x e
@@ -160,7 +173,10 @@ Definition val_is_unboxed (v : val) : Prop :=
   end.
 
 (** The state: heaps of vals. *)
-Definition state := gmap loc val.
+Record state : Type := {
+  heap: gmap loc val;
+  used_proph_id: gset proph_id;
+}.
 
 (** Equality and other typeclass stuff *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -192,11 +208,13 @@ Defined.
 Instance base_lit_countable : Countable base_lit.
 Proof.
  refine (inj_countable' (Î» l, match l with
-  | LitInt n => inl (inl n) | LitBool b => inl (inr b)
-  | LitUnit => inr (inl ()) | LitLoc l => inr (inr l)
+  | LitInt n => (inl (inl n), None) | LitBool b => (inl (inr b), None)
+  | LitUnit => (inr (inl ()), None) | LitLoc l => (inr (inr l), None)
+  | LitProphecy p => (inr (inl ()), Some p)
   end) (Î» l, match l with
-  | inl (inl n) => LitInt n | inl (inr b) => LitBool b
-  | inr (inl ()) => LitUnit | inr (inr l) => LitLoc l
+  | (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
+  | (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
+  | (_, Some p) => LitProphecy p
   end) _); by intros [].
 Qed.
 Instance un_op_finite : Countable un_op.
@@ -225,12 +243,12 @@ Instance expr_countable : Countable expr.
 Proof.
  set (enc := fix go e :=
   match e with
-  | Var x => GenLeaf (inl (inl x))
-  | Rec f x e => GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
+  | Var x => GenLeaf (Some (inl (inl x)))
+  | Rec f x e => GenNode 0 [GenLeaf (Some ((inl (inr f)))); GenLeaf (Some (inl (inr x))); go e]
   | App e1 e2 => GenNode 1 [go e1; go e2]
-  | Lit l => GenLeaf (inr (inl l))
-  | UnOp op e => GenNode 2 [GenLeaf (inr (inr (inl op))); go e]
-  | BinOp op e1 e2 => GenNode 3 [GenLeaf (inr (inr (inr op))); go e1; go e2]
+  | Lit l => GenLeaf (Some (inr (inl l)))
+  | UnOp op e => GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); go e]
+  | BinOp op e1 e2 => GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); go e1; go e2]
   | If e0 e1 e2 => GenNode 4 [go e0; go e1; go e2]
   | Pair e1 e2 => GenNode 5 [go e1; go e2]
   | Fst e => GenNode 6 [go e]
@@ -244,15 +262,17 @@ Proof.
   | Store e1 e2 => GenNode 14 [go e1; go e2]
   | CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
   | FAA e1 e2 => GenNode 16 [go e1; go e2]
+  | NewProph => GenLeaf None
+  | ResolveProph e1 e2 => GenNode 17 [go e1; go e2]
   end).
  set (dec := fix go e :=
   match e with
-  | GenLeaf (inl (inl x)) => Var x
-  | GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
+  | GenLeaf (Some(inl (inl x))) => Var x
+  | GenNode 0 [GenLeaf (Some (inl (inr f))); GenLeaf (Some (inl (inr x))); e] => Rec f x (go e)
   | GenNode 1 [e1; e2] => App (go e1) (go e2)
-  | GenLeaf (inr (inl l)) => Lit l
-  | GenNode 2 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
-  | GenNode 3 [GenLeaf (inr (inr (inr op))); e1; e2] => BinOp op (go e1) (go e2)
+  | GenLeaf (Some (inr (inl l))) => Lit l
+  | GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); e] => UnOp op (go e)
+  | GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); e1; e2] => BinOp op (go e1) (go e2)
   | GenNode 4 [e0; e1; e2] => If (go e0) (go e1) (go e2)
   | GenNode 5 [e1; e2] => Pair (go e1) (go e2)
   | GenNode 6 [e] => Fst (go e)
@@ -266,6 +286,8 @@ Proof.
   | GenNode 14 [e1; e2] => Store (go e1) (go e2)
   | GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
   | GenNode 16 [e1; e2] => FAA (go e1) (go e2)
+  | GenLeaf None => NewProph
+  | GenNode 17 [e1; e2] => ResolveProph (go e1) (go e2)
   | _ => Lit LitUnit (* dummy *)
   end).
  refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
@@ -273,6 +295,8 @@ Qed.
 Instance val_countable : Countable val.
 Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.
 
+Instance state_inhabited : Inhabited state :=
+  populate {| heap := inhabitant; used_proph_id := inhabitant |}.
 Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
 Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
 
@@ -303,7 +327,9 @@ Inductive ectx_item :=
   | CasMCtx (e0 : expr) (v2 : val)
   | CasRCtx (e0 : expr) (e1 : expr)
   | FaaLCtx (v2 : val)
-  | FaaRCtx (e1 : expr).
+  | FaaRCtx (e1 : expr)
+  | ProphLCtx (v2 : val)
+  | ProphRCtx (e1 : expr).
 
 Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
@@ -329,6 +355,8 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CasRCtx e0 e1 => CAS e0 e1 e
   | FaaLCtx v2 => FAA e (of_val v2)
   | FaaRCtx e1 => FAA e1 e
+  | ProphLCtx v2 => ResolveProph e (of_val v2)
+  | ProphRCtx e1 => ResolveProph e1 e
   end.
 
 (** Substitution *)
@@ -354,6 +382,8 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   | Store e1 e2 => Store (subst x es e1) (subst x es e2)
   | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
   | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
+  | NewProph => NewProph
+  | ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
   end.
 
 Definition subst' (mx : binder) (es : expr) : expr â†’ expr :=
@@ -412,62 +442,90 @@ Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
   val_is_unboxed vl âˆ¨ val_is_unboxed v1.
 Arguments vals_cas_compare_safe !_ !_ /.
 
-Inductive head_step : expr â†’ state â†’ expr â†’ state â†’ list (expr) â†’ Prop :=
+Definition state_upd_heap (f: gmap loc val â†’ gmap loc val) (Ïƒ: state) : state :=
+  {| heap := f Ïƒ.(heap); used_proph_id := Ïƒ.(used_proph_id) |}.
+Arguments state_upd_heap _ !_ /.
+Definition state_upd_used_proph_id (f: gset proph_id â†’ gset proph_id) (Ïƒ: state) : state :=
+  {| heap := Ïƒ.(heap); used_proph_id := f Ïƒ.(used_proph_id) |}.
+Arguments state_upd_used_proph_id _ !_ /.
+
+Inductive head_step : expr â†’ state â†’ list observation â†’ expr â†’ state â†’ list (expr) â†’ Prop :=
   | BetaS f x e1 e2 v2 e' Ïƒ :
      to_val e2 = Some v2 â†’
      Closed (f :b: x :b: []) e1 â†’
      e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) â†’
-     head_step (App (Rec f x e1) e2) Ïƒ e' Ïƒ []
+     head_step (App (Rec f x e1) e2) Ïƒ [] e' Ïƒ []
   | UnOpS op e v v' Ïƒ :
      to_val e = Some v â†’
      un_op_eval op v = Some v' â†’
-     head_step (UnOp op e) Ïƒ (of_val v') Ïƒ []
+     head_step (UnOp op e) Ïƒ [] (of_val v') Ïƒ []
   | BinOpS op e1 e2 v1 v2 v' Ïƒ :
      to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
      bin_op_eval op v1 v2 = Some v' â†’
-     head_step (BinOp op e1 e2) Ïƒ (of_val v') Ïƒ []
+     head_step (BinOp op e1 e2) Ïƒ [] (of_val v') Ïƒ []
   | IfTrueS e1 e2 Ïƒ :
-     head_step (If (Lit $ LitBool true) e1 e2) Ïƒ e1 Ïƒ []
+     head_step (If (Lit $ LitBool true) e1 e2) Ïƒ [] e1 Ïƒ []
   | IfFalseS e1 e2 Ïƒ :
-     head_step (If (Lit $ LitBool false) e1 e2) Ïƒ e2 Ïƒ []
+     head_step (If (Lit $ LitBool false) e1 e2) Ïƒ [] e2 Ïƒ []
   | FstS e1 v1 e2 v2 Ïƒ :
      to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
-     head_step (Fst (Pair e1 e2)) Ïƒ e1 Ïƒ []
+     head_step (Fst (Pair e1 e2)) Ïƒ [] e1 Ïƒ []
   | SndS e1 v1 e2 v2 Ïƒ :
      to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
-     head_step (Snd (Pair e1 e2)) Ïƒ e2 Ïƒ []
+     head_step (Snd (Pair e1 e2)) Ïƒ [] e2 Ïƒ []
   | CaseLS e0 v0 e1 e2 Ïƒ :
      to_val e0 = Some v0 â†’
-     head_step (Case (InjL e0) e1 e2) Ïƒ (App e1 e0) Ïƒ []
+     head_step (Case (InjL e0) e1 e2) Ïƒ [] (App e1 e0) Ïƒ []
   | CaseRS e0 v0 e1 e2 Ïƒ :
      to_val e0 = Some v0 â†’
-     head_step (Case (InjR e0) e1 e2) Ïƒ (App e2 e0) Ïƒ []
+     head_step (Case (InjR e0) e1 e2) Ïƒ [] (App e2 e0) Ïƒ []
   | ForkS e Ïƒ:
-     head_step (Fork e) Ïƒ (Lit LitUnit) Ïƒ [e]
+     head_step (Fork e) Ïƒ [] (Lit LitUnit) Ïƒ [e]
   | AllocS e v Ïƒ l :
-     to_val e = Some v â†’ Ïƒ !! l = None â†’
-     head_step (Alloc e) Ïƒ (Lit $ LitLoc l) (<[l:=v]>Ïƒ) []
+     to_val e = Some v â†’ Ïƒ.(heap) !! l = None â†’
+     head_step (Alloc e) Ïƒ
+               []
+               (Lit $ LitLoc l) (state_upd_heap <[l:=v]> Ïƒ)
+               []
   | LoadS l v Ïƒ :
-     Ïƒ !! l = Some v â†’
-     head_step (Load (Lit $ LitLoc l)) Ïƒ (of_val v) Ïƒ []
+     Ïƒ.(heap) !! l = Some v â†’
+     head_step (Load (Lit $ LitLoc l)) Ïƒ [] (of_val v) Ïƒ []
   | StoreS l e v Ïƒ :
-     to_val e = Some v â†’ is_Some (Ïƒ !! l) â†’
-     head_step (Store (Lit $ LitLoc l) e) Ïƒ (Lit LitUnit) (<[l:=v]>Ïƒ) []
+     to_val e = Some v â†’ is_Some (Ïƒ.(heap) !! l) â†’
+     head_step (Store (Lit $ LitLoc l) e) Ïƒ
+               []
+               (Lit LitUnit) (state_upd_heap <[l:=v]> Ïƒ)
+               []
   | CasFailS l e1 v1 e2 v2 vl Ïƒ :
      to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
-     Ïƒ !! l = Some vl â†’ vl â‰  v1 â†’
+     Ïƒ.(heap) !! l = Some vl â†’ vl â‰  v1 â†’
      vals_cas_compare_safe vl v1 â†’
-     head_step (CAS (Lit $ LitLoc l) e1 e2) Ïƒ (Lit $ LitBool false) Ïƒ []
+     head_step (CAS (Lit $ LitLoc l) e1 e2) Ïƒ [] (Lit $ LitBool false) Ïƒ []
   | CasSucS l e1 v1 e2 v2 Ïƒ :
      to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
-     Ïƒ !! l = Some v1 â†’
+     Ïƒ.(heap) !! l = Some v1 â†’
      vals_cas_compare_safe v1 v1 â†’
-     head_step (CAS (Lit $ LitLoc l) e1 e2) Ïƒ (Lit $ LitBool true) (<[l:=v2]>Ïƒ) []
+     head_step (CAS (Lit $ LitLoc l) e1 e2) Ïƒ
+               []
+               (Lit $ LitBool true) (state_upd_heap <[l:=v2]> Ïƒ)
+               []
   | FaaS l i1 e2 i2 Ïƒ :
      to_val e2 = Some (LitV (LitInt i2)) â†’
-     Ïƒ !! l = Some (LitV (LitInt i1)) â†’
-     head_step (FAA (Lit $ LitLoc l) e2) Ïƒ (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>Ïƒ) [].
-
+     Ïƒ.(heap) !! l = Some (LitV (LitInt i1)) â†’
+     head_step (FAA (Lit $ LitLoc l) e2) Ïƒ
+               []
+               (Lit $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]> Ïƒ)
+               []
+  | NewProphS Ïƒ p :
+     p âˆ‰ Ïƒ.(used_proph_id) â†’
+     head_step NewProph Ïƒ
+               []
+               (Lit $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} âˆª) Ïƒ)
+               []
+  | ResolveProphS e1 p e2 v Ïƒ :
+     to_val e1 = Some (LitV $ LitProphecy p) â†’
+     to_val e2 = Some v â†’
+     head_step (ResolveProph e1 e2) Ïƒ [(p, v)] (Lit LitUnit) Ïƒ [].
 
 (** Basic properties about the language *)
 Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
@@ -477,11 +535,11 @@ Lemma fill_item_val Ki e :
   is_Some (to_val (fill_item Ki e)) â†’ is_Some (to_val e).
 Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 
-Lemma val_head_stuck e1 Ïƒ1 e2 Ïƒ2 efs : head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ to_val e1 = None.
+Lemma val_head_stuck e1 Ïƒ1 Îº e2 Ïƒ2 efs : head_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
-Lemma head_ctx_step_val Ki e Ïƒ1 e2 Ïƒ2 efs :
-  head_step (fill_item Ki e) Ïƒ1 e2 Ïƒ2 efs â†’ is_Some (to_val e).
+Lemma head_ctx_step_val Ki e Ïƒ1 Îº e2 Ïƒ2 efs :
+  head_step (fill_item Ki e) Ïƒ1 Îº e2 Ïƒ2 efs â†’ is_Some (to_val e).
 Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
 
 Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
@@ -495,10 +553,16 @@ Proof.
 Qed.
 
 Lemma alloc_fresh e v Ïƒ :
-  let l := fresh (dom (gset loc) Ïƒ) in
-  to_val e = Some v â†’ head_step (Alloc e) Ïƒ (Lit (LitLoc l)) (<[l:=v]>Ïƒ) [].
+  let l := fresh (dom (gset loc) Ïƒ.(heap)) in
+  to_val e = Some v â†’
+  head_step (Alloc e) Ïƒ [] (Lit (LitLoc l)) (state_upd_heap <[l:=v]> Ïƒ) [].
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
 
+Lemma new_proph_id_fresh Ïƒ :
+  let p := fresh Ïƒ.(used_proph_id) in
+  head_step NewProph Ïƒ [] (Lit $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} âˆª) Ïƒ) [].
+Proof. constructor. apply is_fresh. Qed.
+
 (* Misc *)
 Lemma to_val_rec f x e `{!Closed (f :b: x :b: []) e} :
   to_val (Rec f x e) = Some (RecV f x e).
diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
new file mode 100644
index 0000000000000000000000000000000000000000..65d05ea26037cb53c72016e9bb81ed0b90e55315
--- /dev/null
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -0,0 +1,92 @@
+From iris.base_logic.lib Require Export invariants.
+From iris.program_logic Require Export atomic.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation par.
+Set Default Proof Using "Type".
+
+(** Nondeterminism and Speculation:
+    Implementing "Late choice versus early choice" example from
+    Logical Relations for Fine-Grained Concurrency by Turon et al. (POPL'13) *)
+
+Definition rand: val :=
+  Î»: "_",
+    let: "y" := ref #false in
+    Fork ("y" <- #true) ;;
+    !"y".
+
+Definition earlyChoice: val :=
+  Î»: "x",
+    let: "r" := rand #() in
+    "x" <- #0 ;;
+    "r".
+
+Definition lateChoice: val :=
+  Î»: "x",
+    let: "p" := NewProph in
+    "x" <- #0 ;;
+    let: "r" := rand #() in
+    resolve_proph: "p" to: "r" ;;
+    "r".
+
+Section coinflip.
+  Context `{!heapG Î£}.
+
+  Local Definition N := nroot .@ "coin".
+
+  Lemma rand_spec :
+    {{{ True }}} rand #() {{{ (b : bool), RET #b; True }}}.
+  Proof.
+    iIntros (Î¦) "_ HP".
+    wp_lam. wp_alloc l as "Hl". wp_lam.
+    iMod (inv_alloc N _ (âˆƒ (b: bool), l â†¦ #b)%I with "[Hl]") as "#Hinv"; first by eauto.
+    wp_apply wp_fork.
+    - iInv N as (b) ">Hl". wp_store. iModIntro. iSplitL; eauto.
+    - wp_lam. iInv N as (b) ">Hl". wp_load. iModIntro. iSplitL "Hl"; first by eauto.
+      iApply "HP". done.
+  Qed.
+
+  Lemma earlyChoice_spec (x: loc) :
+    <<< x â†¦ - >>>
+        earlyChoice #x
+        @ âŠ¤
+    <<< âˆƒ (b: bool), x â†¦ #0, RET #b >>>.
+  Proof.
+    iApply wp_atomic_intro. iIntros (Î¦) "AU". wp_lam.
+    wp_apply rand_spec; first done.
+    iIntros (b) "_". wp_let.
+    wp_bind (_ <- _)%E.
+    iMod "AU" as "[Hl [_ Hclose]]".
+    iDestruct "Hl" as (v) "Hl".
+    wp_store.
+    iMod ("Hclose" with "[Hl]") as "HÎ¦"; first by eauto.
+    iModIntro. wp_seq. done.
+  Qed.
+
+  Definition val_to_bool (v : option val) : bool :=
+    match v with
+    | Some (LitV (LitBool b)) => b
+    | _                       => true
+    end.
+
+  Lemma lateChoice_spec (x: loc) :
+    <<< x â†¦ - >>>
+        lateChoice #x
+        @ âŠ¤
+    <<< âˆƒ (b: bool), x â†¦ #0, RET #b >>>.
+  Proof.
+    iApply wp_atomic_intro. iIntros (Î¦) "AU". wp_lam.
+    wp_apply wp_new_proph; first done.
+    iIntros (v p) "Hp".
+    wp_let.
+    wp_bind (_ <- _)%E.
+    iMod "AU" as "[Hl [_ Hclose]]".
+    iDestruct "Hl" as (v') "Hl".
+    wp_store.
+    iMod ("Hclose" $! (val_to_bool v) with "[Hl]") as "HÎ¦"; first by eauto.
+    iModIntro. wp_seq. wp_apply rand_spec; try done.
+    iIntros (b') "_". wp_let.
+    wp_apply (wp_resolve_proph with "Hp").
+    iIntros (->). wp_seq. done.
+  Qed.
+
+End coinflip.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 8cfb6341945740e72c8afab9eda7416b4bff7ee8..b7805d0789605ab20537acb69aaf2055b6974943 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,7 +1,8 @@
+From iris.algebra Require Import auth gmap.
 From iris.base_logic Require Export gen_heap.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
-From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Export lang proph_map.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
 From stdpp Require Import fin_maps.
@@ -9,12 +10,14 @@ Set Default Proof Using "Type".
 
 Class heapG Î£ := HeapG {
   heapG_invG : invG Î£;
-  heapG_gen_heapG :> gen_heapG loc val Î£
+  heapG_gen_heapG :> gen_heapG loc val Î£;
+  heapG_proph_mapG :> proph_mapG proph_id val Î£
 }.
 
 Instance heapG_irisG `{heapG Î£} : irisG heap_lang Î£ := {
   iris_invG := heapG_invG;
-  state_interp := gen_heap_ctx
+  state_interp Ïƒ Îºs :=
+    (gen_heap_ctx Ïƒ.(heap) âˆ— proph_map_ctx Îºs Ïƒ.(used_proph_id))%I
 }.
 
 (** Override the notations so that scopes and coercions work out *)
@@ -35,17 +38,22 @@ Ltac inv_head_step :=
   repeat match goal with
   | _ => progress simplify_map_eq/= (* simplify memory stuff *)
   | H : to_val _ = Some _ |- _ => apply of_to_val in H
-  | H : head_step ?e _ _ _ _ |- _ =>
+  | H : head_step ?e _ _ _ _ _ |- _ =>
      try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
      and can thus better be avoided. *)
      inversion H; subst; clear H
   end.
 
 Local Hint Extern 0 (atomic _ _) => solve_atomic.
-Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
+Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
+Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl.
 
-Local Hint Constructors head_step.
-Local Hint Resolve alloc_fresh.
+(* [simpl apply] is too stupid, so we need extern hints here. *)
+Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor.
+Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS.
+Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS.
+Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh.
+Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh.
 Local Hint Resolve to_of_val.
 
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
@@ -110,14 +118,15 @@ Lemma wp_fork s E e Î¦ :
   â–· WP e @ s; âŠ¤ {{ _, True }} -âˆ— â–· Î¦ (LitV LitUnit) -âˆ— WP Fork e @ s; E {{ Î¦ }}.
 Proof.
   iIntros "He HÎ¦".
-  iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
+  iApply wp_lift_pure_det_head_step; [by eauto|intros; inv_head_step; by 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.
   iIntros "He HÎ¦".
-  iApply twp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
+  iApply twp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
   iIntros "!> /= {$He}". by iApply twp_value.
 Qed.
 
@@ -127,7 +136,7 @@ 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 auto.
+  iIntros (Ïƒ1 Îº Îºs) "[HÏƒ HÎºs] !>"; iSplit; first by eauto.
   iNext; iIntros (v2 Ïƒ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "HÏƒ") as "[HÏƒ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HÎ¦".
@@ -137,29 +146,27 @@ 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 auto.
-  iIntros (v2 Ïƒ2 efs Hstep); inv_head_step.
+  iIntros (Ïƒ1 Îºs) "[HÏƒ HÎºs] !>"; iSplit; first by eauto.
+  iIntros (Îº v2 Ïƒ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "HÏƒ") as "[HÏƒ Hl]"; first done.
-  iModIntro; iSplit=> //. iFrame. by iApply "HÎ¦".
+  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HÎ¦".
 Qed.
 
 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 %?.
-  iSplit; first by eauto.
-  iNext; iIntros (v2 Ïƒ2 efs Hstep); inv_head_step.
+  iIntros (Ïƒ1 Îº Îºs) "[HÏƒ HÎºs] !>". iDestruct (@gen_heap_valid with "HÏƒ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (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 %?.
-  iSplit; first by eauto.
-  iIntros (v2 Ïƒ2 efs Hstep); inv_head_step.
-  iModIntro; iSplit=> //. iFrame. by iApply "HÎ¦".
+  iIntros (Ïƒ1 Îºs) "[HÏƒ HÎºs] !>". iDestruct (@gen_heap_valid with "HÏƒ Hl") as %?.
+  iSplit; first by eauto. iIntros (Îº v2 Ïƒ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HÎ¦".
 Qed.
 
 Lemma wp_store s E l v' e v :
@@ -168,10 +175,10 @@ 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 %?.
+  iIntros (Ïƒ1 Îº Îºs) "[HÏƒ HÎºs] !>". iDestruct (@gen_heap_valid with "HÏƒ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2 Ïƒ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "HÏƒ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HÎ¦".
+  iModIntro. iSplit=>//. iFrame. by iApply "HÎ¦".
 Qed.
 Lemma twp_store s E l v' e v :
   IntoVal e v â†’
@@ -179,10 +186,10 @@ 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. iIntros (v2 Ïƒ2 efs Hstep); inv_head_step.
+  iIntros (Ïƒ1 Îºs) "[HÏƒ HÎºs] !>". iDestruct (@gen_heap_valid with "HÏƒ Hl") as %?.
+  iSplit; first by eauto. iIntros (Îº v2 Ïƒ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "HÏƒ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HÎ¦".
+  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HÎ¦".
 Qed.
 
 Lemma wp_cas_fail s E l q v' e1 v1 e2 :
@@ -192,7 +199,7 @@ 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 %?.
+  iIntros (Ïƒ1 Îº Îºs) "[HÏƒ HÎºs] !>". iDestruct (@gen_heap_valid with "HÏƒ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' Ïƒ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HÎ¦".
 Qed.
@@ -203,9 +210,9 @@ 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.
-  iModIntro; iSplit=> //. iFrame. by iApply "HÎ¦".
+  iIntros (Ïƒ1 Îºs) "[HÏƒ HÎºs] !>". iDestruct (@gen_heap_valid with "HÏƒ Hl") as %?.
+  iSplit; first by eauto. iIntros (Îº v2' Ïƒ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HÎ¦".
 Qed.
 
 Lemma wp_cas_suc s E l e1 v1 e2 v2 :
@@ -215,10 +222,10 @@ 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 %?.
+  iIntros (Ïƒ1 Îº Îºs) "[HÏƒ HÎºs] !>". iDestruct (@gen_heap_valid with "HÏƒ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' Ïƒ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "HÏƒ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HÎ¦".
+  iModIntro. iSplit=>//. iFrame. by iApply "HÎ¦".
 Qed.
 Lemma twp_cas_suc s E l e1 v1 e2 v2 :
   IntoVal e1 v1 â†’ IntoVal e2 v2 â†’ vals_cas_compare_safe v1 v1 â†’
@@ -227,10 +234,10 @@ 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Ïƒ HÎºs] !>". iDestruct (@gen_heap_valid with "HÏƒ Hl") as %?.
+  iSplit; first by eauto. iIntros (Îº v2' Ïƒ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "HÏƒ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HÎ¦".
+  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HÎ¦".
 Qed.
 
 Lemma wp_faa s E l i1 e2 i2 :
@@ -240,10 +247,10 @@ 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 %?.
+  iIntros (Ïƒ1 Îº Îºs) "[HÏƒ HÎºs] !>". iDestruct (@gen_heap_valid with "HÏƒ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' Ïƒ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "HÏƒ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HÎ¦".
+  iModIntro. iSplit=>//. iFrame. by iApply "HÎ¦".
 Qed.
 Lemma twp_faa s E l i1 e2 i2 :
   IntoVal e2 (LitV (LitInt i2)) â†’
@@ -252,9 +259,46 @@ 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Ïƒ HÎºs] !>". iDestruct (@gen_heap_valid with "HÏƒ Hl") as %?.
+  iSplit; first by eauto. iIntros (Îº e2 Ïƒ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "HÏƒ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HÎ¦".
+  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HÎ¦".
 Qed.
+
+(** Lifting lemmas for creating and resolving prophecy variables *)
+Lemma wp_new_proph :
+  {{{ True }}} NewProph {{{ v (p : proph_id), RET (LitV (LitProphecy p)); proph p v }}}.
+Proof.
+  iIntros (Î¦) "_ HÎ¦". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (Ïƒ1 Îº Îºs) "[HÏƒ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
+  iSplit; first by eauto.
+  iNext; iIntros (v2 Ïƒ2 efs Hstep). inv_head_step.
+  iMod (@proph_map_alloc with "HR") as "[HR Hp]".
+  { intro Hin. apply (iffLR (elem_of_subseteq _ _) Hdom) in Hin. done. }
+  iModIntro; iSplit=> //. iFrame. iSplitL "HR".
+  - iExists _. iSplit; last done.
+    iPureIntro. split.
+    + apply first_resolve_insert; auto.
+    + rewrite dom_insert_L. by apply union_mono_l.
+  - iApply "HÎ¦". done.
+Qed.
+
+Lemma wp_resolve_proph e1 e2 p v w:
+  IntoVal e1 (LitV (LitProphecy p)) â†’
+  IntoVal e2 w â†’
+  {{{ proph p v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); âŒœv = Some wâŒ }}}.
+Proof.
+  iIntros (<- <- Î¦) "Hp HÎ¦". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (Ïƒ1 Îº Îºs) "[HÏƒ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
+  iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
+  iSplit; first by eauto.
+  iNext; iIntros (v2 Ïƒ2 efs Hstep); inv_head_step. iApply fupd_frame_l.
+  iSplit=> //. iFrame.
+  iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
+  iSplitR "HÎ¦".
+  - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
+    rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
+  - iApply "HÎ¦". iPureIntro. by eapply first_resolve_eq.
+Qed.
+
 End lifting.
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 80e876e8caee6bd8935ef8a35487bae2f1b76c5c..01cec440238754c6f07e95142acf1e5485ec18a3 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -8,6 +8,7 @@ Delimit Scope val_scope with V.
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
+Coercion LitProphecy : proph_id >-> base_lit.
 
 Coercion App : expr >-> Funclass.
 Coercion of_val : val >-> expr.
@@ -155,3 +156,5 @@ Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
 Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
+
+Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.
diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
new file mode 100644
index 0000000000000000000000000000000000000000..5f19f0c774c5d75678af3b1d1c42f8ae4ba4d048
--- /dev/null
+++ b/theories/heap_lang/proph_map.v
@@ -0,0 +1,177 @@
+From iris.algebra Require Import auth gmap.
+From iris.base_logic.lib Require Export own.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+Import uPred.
+
+Definition proph_map (P V : Type) `{Countable P} := gmap P (option V).
+Definition proph_val_list (P V : Type) := list (P * V).
+
+Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
+  gmapUR P $ exclR $ optionC $ leibnizC V.
+
+Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
+  fmap (Î» v, Excl (v : option (leibnizC V))) pvs.
+
+(** The CMRA we need. *)
+Class proph_mapG (P V : Type) (Î£ : gFunctors) `{Countable P} := ProphMapG {
+  proph_map_inG :> inG Î£ (authR (proph_mapUR P V));
+  proph_map_name : gname
+}.
+Arguments proph_map_name {_ _ _ _ _} _ : assert.
+
+Class proph_mapPreG (P V : Type) (Î£ : gFunctors) `{Countable P} :=
+  { proph_map_preG_inG :> inG Î£ (authR (proph_mapUR P V)) }.
+
+Definition proph_mapÎ£ (P V : Type) `{Countable P} : gFunctors :=
+  #[GFunctor (authR (proph_mapUR P V))].
+
+Instance subG_proph_mapPreG {Î£ P V} `{Countable P} :
+  subG (proph_mapÎ£ P V) Î£ â†’ proph_mapPreG P V Î£.
+Proof. solve_inG. Qed.
+
+Section definitions.
+  Context `{pG : proph_mapG P V Î£}.
+
+  (** The first resolve for [p] in [pvs] *)
+  Definition first_resolve (pvs : proph_val_list P V) (p : P) :=
+    (map_of_list pvs : gmap P V) !! p.
+
+  Definition first_resolve_in_list (R : proph_map P V) pvs :=
+    âˆ€ p v, p âˆˆ dom (gset _) R â†’
+           first_resolve pvs p = Some v â†’
+           R !! p = Some (Some v).
+
+  Definition proph_map_auth (R : proph_map P V) : iProp Î£ :=
+    own (proph_map_name pG) (â— (to_proph_map R)).
+
+  Definition proph_map_ctx (pvs : proph_val_list P V) (ps : gset P) : iProp Î£ :=
+    (âˆƒ R, âŒœfirst_resolve_in_list R pvs âˆ§
+          dom (gset _) R âŠ† psâŒ âˆ—
+          proph_map_auth R)%I.
+
+  Definition proph_def (p : P) (v: option V) : iProp Î£ :=
+    own (proph_map_name pG) (â—¯ {[ p := Excl (v : option $ leibnizC V) ]}).
+  Definition proph_aux : seal (@proph_def). by eexists. Qed.
+  Definition proph := proph_aux.(unseal).
+  Definition proph_eq :
+    @proph = @proph_def := proph_aux.(seal_eq).
+
+End definitions.
+
+Section first_resolve.
+  Context {P V : Type} `{Countable P}.
+  Implicit Type pvs : proph_val_list P V.
+  Implicit Type p : P.
+  Implicit Type v : V.
+  Implicit Type R : proph_map P V.
+
+  Lemma first_resolve_insert pvs p R :
+    first_resolve_in_list R pvs â†’
+    p âˆ‰ dom (gset _) R â†’
+    first_resolve_in_list (<[p := first_resolve pvs p]> R) pvs.
+  Proof.
+    intros Hf Hnotin p' v' Hp'. rewrite (dom_insert_L R p) in Hp'.
+    erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin] => [->].
+    - by rewrite lookup_insert.
+    - rewrite lookup_insert_ne; first auto. by intros ->.
+  Qed.
+
+  Lemma first_resolve_delete pvs p v R :
+    first_resolve_in_list R ((p, v) :: pvs) â†’
+    first_resolve_in_list (delete p R) pvs.
+  Proof.
+    intros Hfr p' v' Hpin Heq. rewrite dom_delete_L in Hpin. rewrite /first_resolve in Heq.
+    apply elem_of_difference in Hpin as [Hpin Hne%not_elem_of_singleton].
+    erewrite <- lookup_insert_ne in Heq; last done. rewrite lookup_delete_ne; eauto.
+  Qed.
+
+  Lemma first_resolve_eq R p v w pvs :
+    first_resolve_in_list R ((p, v) :: pvs) â†’
+    R !! p = Some w â†’
+    w = Some v.
+  Proof.
+    intros Hfr Hlookup. specialize (Hfr p v (elem_of_dom_2 _ _ _ Hlookup)).
+    rewrite /first_resolve lookup_insert in Hfr. rewrite Hfr in Hlookup; last done.
+    inversion Hlookup. done.
+  Qed.
+
+End first_resolve.
+
+Section to_proph_map.
+  Context (P V : Type) `{Countable P}.
+  Implicit Types p : P.
+  Implicit Types R : proph_map P V.
+
+  Lemma to_proph_map_valid R : âœ“ to_proph_map R.
+  Proof. intros l. rewrite lookup_fmap. by case (R !! l). Qed.
+
+  Lemma to_proph_map_insert p v R :
+    to_proph_map (<[p := v]> R) = <[p := Excl (v: option (leibnizC V))]> (to_proph_map R).
+  Proof. by rewrite /to_proph_map fmap_insert. Qed.
+
+  Lemma to_proph_map_delete p R :
+    to_proph_map (delete p R) = delete p (to_proph_map R).
+  Proof. by rewrite /to_proph_map fmap_delete. Qed.
+
+  Lemma lookup_to_proph_map_None R p :
+    R !! p = None â†’ to_proph_map R !! p = None.
+  Proof. by rewrite /to_proph_map lookup_fmap=> ->. Qed.
+
+  Lemma proph_map_singleton_included R p v :
+    {[p := Excl v]} â‰¼ to_proph_map R â†’ R !! p = Some v.
+  Proof.
+    rewrite singleton_included=> -[v' []].
+    rewrite /to_proph_map lookup_fmap fmap_Some_equiv=> -[v'' [Hp ->]].
+    intros [=->]%Some_included_exclusive%leibniz_equiv_iff; first done; last done.
+    apply excl_exclusive.
+  Qed.
+End to_proph_map.
+
+
+Lemma proph_map_init `{proph_mapPreG P V PVS} pvs ps :
+  (|==> âˆƒ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
+Proof.
+  iMod (own_alloc (â— to_proph_map âˆ…)) as (Î³) "Hh".
+  { apply: auth_auth_valid. exact: to_proph_map_valid. }
+  iModIntro. iExists (ProphMapG P V PVS _ _ _ Î³), âˆ…. iSplit; last by iFrame.
+  iPureIntro. split =>//.
+Qed.
+
+Section proph_map.
+  Context `{proph_mapG P V Î£}.
+  Implicit Types p : P.
+  Implicit Types v : option V.
+  Implicit Types R : proph_map P V.
+
+  (** General properties of mapsto *)
+  Global Instance proph_timeless p v : Timeless (proph p v).
+  Proof. rewrite proph_eq /proph_def. apply _. Qed.
+
+  Lemma proph_map_alloc R p v :
+    p âˆ‰ dom (gset _) R â†’
+    proph_map_auth R ==âˆ— proph_map_auth (<[p := v]> R) âˆ— proph p v.
+  Proof.
+    iIntros (Hp) "HR". rewrite /proph_map_ctx proph_eq /proph_def.
+    iMod (own_update with "HR") as "[HR Hl]".
+    { eapply auth_update_alloc,
+        (alloc_singleton_local_update _ _ (Excl $ (v : option (leibnizC _))))=> //.
+      apply lookup_to_proph_map_None. apply (iffLR (not_elem_of_dom _ _) Hp). }
+    iModIntro. rewrite /proph_map_auth to_proph_map_insert. iFrame.
+  Qed.
+
+  Lemma proph_map_remove R p v :
+    proph_map_auth R -âˆ— proph p v ==âˆ— proph_map_auth (delete p R).
+  Proof.
+    iIntros "HR Hp". rewrite /proph_map_ctx proph_eq /proph_def.
+    rewrite /proph_map_auth to_proph_map_delete. iApply (own_update_2 with "HR Hp").
+    apply auth_update_dealloc, (delete_singleton_local_update _ _ _).
+  Qed.
+
+  Lemma proph_map_valid R p v : proph_map_auth R -âˆ— proph p v -âˆ— âŒœR !! p = Some vâŒ.
+  Proof.
+    iIntros "HR Hp". rewrite /proph_map_ctx proph_eq /proph_def.
+    iDestruct (own_valid_2 with "HR Hp")
+      as %[HH%proph_map_singleton_included _]%auth_valid_discrete_2; auto.
+  Qed.
+End proph_map.
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 31e5c3a366f103685fb7e8f1ce0d237694cefeaa..d0cca5401f823ae2782e46e5d2e42adf42eb9fbb 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -35,7 +35,9 @@ Inductive expr :=
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
   | CAS (e0 : expr) (e1 : expr) (e2 : expr)
-  | FAA (e1 : expr) (e2 : expr).
+  | FAA (e1 : expr) (e2 : expr)
+  | NewProph
+  | ResolveProph (e1 : expr) (e2 : expr).
 
 Fixpoint to_expr (e : expr) : heap_lang.expr :=
   match e with
@@ -60,6 +62,8 @@ Fixpoint to_expr (e : expr) : heap_lang.expr :=
   | Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
   | CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
   | FAA e1 e2 => heap_lang.FAA (to_expr e1) (to_expr e2)
+  | NewProph => heap_lang.NewProph
+  | ResolveProph e1 e2 => heap_lang.ResolveProph (to_expr e1) (to_expr e2)
   end.
 
 Ltac of_expr e :=
@@ -94,6 +98,10 @@ Ltac of_expr e :=
      constr:(CAS e0 e1 e2)
   | heap_lang.FAA ?e1 ?e2 =>
      let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
+  | heap_lang.NewProph =>
+     constr:(NewProph)
+  | heap_lang.ResolveProph ?e1 ?e2 =>
+     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(ResolveProph e1 e2)
   | to_expr ?e => e
   | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
   | language.of_val ?v => constr:(Val v (of_val v) (to_of_val v))
@@ -108,10 +116,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   | Val _ _ _ | ClosedExpr _ => true
   | Var x => bool_decide (x âˆˆ X)
   | Rec f x e => is_closed (f :b: x :b: X) e
-  | Lit _ => true
+  | Lit _ | NewProph => true
   | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
      is_closed X e
-  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | ResolveProph e1 e2 =>
      is_closed X e1 && is_closed X e2
   | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
      is_closed X e0 && is_closed X e1 && is_closed X e2
@@ -171,6 +179,8 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   | Store e1 e2 => Store (subst x es e1) (subst x es e2)
   | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
   | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
+  | NewProph => NewProph
+  | ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
   end.
 Lemma to_expr_subst x er e :
   to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
@@ -190,6 +200,8 @@ Definition is_atomic (e : expr) :=
   | Fork _ => true
   (* Make "skip" atomic *)
   | App (Rec _ _ (Lit _)) (Lit _) => true
+  | NewProph => true
+  | ResolveProph e1 e2 => bool_decide (is_Some (to_val e1) âˆ§ is_Some (to_val e2))
   | _ => false
   end.
 Lemma is_atomic_correct s e : is_atomic e â†’ Atomic s (to_expr e).
@@ -293,4 +305,6 @@ Ltac reshape_expr e tac :=
   | CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
   | FAA ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (FaaLCtx v2 :: K) e1)
   | FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
+  | ResolveProph ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (ProphLCtx v2 :: K) e1)
+  | ResolveProph ?e1 ?e2 => go (ProphRCtx e1 :: K) e2
   end in go (@nil ectx_item) e.
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 55e7f5f5e41fbce3c9df3f0ed829461dc29c3d8c..9006687fa62732e3329ec44de369883f661cd564 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -6,10 +6,12 @@ Set Default Proof Using "Type".
 
 Definition heap_total Î£ `{heapPreG Î£} s e Ïƒ Ï† :
   (âˆ€ `{heapG Î£}, WP e @ s; âŠ¤ [{ v, âŒœÏ† vâŒ }]%I) â†’
-  sn step ([e], Ïƒ).
+  sn erased_step ([e], Ïƒ).
 Proof.
   intros Hwp; eapply (twp_total _ _); iIntros (?) "".
-  iMod (gen_heap_init Ïƒ) as (?) "Hh".
-  iModIntro. iExists gen_heap_ctx; iFrame.
-  iApply (Hwp (HeapG _ _ _)).
+  iMod (gen_heap_init Ïƒ.(heap)) as (?) "Hh".
+  iMod (proph_map_init [] Ïƒ.(used_proph_id)) as (?) "Hp".
+  iModIntro.
+  iExists (Î» Ïƒ Îºs, (gen_heap_ctx Ïƒ.(heap) âˆ— proph_map_ctx Îºs Ïƒ.(used_proph_id))%I). iFrame.
+  iApply (Hwp (HeapG _ _ _ _)).
 Qed.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index b53adc80ddba7e251d7872084b5b45f54c40434d..095aa0c67cb599721eec4930d54569293979f379 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -37,26 +37,26 @@ Qed.
 Record adequate {Î›} (s : stuckness) (e1 : expr Î›) (Ïƒ1 : state Î›)
     (Ï† : val Î› â†’ state Î› â†’ Prop) := {
   adequate_result t2 Ïƒ2 v2 :
-   rtc step ([e1], Ïƒ1) (of_val v2 :: t2, Ïƒ2) â†’ Ï† v2 Ïƒ2;
+   rtc erased_step ([e1], Ïƒ1) (of_val v2 :: t2, Ïƒ2) â†’ Ï† v2 Ïƒ2;
   adequate_not_stuck t2 Ïƒ2 e2 :
    s = NotStuck â†’
-   rtc step ([e1], Ïƒ1) (t2, Ïƒ2) â†’
+   rtc erased_step ([e1], Ïƒ1) (t2, Ïƒ2) â†’
    e2 âˆˆ t2 â†’ (is_Some (to_val e2) âˆ¨ reducible e2 Ïƒ2)
 }.
 
 Theorem adequate_tp_safe {Î›} (e1 : expr Î›) t2 Ïƒ1 Ïƒ2 Ï† :
   adequate NotStuck e1 Ïƒ1 Ï† â†’
-  rtc step ([e1], Ïƒ1) (t2, Ïƒ2) â†’
-  Forall (Î» e, is_Some (to_val e)) t2 âˆ¨ âˆƒ t3 Ïƒ3, step (t2, Ïƒ2) (t3, Ïƒ3).
+  rtc erased_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_not_stuck NotStuck e1 Ïƒ1 Ï† Had t2 Ïƒ2 e2) as [?|(e3&Ïƒ3&efs&?)];
+  destruct (adequate_not_stuck NotStuck 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.
-  right; exists (t2' ++ e3 :: t2'' ++ efs), Ïƒ3; econstructor; eauto.
+  right; exists Îº, (t2' ++ e3 :: t2'' ++ efs), Ïƒ3; econstructor; eauto.
 Qed.
 
 Section adequacy.
@@ -66,48 +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 Î¦ :
-  prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’
-  world' E Ïƒ1 âˆ— WP e1 @ s; E {{ Î¦ }}
-  ==âˆ— â–· |==> â—‡ (world' E Ïƒ2 âˆ— WP e2 @ s; E {{ Î¦ }} âˆ— wptp s efs).
+Lemma wp_step s E e1 Ïƒ1 Îº Îºs e2 Ïƒ2 efs Î¦ :
+  prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’
+  world' E Ïƒ1 (Îº ++ Îº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.
+  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)".
   iIntros "!> !>". by iMod ("H" with "[$Hw $HE]") as ">($ & $ & $)".
 Qed.
 
-Lemma wptp_step s e1 t1 t2 Ïƒ1 Ïƒ2 Î¦ :
-  step (e1 :: t1,Ïƒ1) (t2, Ïƒ2) â†’
-  world Ïƒ1 âˆ— WP e1 @ s; âŠ¤ {{ Î¦ }} âˆ— wptp s t1
-  ==âˆ— âˆƒ e2 t2', âŒœt2 = e2 :: t2'âŒ âˆ— â–· |==> â—‡ (world Ïƒ2 âˆ— WP e2 @ s; âŠ¤ {{ Î¦ }} âˆ— wptp s t2').
+Lemma wptp_step s e1 t1 t2 Îº Îºs Ïƒ1 Ïƒ2 Î¦ :
+  step (e1 :: t1,Ïƒ1) Îº (t2, Ïƒ2) â†’
+  world Ïƒ1 (Îº ++ Îºs) âˆ— WP e1 @ s; âŠ¤ {{ Î¦ }} âˆ— wptp s t1
+  ==âˆ— âˆƒ e2 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 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 t2 Ïƒ1 Ïƒ2 Î¦ :
-  nsteps step n (e1 :: t1, Ïƒ1) (t2, Ïƒ2) â†’
-  world Ïƒ1 âˆ— WP e1 @ s; âŠ¤ {{ Î¦ }} âˆ— wptp s t1 âŠ¢
+Lemma wptp_steps s n e1 t1 Îºs Îºs' t2 Ïƒ1 Ïƒ2 Î¦ :
+  nsteps n (e1 :: t1, Ïƒ1) Îºs (t2, Ïƒ2) â†’
+  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 t2 Ïƒ1 Ïƒ2; simpl; induction n as [|n IH]=> e1 t1 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 <- 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} :
@@ -123,9 +125,11 @@ Proof.
   by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
 Qed.
 
-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 @ s; âŠ¤ {{ v, âˆ€ Ïƒ, state_interp Ïƒ ={âŠ¤,âˆ…}=âˆ— âŒœÏ† v ÏƒâŒ }} âˆ— wptp s t1
+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 (Îº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.
@@ -135,19 +139,19 @@ 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:?.
   { iIntros "!> !> !%". left. by exists v. }
-  rewrite uPred_fupd_eq. iMod ("H" with "HÏƒ [-]") as ">(?&?&%&?)"; first by iFrame.
+  rewrite uPred_fupd_eq. iMod ("H" $! _ [] with "HÏƒ [-]") as ">(?&?&%&?)"; first by iFrame.
   iIntros "!> !> !%". by right.
 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 NotStuck t1
+Lemma wptp_safe n e1 Îºs Îºs' e2 t1 t2 Ïƒ1 Ïƒ2 Î¦ :
+  nsteps n (e1 :: t1, Ïƒ1) Îºs (t2, Ïƒ2) â†’ e2 âˆˆ t2 â†’
+  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.
@@ -157,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 e2 t1 t2 Ïƒ1 Ïƒ2 Ï† Î¦ :
-  nsteps step n (e1 :: t1, Ïƒ1) (t2, Ïƒ2) â†’
-  (state_interp Ïƒ2 ={âŠ¤,âˆ…}=âˆ— âŒœÏ†âŒ) âˆ— world Ïƒ1 âˆ— WP e1 @ s; âŠ¤ {{ Î¦ }} âˆ— wptp s t1
+Lemma wptp_invariance s n e1 Îºs Îºs' e2 t1 t2 Ïƒ1 Ïƒ2 Ï† Î¦ :
+  nsteps n (e1 :: t1, Ïƒ1) Îºs (t2, Ïƒ2) â†’
+  (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.
@@ -171,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 ?]%rtc_nsteps.
+  - 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.
-  - destruct s; last done. intros t2 Ïƒ2 e2 _ [n ?]%rtc_nsteps ?.
+    iApply (@wptp_result _ _ (IrisG _ _ _ Hinv Istate) _ _ _ _ _ []); first by eauto.
+    rewrite app_nil_r. 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) _ _ _ []); [by eauto..|].
+    rewrite app_nil_r. 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) â†’
-  rtc step ([e], Ïƒ1) (t2, Ïƒ2) â†’
+  (âˆ€ `{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 ?]%rtc_nsteps.
+  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) â†’
-  rtc step ([e], Ïƒ1) (t2, Ïƒ2) â†’
+  (âˆ€ `{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 7aee798202a9431586705b026e601d2e80de536f..c591c3a651bde6b9a09c0b8a4b36d4e6daf5a154 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -10,19 +10,19 @@ structure. Use the coercion [LanguageOfEctx] as defined in the bottom of this
 file for doing that. *)
 
 Section ectx_language_mixin.
-  Context {expr val ectx state : Type}.
+  Context {expr val ectx state observation : Type}.
   Context (of_val : val â†’ expr).
   Context (to_val : expr â†’ option val).
   Context (empty_ectx : ectx).
   Context (comp_ectx : ectx â†’ ectx â†’ ectx).
   Context (fill : ectx â†’ expr â†’ expr).
-  Context (head_step : expr â†’ state â†’ expr â†’ state â†’ list expr â†’ Prop).
+  Context (head_step : expr â†’ state â†’ list observation â†’ expr â†’ state â†’ list expr â†’ Prop).
 
   Record EctxLanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
     mixin_of_to_val e v : to_val e = Some v â†’ of_val v = e;
-    mixin_val_head_stuck e1 Ïƒ1 e2 Ïƒ2 efs :
-      head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ to_val e1 = None;
+    mixin_val_head_stuck e1 Ïƒ1 Îº e2 Ïƒ2 efs :
+      head_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ to_val e1 = None;
 
     mixin_fill_empty e : fill empty_ectx e = e;
     mixin_fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
@@ -35,10 +35,10 @@ Section ectx_language_mixin.
     mixin_ectx_positive K1 K2 :
       comp_ectx K1 K2 = empty_ectx â†’ K1 = empty_ectx âˆ§ K2 = empty_ectx;
 
-    mixin_step_by_val K K' e1 e1' Ïƒ1 e2 Ïƒ2 efs :
+    mixin_step_by_val K K' e1 e1' Ïƒ1 Îº e2 Ïƒ2 efs :
       fill K e1 = fill K' e1' â†’
       to_val e1 = None â†’
-      head_step e1' Ïƒ1 e2 Ïƒ2 efs â†’
+      head_step e1' Ïƒ1 Îº e2 Ïƒ2 efs â†’
       âˆƒ K'', K' = comp_ectx K K'';
   }.
 End ectx_language_mixin.
@@ -48,25 +48,26 @@ Structure ectxLanguage := EctxLanguage {
   val : Type;
   ectx : Type;
   state : Type;
+  observation : Type;
 
   of_val : val â†’ expr;
   to_val : expr â†’ option val;
   empty_ectx : ectx;
   comp_ectx : ectx â†’ ectx â†’ ectx;
   fill : ectx â†’ expr â†’ expr;
-  head_step : expr â†’ state â†’ expr â†’ state â†’ list expr â†’ Prop;
+  head_step : expr â†’ state â†’ list observation â†’ expr â†’ state â†’ list expr â†’ Prop;
 
   ectx_language_mixin :
     EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
 }.
 
-Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _} _.
+Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _ _} _.
 Arguments of_val {_} _%V.
 Arguments to_val {_} _%E.
 Arguments empty_ectx {_}.
 Arguments comp_ectx {_} _ _.
 Arguments fill {_} _ _%E.
-Arguments head_step {_} _%E _ _%E _ _.
+Arguments head_step {_} _%E _ _ _%E _ _.
 
 (* From an ectx_language, we can construct a language. *)
 Section ectx_language.
@@ -76,7 +77,7 @@ Section ectx_language.
   Implicit Types K : ectx Î›.
 
   (* Only project stuff out of the mixin that is not also in language *)
-  Lemma val_head_stuck e1 Ïƒ1 e2 Ïƒ2 efs : head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ to_val e1 = None.
+  Lemma val_head_stuck e1 Ïƒ1 Îº e2 Ïƒ2 efs : head_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ to_val e1 = None.
   Proof. apply ectx_language_mixin. Qed.
   Lemma fill_empty e : fill empty_ectx e = e.
   Proof. apply ectx_language_mixin. Qed.
@@ -89,17 +90,19 @@ Section ectx_language.
   Lemma ectx_positive K1 K2 :
     comp_ectx K1 K2 = empty_ectx â†’ K1 = empty_ectx âˆ§ K2 = empty_ectx.
   Proof. apply ectx_language_mixin. Qed.
-  Lemma step_by_val K K' e1 e1' Ïƒ1 e2 Ïƒ2 efs :
+  Lemma step_by_val K K' e1 e1' Ïƒ1 Îº e2 Ïƒ2 efs :
     fill K e1 = fill K' e1' â†’
     to_val e1 = None â†’
-    head_step e1' Ïƒ1 e2 Ïƒ2 efs â†’
+    head_step e1' Ïƒ1 Îº e2 Ïƒ2 efs â†’
     âˆƒ K'', K' = comp_ectx K K''.
   Proof. apply ectx_language_mixin. Qed.
 
   Definition head_reducible (e : expr Î›) (Ïƒ : state Î›) :=
-    âˆƒ e' Ïƒ' efs, head_step e Ïƒ e' Ïƒ' efs.
+    âˆƒ Îº e' Ïƒ' efs, head_step e Ïƒ Îº e' Ïƒ' efs.
+  Definition head_reducible_no_obs (e : expr Î›) (Ïƒ : state Î›) :=
+    âˆƒ e' Ïƒ' efs, head_step e Ïƒ [] e' Ïƒ' efs.
   Definition head_irreducible (e : expr Î›) (Ïƒ : state Î›) :=
-    âˆ€ e' Ïƒ' efs, Â¬head_step e Ïƒ e' Ïƒ' efs.
+    âˆ€ Îº e' Ïƒ' efs, Â¬head_step e Ïƒ Îº e' Ïƒ' efs.
   Definition head_stuck (e : expr Î›) (Ïƒ : state Î›) :=
     to_val e = None âˆ§ head_irreducible e Ïƒ.
 
@@ -108,14 +111,14 @@ Section ectx_language.
   Definition sub_redexes_are_values (e : expr Î›) :=
     âˆ€ K e', e = fill K e' â†’ to_val e' = None â†’ K = empty_ectx.
 
-  Inductive prim_step (e1 : expr Î›) (Ïƒ1 : state Î›)
+  Inductive prim_step (e1 : expr Î›) (Ïƒ1 : state Î›) (Îº : list (observation Î›))
       (e2 : expr Î›) (Ïƒ2 : state Î›) (efs : list (expr Î›)) : Prop :=
     Ectx_step K e1' e2' :
       e1 = fill K e1' â†’ e2 = fill K e2' â†’
-      head_step e1' Ïƒ1 e2' Ïƒ2 efs â†’ prim_step e1 Ïƒ1 e2 Ïƒ2 efs.
+      head_step e1' Ïƒ1 Îº e2' Ïƒ2 efs â†’ prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs.
 
-  Lemma Ectx_step' K e1 Ïƒ1 e2 Ïƒ2 efs :
-    head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ prim_step (fill K e1) Ïƒ1 (fill K e2) Ïƒ2 efs.
+  Lemma Ectx_step' K e1 Ïƒ1 Îº e2 Ïƒ2 efs :
+    head_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ prim_step (fill K e1) Ïƒ1 Îº (fill K e2) Ïƒ2 efs.
   Proof. econstructor; eauto. Qed.
 
   Definition ectx_lang_mixin : LanguageMixin of_val to_val prim_step.
@@ -123,29 +126,34 @@ Section ectx_language.
     split.
     - apply ectx_language_mixin.
     - apply ectx_language_mixin.
-    - intros ????? [??? -> -> ?%val_head_stuck].
+    - intros ?????? [??? -> -> ?%val_head_stuck].
       apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
   Qed.
 
   Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
 
   Definition head_atomic (a : atomicity) (e : expr Î›) : Prop :=
-    âˆ€ Ïƒ e' Ïƒ' efs,
-      head_step e Ïƒ e' Ïƒ' efs â†’
+    âˆ€ Ïƒ Îº e' Ïƒ' efs,
+      head_step e Ïƒ Îº e' Ïƒ' efs â†’
       if a is WeaklyAtomic then irreducible e' Ïƒ' else is_Some (to_val e').
 
   (* Some lemmas about this language *)
   Lemma fill_not_val K e : to_val e = None â†’ to_val (fill K e) = None.
   Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
 
-  Lemma head_prim_step e1 Ïƒ1 e2 Ïƒ2 efs :
-    head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ prim_step e1 Ïƒ1 e2 Ïƒ2 efs.
+  Lemma head_prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs :
+    head_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs.
   Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
 
+  Lemma head_reducible_no_obs_reducible e Ïƒ :
+    head_reducible_no_obs e Ïƒ â†’ head_reducible e Ïƒ.
+  Proof. intros (?&?&?&?). eexists. eauto. Qed.
   Lemma not_head_reducible e Ïƒ : Â¬head_reducible e Ïƒ â†” head_irreducible e Ïƒ.
   Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.
 
   Lemma head_prim_reducible e Ïƒ : head_reducible e Ïƒ â†’ reducible e Ïƒ.
+  Proof. intros (Îº&e'&Ïƒ'&efs&?). eexists Îº, e', Ïƒ', efs. by apply head_prim_step. Qed.
+  Lemma head_prim_reducible_no_obs e Ïƒ : head_reducible_no_obs e Ïƒ â†’ reducible_no_obs e Ïƒ.
   Proof. intros (e'&Ïƒ'&efs&?). eexists e', Ïƒ', efs. by apply head_prim_step. Qed.
   Lemma head_prim_irreducible e Ïƒ : irreducible e Ïƒ â†’ head_irreducible e Ïƒ.
   Proof.
@@ -155,7 +163,7 @@ Section ectx_language.
   Lemma prim_head_reducible e Ïƒ :
     reducible e Ïƒ â†’ sub_redexes_are_values e â†’ head_reducible e Ïƒ.
   Proof.
-    intros (e'&Ïƒ'&efs&[K e1' e2' -> -> Hstep]) ?.
+    intros (Îº&e'&Ïƒ'&efs&[K e1' e2' -> -> Hstep]) ?.
     assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
     rewrite fill_empty /head_reducible; eauto.
   Qed.
@@ -175,18 +183,18 @@ Section ectx_language.
   Lemma ectx_language_atomic a e :
     head_atomic a e â†’ sub_redexes_are_values e â†’ Atomic a e.
   Proof.
-    intros Hatomic_step Hatomic_fill Ïƒ e' Ïƒ' efs [K e1' e2' -> -> Hstep].
+    intros Hatomic_step Hatomic_fill Ïƒ Îº e' Ïƒ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
     rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
   Qed.
 
-  Lemma head_reducible_prim_step e1 Ïƒ1 e2 Ïƒ2 efs :
+  Lemma head_reducible_prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs :
     head_reducible e1 Ïƒ1 â†’
-    prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’
-    head_step e1 Ïƒ1 e2 Ïƒ2 efs.
+    prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’
+    head_step e1 Ïƒ1 Îº e2 Ïƒ2 efs.
   Proof.
-    intros (e2''&Ïƒ2''&efs''&?) [K e1' e2' -> -> Hstep].
-    destruct (step_by_val K empty_ectx e1' (fill K e1') Ïƒ1 e2'' Ïƒ2'' efs'')
+    intros (Îº'&e2''&Ïƒ2''&efs''&?) [K e1' e2' -> -> Hstep].
+    destruct (step_by_val K empty_ectx e1' (fill K e1') Ïƒ1 Îº' e2'' Ïƒ2'' efs'')
       as [K' [-> _]%symmetry%ectx_positive];
       eauto using fill_empty, fill_not_val, val_head_stuck.
     by rewrite !fill_empty.
@@ -197,19 +205,19 @@ Section ectx_language.
   Proof.
     split; simpl.
     - eauto using fill_not_val.
-    - intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
+    - intros ?????? [K' e1' e2' Heq1 Heq2 Hstep].
       by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
-    - intros e1 Ïƒ1 e2 Ïƒ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
-      destruct (step_by_val K K'' e1 e1'' Ïƒ1 e2'' Ïƒ2 efs) as [K' ->]; eauto.
+    - intros e1 Ïƒ1 Îº e2 Ïƒ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
+      destruct (step_by_val K K'' e1 e1'' Ïƒ1 Îº e2'' Ïƒ2 efs) as [K' ->]; eauto.
       rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
       exists (fill K' e2''); rewrite -fill_comp; split; auto.
       econstructor; eauto.
   Qed.
 
   Record pure_head_step (e1 e2 : expr Î›) := {
-    pure_head_step_safe Ïƒ1 : head_reducible e1 Ïƒ1;
-    pure_head_step_det Ïƒ1 e2' Ïƒ2 efs :
-      head_step e1 Ïƒ1 e2' Ïƒ2 efs â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = []
+    pure_head_step_safe Ïƒ1 : head_reducible_no_obs e1 Ïƒ1;
+    pure_head_step_det Ïƒ1 Îº e2' Ïƒ2 efs :
+      head_step e1 Ïƒ1 Îº e2' Ïƒ2 efs â†’ Îº = [] âˆ§ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = []
   }.
 
   Lemma pure_head_step_pure_step e1 e2 : pure_head_step e1 e2 â†’ pure_step e1 e2.
@@ -217,7 +225,7 @@ Section ectx_language.
     intros [Hp1 Hp2]. split.
     - intros Ïƒ. destruct (Hp1 Ïƒ) as (e2' & Ïƒ2 & efs & ?).
       eexists e2', Ïƒ2, efs. by apply head_prim_step.
-    - intros Ïƒ1 e2' Ïƒ2 efs ?%head_reducible_prim_step; eauto.
+    - intros Ïƒ1 Îº e2' Ïƒ2 efs ?%head_reducible_prim_step; eauto using head_reducible_no_obs_reducible.
   Qed.
 
   Global Instance pure_exec_fill K Ï† n e1 e2 :
@@ -237,6 +245,6 @@ work.
 Note that this trick no longer works when we switch to canonical projections
 because then the pattern match [let '...] will be desugared into projections. *)
 Definition LanguageOfEctx (Î› : ectxLanguage) : language :=
-  let '@EctxLanguage E V C St of_val to_val empty comp fill head mix := Î› in
-  @Language E V St of_val to_val _
-    (@ectx_lang_mixin (@EctxLanguage E V C St of_val to_val empty comp fill head mix)).
+  let '@EctxLanguage E V C St K of_val to_val empty comp fill head mix := Î› in
+  @Language E V St K of_val to_val _
+    (@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill head mix)).
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 419f8365e19ae3b506ec399a8096a4383624d5af..080d399471f27ba1ea659c3d11a2bd3b827b2ed2 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -16,51 +16,51 @@ 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 }})
+    âˆ€ e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={âˆ…,âˆ…,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 (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 }})
+    â–· âˆ€ e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={âˆ…,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 (?) "?".
+  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (???) "?".
   iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (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 â†’ Ïƒ1 = Ïƒ2) â†’
-  (|={E,E'}â–·=> âˆ€ e2 efs Ïƒ, âŒœhead_step e1 Ïƒ e2 Ïƒ efsâŒ â†’
+  (âˆ€ Ïƒ1 Îº e2 Ïƒ2 efs, head_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ Îº = [] âˆ§ Ïƒ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 {{ Î¦ }}.
 Proof using Hinh.
   iIntros (??) "H". iApply wp_lift_pure_step; [|by eauto|].
   { by destruct s; auto. }
   iApply (step_fupd_wand with "H"); iIntros "H".
-  iIntros (????). iApply "H"; eauto.
+  iIntros (?????). iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_pure_head_stuck E Î¦ 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 âˆ—
+    âˆ€ e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={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) "%".
-  iApply "H"; auto.
+  iIntros (Ïƒ1 Îº Îºs) "HÏƒ1". iMod ("H" with "HÏƒ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct s; auto. iIntros (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 âˆ—
+    â–· âˆ€ e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={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) "%".
-  iApply "H"; auto.
+  iIntros (Ïƒ1 Îº Îºs) "HÏƒ1". iMod ("H" with "HÏƒ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct s; auto. iNext. iIntros (e2 Ïƒ2 efs Hstep).
+  iApply "H"; eauto.
 Qed.
 
-Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Î¦} e1 :
+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))
+    âˆ€ e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={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 with "HÏƒ1") as "[$ H]"; iModIntro.
+  iIntros (v2 Ïƒ2 efs Hstep).
+  iMod ("H" $! 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))
+    â–· âˆ€ e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={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 (v2 Ïƒ2 efs Hstep).
+  iMod ("H" $! 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' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs') â†’
+  (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs',
+    head_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] âˆ§ Ïƒ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.
@@ -146,8 +147,8 @@ Qed.
 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') â†’
+  (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs',
+    head_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] âˆ§ Ïƒ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.
@@ -157,8 +158,8 @@ Qed.
 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' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ [] = efs') â†’
+  (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs',
+    head_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] âˆ§  Ïƒ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 bd73dfc65c8b23534a1d6f6d551d08603850a561..603d216516f1f8c2bb60ae876a68106f656f33f7 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -27,16 +27,16 @@ Below you can find the relevant parts:
 *)
 
 Section ectxi_language_mixin.
-  Context {expr val ectx_item state : Type}.
+  Context {expr val ectx_item state observation : Type}.
   Context (of_val : val â†’ expr).
   Context (to_val : expr â†’ option val).
   Context (fill_item : ectx_item â†’ expr â†’ expr).
-  Context (head_step : expr â†’ state â†’ expr â†’ state â†’ list expr â†’ Prop).
+  Context (head_step : expr â†’ state â†’ list observation â†’ expr â†’ state â†’ list expr â†’ Prop).
 
   Record EctxiLanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
     mixin_of_to_val e v : to_val e = Some v â†’ of_val v = e;
-    mixin_val_stuck e1 Ïƒ1 e2 Ïƒ2 efs : head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ to_val e1 = None;
+    mixin_val_stuck e1 Ïƒ1 Îº e2 Ïƒ2 efs : head_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ to_val e1 = None;
 
     mixin_fill_item_inj Ki : Inj (=) (=) (fill_item Ki);
     mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) â†’ is_Some (to_val e);
@@ -44,8 +44,8 @@ Section ectxi_language_mixin.
       to_val e1 = None â†’ to_val e2 = None â†’
       fill_item Ki1 e1 = fill_item Ki2 e2 â†’ Ki1 = Ki2;
 
-    mixin_head_ctx_step_val Ki e Ïƒ1 e2 Ïƒ2 efs :
-      head_step (fill_item Ki e) Ïƒ1 e2 Ïƒ2 efs â†’ is_Some (to_val e);
+    mixin_head_ctx_step_val Ki e Ïƒ1 Îº e2 Ïƒ2 efs :
+      head_step (fill_item Ki e) Ïƒ1 Îº e2 Ïƒ2 efs â†’ is_Some (to_val e);
   }.
 End ectxi_language_mixin.
 
@@ -54,21 +54,22 @@ Structure ectxiLanguage := EctxiLanguage {
   val : Type;
   ectx_item : Type;
   state : Type;
+  observation : Type;
 
   of_val : val â†’ expr;
   to_val : expr â†’ option val;
   fill_item : ectx_item â†’ expr â†’ expr;
-  head_step : expr â†’ state â†’ expr â†’ state â†’ list expr â†’ Prop;
+  head_step : expr â†’ state â†’ list observation â†’ expr â†’ state â†’ list expr â†’ Prop;
 
   ectxi_language_mixin :
     EctxiLanguageMixin of_val to_val fill_item head_step
 }.
 
-Arguments EctxiLanguage {_ _ _ _ _ _ _ _} _.
+Arguments EctxiLanguage {_ _ _ _ _ _ _ _ _} _.
 Arguments of_val {_} _%V.
 Arguments to_val {_} _%E.
 Arguments fill_item {_} _ _%E.
-Arguments head_step {_} _%E _ _%E _ _.
+Arguments head_step {_} _%E _ _ _%E _ _.
 
 Section ectxi_language.
   Context {Î› : ectxiLanguage}.
@@ -84,8 +85,8 @@ Section ectxi_language.
     to_val e1 = None â†’ to_val e2 = None â†’
     fill_item Ki1 e1 = fill_item Ki2 e2 â†’ Ki1 = Ki2.
   Proof. apply ectxi_language_mixin. Qed.
-  Lemma head_ctx_step_val Ki e Ïƒ1 e2 Ïƒ2 efs :
-    head_step (fill_item Ki e) Ïƒ1 e2 Ïƒ2 efs â†’ is_Some (to_val e).
+  Lemma head_ctx_step_val Ki e Ïƒ1 Îº e2 Ïƒ2 efs :
+    head_step (fill_item Ki e) Ïƒ1 Îº e2 Ïƒ2 efs â†’ is_Some (to_val e).
   Proof. apply ectxi_language_mixin. Qed.
 
   Definition fill (K : ectx) (e : expr Î›) : expr Î› := foldl (flip fill_item) e K.
@@ -109,7 +110,7 @@ Section ectxi_language.
     - intros K; induction K as [|Ki K IH]; rewrite /Inj; naive_solver.
     - done.
     - by intros [] [].
-    - intros K K' e1 e1' Ïƒ1 e2 Ïƒ2 efs Hfill Hred Hstep; revert K' Hfill.
+    - intros K K' e1 Îº e1' Ïƒ1 e2 Ïƒ2 efs Hfill Hred Hstep; revert K' Hfill.
       induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
       destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
       { rewrite fill_app in Hstep. apply head_ctx_step_val in Hstep.
@@ -147,6 +148,6 @@ Coercion ectxi_lang_ectx : ectxiLanguage >-> ectxLanguage.
 Coercion ectxi_lang : ectxiLanguage >-> language.
 
 Definition EctxLanguageOfEctxi (Î› : ectxiLanguage) : ectxLanguage :=
-  let '@EctxiLanguage E V C St of_val to_val fill head mix := Î› in
-  @EctxLanguage E V (list C) St of_val to_val _ _ _ _
-    (@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St of_val to_val fill head mix)).
+  let '@EctxiLanguage E V C St K of_val to_val fill head mix := Î› in
+  @EctxLanguage E V (list C) St K of_val to_val _ _ _ _
+    (@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St K of_val to_val fill head mix)).
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 8c50057f499e9ad7089d442916fb0f8433208fdf..58b8cc5c7056106c7ba04879e4f97b23a3c2f9e5 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -2,15 +2,18 @@ From iris.algebra Require Export ofe.
 Set Default Proof Using "Type".
 
 Section language_mixin.
-  Context {expr val state : Type}.
+  Context {expr val state observation : Type}.
   Context (of_val : val â†’ expr).
   Context (to_val : expr â†’ option val).
-  Context (prim_step : expr â†’ state â†’ expr â†’ state â†’ list expr â†’ Prop).
+  (** We annotate the reduction relation with observations [Îº], which we will
+     use in the definition of weakest preconditions to predict future
+     observations and assert correctness of the predictions. *)
+  Context (prim_step : expr â†’ state â†’ list observation â†’ expr â†’ state â†’ list expr â†’ Prop).
 
   Record LanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
     mixin_of_to_val e v : to_val e = Some v â†’ of_val v = e;
-    mixin_val_stuck e Ïƒ e' Ïƒ' efs : prim_step e Ïƒ e' Ïƒ' efs â†’ to_val e = None
+    mixin_val_stuck e Ïƒ Îº e' Ïƒ' efs : prim_step e Ïƒ Îº e' Ïƒ' efs â†’ to_val e = None
   }.
 End language_mixin.
 
@@ -18,9 +21,10 @@ Structure language := Language {
   expr : Type;
   val : Type;
   state : Type;
+  observation : Type;
   of_val : val â†’ expr;
   to_val : expr â†’ option val;
-  prim_step : expr â†’ state â†’ expr â†’ state â†’ list expr â†’ Prop;
+  prim_step : expr â†’ state â†’ list observation â†’ expr â†’ state â†’ list expr â†’ Prop;
   language_mixin : LanguageMixin of_val to_val prim_step
 }.
 Delimit Scope expr_scope with E.
@@ -28,10 +32,10 @@ Delimit Scope val_scope with V.
 Bind Scope expr_scope with expr.
 Bind Scope val_scope with val.
 
-Arguments Language {_ _ _ _ _ _} _.
+Arguments Language {_ _ _ _ _ _ _} _.
 Arguments of_val {_} _.
 Arguments to_val {_} _.
-Arguments prim_step {_} _ _ _ _ _.
+Arguments prim_step {_} _ _ _ _ _ _.
 
 Canonical Structure stateC Î› := leibnizC (state Î›).
 Canonical Structure valC Î› := leibnizC (val Î›).
@@ -42,12 +46,12 @@ Definition cfg (Î› : language) := (list (expr Î›) * state Î›)%type.
 Class LanguageCtx {Î› : language} (K : expr Î› â†’ expr Î›) := {
   fill_not_val e :
     to_val e = None â†’ to_val (K e) = None;
-  fill_step e1 Ïƒ1 e2 Ïƒ2 efs :
-    prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’
-    prim_step (K e1) Ïƒ1 (K e2) Ïƒ2 efs;
-  fill_step_inv e1' Ïƒ1 e2 Ïƒ2 efs :
-    to_val e1' = None â†’ prim_step (K e1') Ïƒ1 e2 Ïƒ2 efs â†’
-    âˆƒ e2', e2 = K e2' âˆ§ prim_step e1' Ïƒ1 e2' Ïƒ2 efs
+  fill_step e1 Ïƒ1 Îº e2 Ïƒ2 efs :
+    prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’
+    prim_step (K e1) Ïƒ1 Îº (K e2) Ïƒ2 efs;
+  fill_step_inv e1' Ïƒ1 Îº e2 Ïƒ2 efs :
+    to_val e1' = None â†’ prim_step (K e1') Ïƒ1 Îº e2 Ïƒ2 efs â†’
+    âˆƒ e2', e2 = K e2' âˆ§ prim_step e1' Ïƒ1 Îº e2' Ïƒ2 efs
 }.
 
 Instance language_ctx_id Î› : LanguageCtx (@id (expr Î›)).
@@ -64,13 +68,16 @@ Section language.
   Proof. apply language_mixin. Qed.
   Lemma of_to_val e v : to_val e = Some v â†’ of_val v = e.
   Proof. apply language_mixin. Qed.
-  Lemma val_stuck e Ïƒ e' Ïƒ' efs : prim_step e Ïƒ e' Ïƒ' efs â†’ to_val e = None.
+  Lemma val_stuck e Ïƒ Îº e' Ïƒ' efs : prim_step e Ïƒ Îº e' Ïƒ' efs â†’ to_val e = None.
   Proof. apply language_mixin. Qed.
 
   Definition reducible (e : expr Î›) (Ïƒ : state Î›) :=
-    âˆƒ e' Ïƒ' efs, prim_step e Ïƒ e' Ïƒ' efs.
+    âˆƒ Îº e' Ïƒ' efs, prim_step e Ïƒ Îº e' Ïƒ' efs.
+  (* Total WP only permits reductions without observations *)
+  Definition reducible_no_obs (e : expr Î›) (Ïƒ : state Î›) :=
+    âˆƒ e' Ïƒ' efs, prim_step e Ïƒ [] e' Ïƒ' efs.
   Definition irreducible (e : expr Î›) (Ïƒ : state Î›) :=
-    âˆ€ e' Ïƒ' efs, Â¬prim_step e Ïƒ e' Ïƒ' efs.
+    âˆ€ Îº e' Ïƒ' efs, Â¬prim_step e Ïƒ Îº e' Ïƒ' efs.
   Definition stuck (e : expr Î›) (Ïƒ : state Î›) :=
     to_val e = None âˆ§ irreducible e Ïƒ.
 
@@ -86,16 +93,35 @@ Section language.
      in case `e` reduces to a stuck non-value, there is no proof that the
      invariants have been established again. *)
   Class Atomic (a : atomicity) (e : expr Î›) : Prop :=
-    atomic Ïƒ e' Ïƒ' efs :
-      prim_step e Ïƒ e' Ïƒ' efs â†’
+    atomic Ïƒ e' Îº Ïƒ' efs :
+      prim_step e Ïƒ Îº e' Ïƒ' efs â†’
       if a is WeaklyAtomic then irreducible e' Ïƒ' else is_Some (to_val e').
 
-  Inductive step (Ï1 Ï2 : cfg Î›) : Prop :=
+  Inductive step (Ï1 : cfg Î›) (Îº : list (observation Î›)) (Ï2 : cfg Î›) : Prop :=
     | step_atomic e1 Ïƒ1 e2 Ïƒ2 efs t1 t2 :
        Ï1 = (t1 ++ e1 :: t2, Ïƒ1) â†’
        Ï2 = (t1 ++ e2 :: t2 ++ efs, Ïƒ2) â†’
-       prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’
-       step Ï1 Ï2.
+       prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’
+       step Ï1 Îº Ï2.
+  Hint Constructors step.
+
+  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 (Îº ++ Îºs) Ï3.
+  Hint Constructors nsteps.
+
+  Definition erased_step (Ï1 Ï2 : cfg Î›) := âˆƒ Îº, step Ï1 Îº Ï2.
+
+  Lemma erased_steps_nsteps Ï1 Ï2 :
+    rtc erased_step Ï1 Ï2 â†’
+    âˆƒ n Îºs, nsteps n Ï1 Îºs Ï2.
+  Proof.
+    induction 1; firstorder; eauto. (* FIXME: [naive_solver eauto] should be able to handle this *)
+  Qed.
 
   Lemma of_to_val_flip v e : of_val v = e â†’ to_val e = Some v.
   Proof. intros <-. by rewrite to_of_val. Qed.
@@ -103,9 +129,11 @@ Section language.
   Lemma not_reducible e Ïƒ : Â¬reducible e Ïƒ â†” irreducible e Ïƒ.
   Proof. unfold reducible, irreducible. naive_solver. Qed.
   Lemma reducible_not_val e Ïƒ : reducible e Ïƒ â†’ to_val e = None.
-  Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
+  Proof. intros (?&?&?&?&?); eauto using val_stuck. Qed.
+  Lemma reducible_no_obs_reducible e Ïƒ : reducible_no_obs e Ïƒ â†’ reducible e Ïƒ.
+  Proof. intros (?&?&?&?); eexists; eauto. Qed.
   Lemma val_irreducible e Ïƒ : is_Some (to_val e) â†’ irreducible e Ïƒ.
-  Proof. intros [??] ??? ?%val_stuck. by destruct (to_val e). Qed.
+  Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Î›).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
@@ -116,15 +144,21 @@ Section language.
   Lemma reducible_fill `{LanguageCtx Î› K} e Ïƒ :
     to_val e = None â†’ reducible (K e) Ïƒ â†’ reducible e Ïƒ.
   Proof.
-    intros ? (e'&Ïƒ'&efs&Hstep); unfold reducible.
+    intros ? (e'&Ïƒ'&k&efs&Hstep); unfold reducible.
+    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
+  Qed.
+  Lemma reducible_no_obs_fill `{LanguageCtx Î› K} e Ïƒ :
+    to_val e = None â†’ reducible_no_obs (K e) Ïƒ â†’ reducible_no_obs e Ïƒ.
+  Proof.
+    intros ? (e'&Ïƒ'&efs&Hstep); unfold reducible_no_obs.
     apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
   Qed.
   Lemma irreducible_fill `{LanguageCtx Î› K} e Ïƒ :
     to_val e = None â†’ irreducible e Ïƒ â†’ irreducible (K e) Ïƒ.
   Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
 
-  Lemma step_Permutation (t1 t1' t2 : list (expr Î›)) Ïƒ1 Ïƒ2 :
-    t1 â‰¡â‚š t1' â†’ step (t1,Ïƒ1) (t2,Ïƒ2) â†’ âˆƒ t2', t2 â‰¡â‚š t2' âˆ§ step (t1',Ïƒ1) (t2',Ïƒ2).
+  Lemma step_Permutation (t1 t1' t2 : list (expr Î›)) Îº Ïƒ1 Ïƒ2 :
+    t1 â‰¡â‚š t1' â†’ step (t1,Ïƒ1) Îº (t2,Ïƒ2) â†’ âˆƒ t2', t2 â‰¡â‚š t2' âˆ§ step (t1',Ïƒ1) Îº (t2',Ïƒ2).
   Proof.
     intros Ht [e1 Ïƒ1' e2 Ïƒ2' efs tl tr ?? Hstep]; simplify_eq/=.
     move: Ht; rewrite -Permutation_middle (symmetry_iff (â‰¡â‚š)).
@@ -133,32 +167,39 @@ Section language.
     by rewrite -!Permutation_middle !assoc_L Ht.
   Qed.
 
+  Lemma erased_step_Permutation (t1 t1' t2 : list (expr Î›)) Ïƒ1 Ïƒ2 :
+    t1 â‰¡â‚š t1' â†’ erased_step (t1,Ïƒ1) (t2,Ïƒ2) â†’ âˆƒ t2', t2 â‰¡â‚š t2' âˆ§ erased_step (t1',Ïƒ1) (t2',Ïƒ2).
+  Proof.
+    intros Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
+     (* FIXME: [naive_solver] should be able to handle this *)
+  Qed.
+
   Record pure_step (e1 e2 : expr Î›) := {
-    pure_step_safe Ïƒ1 : reducible e1 Ïƒ1;
-    pure_step_det Ïƒ1 e2' Ïƒ2 efs :
-      prim_step e1 Ïƒ1 e2' Ïƒ2 efs â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = []
+    pure_step_safe Ïƒ1 : reducible_no_obs e1 Ïƒ1;
+    pure_step_det Ïƒ1 Îº e2' Ïƒ2 efs :
+      prim_step e1 Ïƒ1 Îº e2' Ïƒ2 efs â†’ Îº = [] âˆ§ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = []
   }.
 
   (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
   succeeding when it did not actually do anything. *)
   Class PureExec (Ï† : Prop) (n : nat) (e1 e2 : expr Î›) :=
-    pure_exec : Ï† â†’ nsteps pure_step n e1 e2.
+    pure_exec : Ï† â†’ relations.nsteps pure_step n e1 e2.
 
   Lemma pure_step_ctx K `{LanguageCtx Î› K} e1 e2 :
     pure_step e1 e2 â†’
     pure_step (K e1) (K e2).
   Proof.
     intros [Hred Hstep]. split.
-    - unfold reducible in *. naive_solver eauto using fill_step.
-    - intros Ïƒ1 e2' Ïƒ2 efs Hpstep.
-      destruct (fill_step_inv e1 Ïƒ1 e2' Ïƒ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
+    - unfold reducible_no_obs in *. naive_solver eauto using fill_step.
+    - intros Ïƒ1 Îº e2' Ïƒ2 efs Hpstep.
+      destruct (fill_step_inv e1 Ïƒ1 Îº e2' Ïƒ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
       + destruct (Hred Ïƒ1) as (? & ? & ? & ?); eauto using val_stuck.
-      + destruct (Hstep Ïƒ1 e2'' Ïƒ2 efs) as (-> & -> & ->); auto.
+      + edestruct (Hstep Ïƒ1 Îº e2'' Ïƒ2 efs) as (? & -> & -> & ->); auto.
   Qed.
 
   Lemma pure_step_nsteps_ctx K `{LanguageCtx Î› K} n e1 e2 :
-    nsteps pure_step n e1 e2 â†’
-    nsteps pure_step n (K e1) (K e2).
+    relations.nsteps pure_step n e1 e2 â†’
+    relations.nsteps pure_step n (K e1) (K e2).
   Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.
 
   (* We do not make this an instance because it is awfully general. *)
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 637b6258e4c44f8d3e44165b348131fd8d6d6747..1185a506fca4a1b23b6944e673daf9e442f9adaf 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -11,56 +11,59 @@ Implicit Types Ïƒ : state Î›.
 Implicit Types P Q : iProp Î£.
 Implicit Types Î¦ : val Î› â†’ iProp Î£.
 
+Hint Resolve reducible_no_obs_reducible.
+
 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 }})
+    âˆ€ e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={âˆ…,âˆ…,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 }})
+    â–· âˆ€ e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={âˆ…,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 â†’ Ïƒ1 = Ïƒ2) â†’
-  (|={E,E'}â–·=> âˆ€ e2 efs Ïƒ, âŒœprim_step e1 Ïƒ e2 Ïƒ efsâŒ â†’
+  (âˆ€ Îº Ïƒ1 e2 Ïƒ2 efs, prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ Îº = [] âˆ§ Ïƒ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 {{ Î¦ }}.
 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 (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 +74,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,14 +82,14 @@ 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 âˆ—
+    âˆ€ e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={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 "_".
@@ -99,28 +102,29 @@ 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 âˆ—
+    â–· âˆ€ e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={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' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs')â†’
+  (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs', prim_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] âˆ§ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs')â†’
   (|={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 s E E'); try done.
-  { by intros; eapply Hpuredet. }
+  { by naive_solver. }
   iApply (step_fupd_wand with "H"); iIntros "H".
-  by iIntros (e' efs' Ïƒ (_&->&->)%Hpuredet).
+  by iIntros (Îº e' efs' Ïƒ (->&_&->&->)%Hpuredet).
 Qed.
 
 Lemma wp_pure_step_fupd `{Inhabited (state Î›)} s E E' e1 e2 Ï† n Î¦ :
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 59f471673c84e1a5b79df1b4ef50c096aa53e1cf..42455a4d165a3a93c063b0b2ee1df86fa065dadc 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -5,65 +5,86 @@ 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_name : gname;
+  ownP_state_inG :> inG Î£ (authR (optionUR (exclR (leibnizC Î›state))));
+  ownP_obs_inG :> inG Î£ (authR (optionUR (exclR (leibnizC (list Î›observation)))));
+  ownP_state_name : gname;
+  ownP_obs_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_state_name (â— (Excl' (Ïƒ:leibnizC Î›state))) âˆ—
+                       own ownP_obs_name (â— (Excl' (Îºs:leibnizC (list Î›observation)))))%I
 }.
 Global Opaque iris_invG.
 
-Definition ownPÎ£ (Î›state : Type) : gFunctors :=
+Definition ownPÎ£ (Î›state Î›observation : Type) : gFunctors :=
   #[invÎ£;
-    GFunctor (authUR (optionUR (exclR (leibnizC Î›state))))].
+    GFunctor (authR (optionUR (exclR (leibnizC Î›state))));
+    GFunctor (authR (optionUR (exclR (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_state_inG :> inG Î£ (authR (optionUR (exclR (leibnizC Î›state))));
+  ownPPre_obs_inG :> inG Î£ (authR (optionUR (exclR (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' Ïƒ)).
-Typeclasses Opaque ownP.
-Instance: Params (@ownP) 3.
+Definition ownP_state `{ownPG' Î›state Î›observation Î£} (Ïƒ : Î›state) : iProp Î£ :=
+  own ownP_state_name (â—¯ (Excl' (Ïƒ:leibnizC Î›state))).
 
+Definition ownP_obs `{ownPG' Î›state Î›observation Î£} (Îºs: list Î›observation) : iProp Î£ :=
+  own ownP_obs_name (â—¯ (Excl' (Îºs:leibnizC (list Î›observation)))).
+
+Typeclasses Opaque ownP_state ownP_obs.
+Instance: Params (@ownP_state) 3.
+Instance: Params (@ownP_obs) 3.
 
 (* Adequacy *)
 Theorem ownP_adequacy Î£ `{ownPPreG Î› Î£} s e Ïƒ Ï† :
-  (âˆ€ `{ownPG Î› Î£}, ownP Ïƒ âŠ¢ WP e @ s; âŠ¤ {{ v, âŒœÏ† vâŒ }}) â†’
+  (âˆ€ `{ownPG Î› Î£} Îºs, ownP_state Ïƒ âˆ— ownP_obs Îº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 _)) â‹… â—¯ (Excl' Ïƒ)))
     as (Î³Ïƒ) "[HÏƒ HÏƒf]"; first done.
-  iModIntro. iExists (Î» Ïƒ, own Î³Ïƒ (â— (Excl' (Ïƒ:leibnizC _)))). iFrame "HÏƒ".
-  iApply (Hwp (OwnPG _ _ _ _ Î³Ïƒ)). by rewrite /ownP.
+  iMod (own_alloc (â— (Excl' (Îºs : leibnizC _)) â‹… â—¯ (Excl' Îºs)))
+    as (Î³Îºs) "[HÎºs HÎºsf]"; first done.
+  iModIntro. iExists (Î» Ïƒ Îºs,
+                      own Î³Ïƒ (â— (Excl' (Ïƒ:leibnizC _))) âˆ— own Î³Îºs (â— (Excl' (Îºs:leibnizC _))))%I.
+  iFrame "HÏƒ HÎºs".
+  iApply (Hwp (OwnPG _ _ _ _ _ _ Î³Ïƒ Î³Îºs)). rewrite /ownP_state /ownP_obs. iFrame.
 Qed.
 
 Theorem ownP_invariance Î£ `{ownPPreG Î› Î£} s e Ïƒ1 t2 Ïƒ2 Ï† :
-  (âˆ€ `{ownPG Î› Î£},
-    ownP Ïƒ1 ={âŠ¤}=âˆ— WP e @ s; âŠ¤ {{ _, True }} âˆ— |={âŠ¤,âˆ…}=> âˆƒ Ïƒ', ownP Ïƒ' âˆ§ âŒœÏ† Ïƒ'âŒ) â†’
-  rtc step ([e], Ïƒ1) (t2, Ïƒ2) â†’
+  (âˆ€ `{ownPG Î› Î£} Îºs,
+      ownP_state Ïƒ1 âˆ— ownP_obs Îºs ={âŠ¤}=âˆ— WP e @ s; âŠ¤ {{ _, True }} âˆ—
+      |={âŠ¤,âˆ…}=> âˆƒ Ïƒ' Îºs', ownP_state Ïƒ' âˆ— ownP_obs Îº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 _)) â‹… â—¯ (Excl' Ïƒ1)))
     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.
+  iMod (own_alloc (â— (Excl' (Îºs ++ Îºs' : leibnizC _)) â‹… â—¯ (Excl' (Îºs ++ Îºs'))))
+    as (Î³Îºs) "[HÎºs HÎºsf]"; first done.
+  iExists (Î» Ïƒ Îºs',
+           own Î³Ïƒ (â— (Excl' (Ïƒ:leibnizC _))) âˆ— own Î³Îºs (â— (Excl' (Îºs':leibnizC _))))%I.
+  iFrame "HÏƒ HÎºs".
+  iMod (Hwp (OwnPG _ _ _ _ _ _ Î³Ïƒ Î³Îºs) with "[HÏƒf HÎºsf]") as "[$ H]";
+    first by rewrite /ownP_state /ownP_obs; iFrame.
+  iIntros "!> [HÏƒ HÎºs]". iMod "H" as (Ïƒ2' Îºs'') "[HÏƒf [HÎºsf %]]". rewrite/ownP_state /ownP_obs.
+  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.
 Qed.
 
 
@@ -74,118 +95,139 @@ 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_state Ïƒ2 -âˆ— ownP_obs Îº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.
+    iIntros "[HÏƒâ— HÎºsâ—] HÏƒâ—¯ HÎºsâ—¯". rewrite /ownP_state /ownP_obs.
+    iDestruct (own_valid_2 with "HÏƒâ— HÏƒâ—¯")
+      as %[Hps _]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "HÎºsâ— HÎºsâ—¯")
+      as %[Hpo _]%auth_valid_discrete_2.
+    pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
+    pose proof (leibniz_equiv _ _ (Excl_included _ _ Hpo)) as ->.
+    done.
   Qed.
-  Lemma ownP_twice Ïƒ1 Ïƒ2 : ownP Ïƒ1 âˆ— ownP Ïƒ2 âŠ¢ False.
-  Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
-  Global Instance ownP_timeless Ïƒ : Timeless (@ownP (state Î›) Î£ _ Ïƒ).
-  Proof. rewrite /ownP; apply _. Qed.
+  Lemma ownP_state_twice Ïƒ1 Ïƒ2 : ownP_state Ïƒ1 âˆ— ownP_state Ïƒ2 âŠ¢ False.
+  Proof. rewrite /ownP_state -own_op own_valid. by iIntros (?). Qed.
+  Lemma ownP_obs_twice Îºs1 Îºs2 : ownP_obs Îºs1 âˆ— ownP_obs Îºs2 âŠ¢ False.
+  Proof. rewrite /ownP_obs -own_op own_valid. by iIntros (?). Qed.
+  Global Instance ownP_state_timeless Ïƒ : Timeless (@ownP_state (state Î›) (observation Î›) Î£ _ Ïƒ).
+  Proof. rewrite /ownP_state; apply _. Qed.
+  Global Instance ownP_obs_timeless Îºs : Timeless (@ownP_obs (state Î›) (observation Î›) Î£ _ Îºs).
+  Proof. rewrite /ownP_obs; 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_state Ïƒ1 âˆ— â–· ownP_obs Îºs âˆ—
+      â–· âˆ€ Îº Îºs' e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs âˆ§ Îºs = Îº ++ Îºs'âŒ -âˆ—
+      ownP_state Ïƒ2 âˆ— ownP_obs Îº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 %->.
+    - iApply wp_lift_step; [done|]; iIntros (Ïƒ1 Îº Îºs) "HÏƒÎºs".
+      iMod "H" as (Ïƒ1' Îºs' ?) "[>HÏƒf [>HÎºsf H]]".
+      iDestruct (ownP_eq with "HÏƒÎºs HÏƒf HÎºsf") as %[<- <-].
       iModIntro; iSplit; [by destruct s|]; iNext; iIntros (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)). }
-      iFrame "HÏƒ". iApply ("H" with "[]"); eauto.
+      iDestruct "HÏƒÎºs" as "[HÏƒ HÎºs]".
+      rewrite /ownP_state /ownP_obs.
+      iMod (own_update_2 with "HÏƒ HÏƒf") as "[HÏƒ HÏƒf]".
+      { apply auth_update. apply: option_local_update.
+         by apply: (exclusive_local_update _ (Excl Ïƒ2)). }
+      iMod (own_update_2 with "HÎºs HÎºsf") as "[HÎºs HÎºsf]".
+      { apply auth_update. apply: option_local_update.
+        by apply: (exclusive_local_update _ (Excl (Îºs:leibnizC _))). }
+      iFrame "HÏƒ HÎºs". iApply ("H" with "[]"); eauto with iFrame.
   Qed.
 
   Lemma ownP_lift_stuck E Î¦ e :
-    (|={E,âˆ…}=> âˆƒ Ïƒ, âŒœstuck e ÏƒâŒ âˆ— â–· ownP Ïƒ)
+    (|={E,âˆ…}=> âˆƒ Ïƒ Îºs, âŒœstuck e ÏƒâŒ âˆ— â–· (ownP_state Ïƒ âˆ— ownP_obs Îºs))
     âŠ¢ WP e @ E ?{{ Î¦ }}.
   Proof.
     iIntros "H". destruct (to_val e) as [v|] eqn:EQe.
     - apply of_to_val in EQe as <-. iApply fupd_wp.
-      iMod "H" as (Ïƒ1) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
+      iMod "H" as (Ïƒ1 Îºs) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
       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 %->.
+    - iApply wp_lift_stuck; [done|]. iIntros (Ïƒ1 Îºs) "HÏƒ".
+      iMod "H" as (Ïƒ1' Îºs') "(% & >[HÏƒf HÎºsf])".
+      by iDestruct (ownP_eq with "HÏƒ HÏƒf HÎºsf") 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 â†’ Ïƒ1 = Ïƒ2) â†’
-    (â–· âˆ€ e2 efs Ïƒ, âŒœprim_step e1 Ïƒ e2 Ïƒ efsâŒ â†’
+    (âˆ€ Ïƒ1 Îº e2 Ïƒ2 efs, prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ Îº = [] âˆ§ Ïƒ1 = Ïƒ2) â†’
+    (â–· âˆ€ Îº e2 efs Ïƒ, âŒœprim_step e1 Ïƒ Îº e2 Ïƒ efsâŒ â†’
       WP e2 @ s; E {{ Î¦ }} âˆ— [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ {{ _, True }})
     âŠ¢ WP e1 @ s; E {{ Î¦ }}.
   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 (fupd_intro_mask' E âˆ…) as "Hclose"; first set_solver.
+    iIntros (Ïƒ1 Îº Îºs) "HÏƒ". iMod (fupd_intro_mask' E âˆ…) as "Hclose"; first set_solver.
     iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 Ïƒ2 efs ?).
-    destruct (Hstep Ïƒ1 e2 Ïƒ2 efs); auto; subst.
+    destruct (Hstep Ïƒ1 Îº e2 Ïƒ2 efs); auto; subst.
     by iMod "Hclose"; iModIntro; iFrame; iApply "H".
   Qed.
 
   (** Derived lifting lemmas. *)
-  Lemma ownP_lift_atomic_step {s E Î¦} e1 Ïƒ1 :
+  Lemma ownP_lift_atomic_step {s E Î¦} e1 Ïƒ1 Îºs :
     (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 -âˆ—
+    (â–· (ownP_state Ïƒ1 âˆ— ownP_obs Îºs) âˆ—
+       â–· âˆ€ Îº Îºs' e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs âˆ§ Îºs = Îº ++ Îºs'âŒ -âˆ—
+         ownP_state Ïƒ2 -âˆ— ownP_obs Îºs' -âˆ—
       from_option Î¦ False (to_val e2) âˆ— [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ {{ _, True }})
     âŠ¢ WP e1 @ s; E {{ Î¦ }}.
   Proof.
-    iIntros (?) "[HÏƒ H]"; iApply ownP_lift_step.
+    iIntros (?) "[[HÏƒ HÎºs] H]"; iApply ownP_lift_step.
     iMod (fupd_intro_mask' E âˆ…) as "Hclose"; first set_solver.
-    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..|].
+    iModIntro; iExists Ïƒ1, Îºs; iFrame; iSplit; first by destruct s.
+    iNext; iIntros (Îº Îºs' e2 Ïƒ2 efs [??]) "[HÏƒ HÎºs]".
+    iDestruct ("H" $! Îº Îºs' e2 Ïƒ2 efs with "[] [HÏƒ] [HÎºs]") as "[HÎ¦ $]"; [by eauto..|].
     destruct (to_val e2) eqn:?; last by iExFalso.
     iMod "Hclose"; iApply wp_value; last done. by apply of_to_val.
   Qed.
 
-  Lemma ownP_lift_atomic_det_step {s E Î¦ e1} Ïƒ1 v2 Ïƒ2 efs :
+  Lemma ownP_lift_atomic_det_step {s E Î¦ e1} Ïƒ1 Îº Îºs v2 Ïƒ2 efs :
     (if s is NotStuck then reducible e1 Ïƒ1 else to_val e1 = None) â†’
-    (âˆ€ e2' Ïƒ2' efs', prim_step e1 Ïƒ1 e2' Ïƒ2' efs' â†’
-                     Ïƒ2 = Ïƒ2' âˆ§ to_val e2' = Some v2 âˆ§ efs = efs') â†’
-    â–· ownP Ïƒ1 âˆ— â–· (ownP Ïƒ2 -âˆ—
+    (âˆ€ Îº' e2' Ïƒ2' efs', prim_step e1 Ïƒ1 Îº' e2' Ïƒ2' efs' â†’
+                     Îº = Îº' âˆ§ Ïƒ2 = Ïƒ2' âˆ§ to_val e2' = Some v2 âˆ§ efs = efs') â†’
+    â–· (ownP_state Ïƒ1 âˆ— ownP_obs (Îº ++ Îºs)) âˆ— â–· (ownP_state Ïƒ2 -âˆ— ownP_obs Îºs -âˆ—
       Î¦ 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".
+    iIntros (? Hdet) "[[HÏƒ1 HÎºs] HÏƒ2]"; iApply ownP_lift_atomic_step; try done.
+    iFrame; iNext; iIntros (Îº' Îºs' e2' Ïƒ2' efs' (? & Heq)) "HÏƒ2' HÎºs'".
+    edestruct (Hdet Îº') as (->&->&Hval&->); first done. rewrite Hval. apply app_inv_head in Heq as ->.
+    iApply ("HÏƒ2" with "HÏƒ2' HÎºs'").
   Qed.
 
-  Lemma ownP_lift_atomic_det_step_no_fork {s E e1} Ïƒ1 v2 Ïƒ2 :
+  Lemma ownP_lift_atomic_det_step_no_fork {s E e1} Ïƒ1 Îº Îºs v2 Ïƒ2 :
     (if s is NotStuck then reducible e1 Ïƒ1 else to_val e1 = None) â†’
-    (âˆ€ e2' Ïƒ2' efs', prim_step e1 Ïƒ1 e2' Ïƒ2' efs' â†’
-      Ïƒ2 = Ïƒ2' âˆ§ to_val e2' = Some v2 âˆ§ [] = efs') â†’
-    {{{ â–· ownP Ïƒ1 }}} e1 @ s; E {{{ RET v2; ownP Ïƒ2 }}}.
+    (âˆ€ Îº' e2' Ïƒ2' efs', prim_step e1 Ïƒ1 Îº' e2' Ïƒ2' efs' â†’
+      Îº = Îº' âˆ§ Ïƒ2 = Ïƒ2' âˆ§ to_val e2' = Some v2 âˆ§ [] = efs') â†’
+    {{{ â–· (ownP_state Ïƒ1 âˆ— ownP_obs (Îº ++ Îºs)) }}} e1 @ s; E {{{ RET v2; ownP_state Ïƒ2 âˆ— ownP_obs Îºs}}}.
   Proof.
-    intros. rewrite -(ownP_lift_atomic_det_step Ïƒ1 v2 Ïƒ2 []); [|done..].
-    rewrite big_sepL_nil right_id. by apply bi.wand_intro_r.
+    intros. rewrite -(ownP_lift_atomic_det_step Ïƒ1 Îº Îºs v2 Ïƒ2 []); [|done..].
+    rewrite big_sepL_nil right_id. apply bi.wand_intro_r. iIntros "[Hs Hs']".
+    iSplitL "Hs"; first by iFrame. iModIntro. iIntros "HÏƒ2 HÎºs". iApply "Hs'". iFrame.
   Qed.
 
   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' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs')â†’
+    (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs', prim_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] âˆ§ Ïƒ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=>//.
-    by apply Hpuredet. 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' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ [] = efs') â†’
+    (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs', prim_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] âˆ§ Ïƒ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.
@@ -203,74 +245,77 @@ Section ectx_lifting.
   Hint Resolve head_stuck_stuck.
 
   Lemma ownP_lift_head_step s E Î¦ e1 :
-    (|={E,âˆ…}=> âˆƒ Ïƒ1, âŒœhead_reducible e1 Ïƒ1âŒ âˆ— â–· ownP Ïƒ1 âˆ—
-      â–· âˆ€ e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 e2 Ïƒ2 efsâŒ -âˆ— ownP Ïƒ2
+    (|={E,âˆ…}=> âˆƒ Ïƒ1 Îºs, âŒœhead_reducible e1 Ïƒ1âŒ âˆ— â–· (ownP_state Ïƒ1  âˆ— ownP_obs Îºs) âˆ—
+            â–· âˆ€ Îº Îºs' e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efs âˆ§ Îºs = Îº ++ Îºs'âŒ -âˆ—
+            ownP_state Ïƒ2 -âˆ— ownP_obs Îºs'
             ={âˆ…,E}=âˆ— WP e2 @ s; E {{ Î¦ }} âˆ— [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ {{ _, True }})
     âŠ¢ WP e1 @ s; E {{ Î¦ }}.
   Proof.
     iIntros "H". iApply ownP_lift_step.
-    iMod "H" as (Ïƒ1 ?) "[HÏƒ1 Hwp]". iModIntro. iExists Ïƒ1. iSplit.
+    iMod "H" as (Ïƒ1 Îºs ?) "[>[HÏƒ1 HÎºs] Hwp]". iModIntro. iExists Ïƒ1, Îºs. iSplit.
     { destruct s; try by eauto using reducible_not_val. }
-    iFrame. iNext. iIntros (e2 Ïƒ2 efs) "% ?".
-    iApply ("Hwp" with "[]"); eauto.
+    iFrame. iNext. iIntros (Îº Îºs' e2 Ïƒ2 efs [? ->]) "[HÏƒ2 HÎºs']".
+    iApply ("Hwp" with "[] HÏƒ2"); eauto.
   Qed.
 
   Lemma ownP_lift_head_stuck E Î¦ e :
     sub_redexes_are_values e â†’
-    (|={E,âˆ…}=> âˆƒ Ïƒ, âŒœhead_stuck e ÏƒâŒ âˆ— â–· ownP Ïƒ)
+    (|={E,âˆ…}=> âˆƒ Ïƒ Îºs, âŒœhead_stuck e ÏƒâŒ âˆ— â–· (ownP_state Ïƒ âˆ— ownP_obs Îºs))
     âŠ¢ WP e @ E ?{{ Î¦ }}.
   Proof.
-    iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (Ïƒ) "[% >HÏƒ]".
-    iExists Ïƒ. by auto.
+    iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (Ïƒ Îºs) "[% >[HÏƒ HÎºs]]".
+    iExists Ïƒ, Îºs. iModIntro. by auto with iFrame.
   Qed.
 
   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 â†’ Ïƒ1 = Ïƒ2) â†’
-    (â–· âˆ€ e2 efs Ïƒ, âŒœhead_step e1 Ïƒ e2 Ïƒ efsâŒ â†’
+    (âˆ€ Ïƒ1 Îº e2 Ïƒ2 efs, head_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ Îº = [] âˆ§ Ïƒ1 = Ïƒ2) â†’
+    (â–· âˆ€ Îº e2 efs Ïƒ, âŒœhead_step e1 Ïƒ Îº e2 Ïƒ efsâŒ â†’
       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 s; auto. }
-    iNext. iIntros (????). iApply "H"; eauto.
+    iNext. iIntros (?????). iApply "H"; eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_head_step {s E Î¦} e1 Ïƒ1 :
+  Lemma ownP_lift_atomic_head_step {s E Î¦} e1 Ïƒ1 Îºs :
     head_reducible e1 Ïƒ1 â†’
-    â–· ownP Ïƒ1 âˆ— â–· (âˆ€ e2 Ïƒ2 efs,
-    âŒœhead_step e1 Ïƒ1 e2 Ïƒ2 efsâŒ -âˆ— ownP Ïƒ2 -âˆ—
+    â–· (ownP_state Ïƒ1 âˆ— ownP_obs Îºs) âˆ— â–· (âˆ€ Îº Îºs' e2 Ïƒ2 efs,
+    âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efs âˆ§ Îºs = Îº ++ Îºs'âŒ -âˆ— ownP_state Ïƒ2 -âˆ— ownP_obs Îºs' -âˆ—
       from_option Î¦ False (to_val e2) âˆ— [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ {{ _, True }})
     âŠ¢ WP e1 @ s; E {{ Î¦ }}.
   Proof.
-    iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto.
+    iIntros (?) "[Hst H]". iApply ownP_lift_atomic_step; eauto.
     { by destruct s; eauto using reducible_not_val. }
-    iFrame. iNext. iIntros (???) "% ?". iApply ("H" with "[]"); eauto.
+    iSplitL "Hst"; first done.
+    iNext. iIntros (????? [? ->]) "HÏƒ ?". iApply ("H" with "[] HÏƒ"); eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_det_head_step {s E Î¦ e1} Ïƒ1 v2 Ïƒ2 efs :
+  Lemma ownP_lift_atomic_det_head_step {s E Î¦ e1} Ïƒ1 Îº Îºs v2 Ïƒ2 efs :
     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 @ s; âŠ¤ {{ _, True }})
+    (âˆ€ Îº' e2' Ïƒ2' efs', head_step e1 Ïƒ1 Îº' e2' Ïƒ2' efs' â†’
+      Îº = Îº' âˆ§ Ïƒ2 = Ïƒ2' âˆ§ to_val e2' = Some v2 âˆ§ efs = efs') â†’
+    â–· (ownP_state Ïƒ1 âˆ— ownP_obs (Îº ++ Îºs)) âˆ— â–· (ownP_state Ïƒ2 -âˆ— ownP_obs Îºs -âˆ—
+                                                    Î¦ v2 âˆ— [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ {{ _, True }})
     âŠ¢ WP e1 @ s; E {{ Î¦ }}.
   Proof.
-    by destruct s; eauto 10 using ownP_lift_atomic_det_step, reducible_not_val.
+    intros Hr Hs. destruct s; apply ownP_lift_atomic_det_step; eauto using reducible_not_val.
   Qed.
 
-  Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} Ïƒ1 v2 Ïƒ2 :
+  Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} Ïƒ1 Îº Îºs v2 Ïƒ2 :
     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 @ s; E {{{ RET v2; ownP Ïƒ2 }}}.
+    (âˆ€ Îº' e2' Ïƒ2' efs', head_step e1 Ïƒ1 Îº' e2' Ïƒ2' efs' â†’
+      Îº = Îº' âˆ§ Ïƒ2 = Ïƒ2' âˆ§ to_val e2' = Some v2 âˆ§ [] = efs') â†’
+    {{{ â–· (ownP_state Ïƒ1 âˆ— ownP_obs (Îº ++ Îºs)) }}} e1 @ s; E {{{ RET v2; ownP_state Ïƒ2 âˆ— ownP_obs Îºs }}}.
   Proof.
-    intros ???; apply ownP_lift_atomic_det_step_no_fork; eauto.
+    intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
     by destruct s; eauto using reducible_not_val.
   Qed.
 
   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' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs') â†’
+    (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs', head_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] âˆ§ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs') â†’
     â–· (WP e2 @ s; E {{ Î¦ }} âˆ— [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ {{ _, True }})
     âŠ¢ WP e1 @ s; E {{ Î¦ }}.
   Proof using Hinh.
@@ -280,7 +325,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' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ [] = efs') â†’
+    (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs', head_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] âˆ§ Ïƒ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 ebb8c9b0c663541bd460479580ebf7258ea00eb6..186b282e457d7f1196e06ee072695c6b5a568043 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, âŒœstep (t1,Ïƒ1) (t2,Ïƒ2)âŒ -âˆ—
-    state_interp Ïƒ1 ={âŠ¤}=âˆ— state_interp Ïƒ2 âˆ— twptp t2)%I.
+  (âˆ€ t2 Ïƒ1 Îº Îºs Ïƒ2, âŒœstep (t1,Ïƒ1) Îº (t2,Ïƒ2)âŒ -âˆ—
+    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 Ïƒ2) "Hstep HÏƒ". iMod ("Hwp" with "[$] [$]") as "[$ [$ ?]]".
   by iApply "H".
 Qed.
 
@@ -50,9 +50,9 @@ 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 (step_Permutation t1' t1 t2 Ïƒ1 Ïƒ2) as (t2'&?&?); try done.
-  iMod ("IH" $! t2' with "[% //] HÏƒ") as "[$ [IH _]]". by iApply "IH".
+  rewrite twptp_unfold /twptp_pre. iIntros (t2 Ïƒ1 Îº Îº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.
 
 Lemma twptp_app t1 t2 : twptp t1 -âˆ— twptp t2 -âˆ— twptp (t1 ++ t2).
@@ -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".
+  rewrite twptp_unfold /twptp_pre. iIntros (t1'' Ïƒ1 Îº Îº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 _]]".
+    + iMod ("IH2" with "[%] HÏƒ1") as "($ & $ & IH2 & _)".
       { by eapply step_atomic with (t1:=[]). }
       iModIntro. rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
       by setoid_rewrite (right_id_L [] (++)).
-    + iMod ("IH1" with "[%] HÏƒ1") as "[$ [IH1 _]]"; first by econstructor.
+    + iMod ("IH1" with "[%] HÏƒ1") as "($ & $ & IH1 & _)"; first by 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 econstructor.
+  - iMod ("IH2" with "[%] HÏƒ1") as "($ & $ & IH2 & _)"; first by econstructor.
     iModIntro. rewrite -assoc. by iApply "IH2".
 Qed.
 
@@ -84,46 +84,47 @@ 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".
+  rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' Ïƒ1' Îº Îº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. }
   iMod ("IH" with "HÏƒ1") as "[_ IH]".
-  iMod ("IH" with "[% //]") as "[$ [[IH _] IHfork]]"; iModIntro.
+  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 Ïƒ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 Ïƒ := (wsat âˆ— ownE âŠ¤ âˆ— state_interp Ïƒ [])%I.
 
-Lemma twptp_total Ïƒ t : world Ïƒ -âˆ— twptp t -âˆ— â–· âŒœsn step (t, Ïƒ)âŒ.
+Lemma twptp_total Ïƒ t : world Ïƒ -âˆ— 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).
+  iApply (pure_mono _ _ (Acc_intro _)). iIntros ([t' Ïƒ'] [Îº Hstep]).
   rewrite /twptp_pre uPred_fupd_eq /uPred_fupd_def.
-  iMod ("IH" with "[% //] HÏƒ [$Hw $HE]") as ">(Hw & HE & HÏƒ & [IH _])".
+  iMod ("IH" with "[% //] HÏƒ [$Hw $HE]") as ">(Hw & HE & % & HÏƒ & [IH _])".
   iApply "IH". by iFrame.
 Qed.
+
 End adequacy.
 
 Theorem twp_total Î£ Î› `{invPreG Î£} s e Ïƒ Î¦ :
   (âˆ€ `{Hinv : invG Î£},
-     (|={âŠ¤}=> âˆƒ stateI : state Î› â†’ iProp Î£,
-       let _ : irisG Î› Î£ := IrisG _ _ Hinv stateI in
-       stateI Ïƒ âˆ— WP e @ s; âŠ¤ [{ Î¦ }])%I) â†’
-  sn step ([e], Ïƒ). (* i.e. ([e], Ïƒ) is strongly normalizing *)
+     (|={âŠ¤}=> âˆƒ stateI : state Î› â†’ list (observation Î›) -> iProp Î£,
+       let _ : irisG Î› Î£ := IrisG _ _ _ Hinv stateI in
+       stateI Ïƒ [] âˆ— WP e @ s; âŠ¤ [{ Î¦ }])%I) â†’
+  sn erased_step ([e], Ïƒ). (* i.e. ([e], Ïƒ) is strongly normalizing *)
 Proof.
   intros Hwp.
   eapply (soundness (M:=iResUR Î£) _ 1); iIntros "/=".
   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 e5d1af45e6fc89383ef3199de3dda66078d0532e..5e774884896c003c777117f3618ccbe19613769f 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -10,74 +10,75 @@ Implicit Types P : iProp Î£.
 Implicit Types Î¦ : val Î› â†’ iProp Î£.
 Implicit Types v : val Î›.
 Implicit Types e : expr Î›.
-Hint Resolve head_prim_reducible head_reducible_prim_step.
+Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step head_reducible_no_obs_reducible.
 
 Lemma twp_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 @ s; E [{ Î¦ }] âˆ— [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ [{ _, True }])
+  (âˆ€ Ïƒ1 Îºs, state_interp Ïƒ1 Îºs ={E,âˆ…}=âˆ—
+    âŒœhead_reducible_no_obs e1 Ïƒ1âŒ âˆ—
+    âˆ€ Îº e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={âˆ…,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 (Îº 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 â†’ Ïƒ1 = Ïƒ2) â†’
-  (|={E}=> âˆ€ e2 efs Ïƒ, âŒœhead_step e1 Ïƒ e2 Ïƒ efsâŒ â†’
+  (âˆ€ Ïƒ1, head_reducible_no_obs e1 Ïƒ1) â†’
+  (âˆ€ Ïƒ1 Îº e2 Ïƒ2 efs, head_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ Îº = [] âˆ§ Ïƒ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 [{ Î¦ }].
 Proof using Hinh.
   iIntros (??) ">H". iApply twp_lift_pure_step; eauto.
-  iIntros "!>" (????). iApply "H"; eauto.
+  iIntros "!>" (?????). iApply "H"; eauto.
 Qed.
 
 Lemma twp_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 âˆ—
+  (âˆ€ Ïƒ1 Îºs, state_interp Ïƒ1 Îºs ={E}=âˆ—
+    âŒœhead_reducible_no_obs e1 Ïƒ1âŒ âˆ—
+    âˆ€ Îº e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={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"; auto.
+  iIntros (Ïƒ1 Îºs) "HÏƒ1". iMod ("H" $! Ïƒ1 with "HÏƒ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct s; auto. iIntros (Îº 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}=âˆ—
-    âŒœ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))
+  (âˆ€ Ïƒ1 Îºs, state_interp Ïƒ1 Îºs ={E}=âˆ—
+    âŒœhead_reducible_no_obs e1 Ïƒ1âŒ âˆ—
+    âˆ€ Îº e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={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 (Îº v2 Ïƒ2 efs Hstep).
+  iMod ("H" 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' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs') â†’
+  (âˆ€ Ïƒ1, head_reducible_no_obs e1 Ïƒ1) â†’
+  (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs',
+    head_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] âˆ§ Ïƒ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.
+Proof using Hinh. eauto 10 using twp_lift_pure_det_step. Qed.
 
 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' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ [] = efs') â†’
+  (âˆ€ Ïƒ1, head_reducible_no_obs e1 Ïƒ1) â†’
+  (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs',
+    head_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] âˆ§ Ïƒ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 c5aaca8fe274da8ea86f474bf45d20300887cda1..dc6f8e3ecd6ecaabbc4d359b7001401b4f6197ea 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -13,59 +13,61 @@ Implicit Types Î¦ : val Î› â†’ iProp Î£.
 
 Lemma twp_lift_step s E Î¦ e1 :
   to_val e1 = 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 e2 @ s; E [{ Î¦ }] âˆ— [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ [{ _, True }])
+  (âˆ€ Ïƒ1 Îºs, state_interp Ïƒ1 Îºs ={E,âˆ…}=âˆ—
+    âŒœif s is NotStuck then reducible_no_obs e1 Ïƒ1 else TrueâŒ âˆ—
+    âˆ€ Îº e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={âˆ…,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 â†’ Ïƒ1 = Ïƒ2) â†’
-  (|={E}=> âˆ€ e2 efs Ïƒ, âŒœprim_step e1 Ïƒ e2 Ïƒ efsâŒ â†’
+  (âˆ€ Ïƒ1, reducible_no_obs e1 Ïƒ1) â†’
+  (âˆ€ Ïƒ1 Îº e2 Ïƒ2 efs, prim_step e1 Ïƒ1 Îº e2 Ïƒ2 efs â†’ Îº = [] /\ Ïƒ1 = Ïƒ2) â†’
+  (|={E}=> âˆ€ Îº e2 efs Ïƒ, âŒœprim_step e1 Ïƒ Îº e2 Ïƒ efsâŒ â†’
     WP e2 @ s; E [{ Î¦ }] âˆ— [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ [{ _, True }])
   âŠ¢ WP e1 @ s; E [{ Î¦ }].
 Proof.
   iIntros (Hsafe Hstep) "H". iApply twp_lift_step.
-  { eapply reducible_not_val, (Hsafe inhabitant). }
-  iIntros (Ïƒ1) "HÏƒ". iMod "H".
+  { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
+  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 ?).
-  destruct (Hstep Ïƒ1 e2 Ïƒ2 efs); auto; subst.
-  iMod "Hclose" as "_". iFrame "HÏƒ". iApply "H"; auto.
+  iSplit; [by destruct s|]. iIntros (Îº e2 Ïƒ2 efs Hstep').
+  destruct (Hstep Ïƒ1 Îº e2 Ïƒ2 efs); auto; subst.
+  iMod "Hclose" as "_". iModIntro. iSplit; first done.
+  iFrame "HÏƒ". iApply "H"; auto.
 Qed.
 
 (* Atomic steps don't need any mask-changing business here, one can
    use the generic lemmas here. *)
 Lemma twp_lift_atomic_step {s E Î¦} e1 :
   to_val e1 = 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 âˆ—
+  (âˆ€ Ïƒ1 Îºs, state_interp Ïƒ1 Îºs ={E}=âˆ—
+    âŒœif s is NotStuck then reducible_no_obs e1 Ïƒ1 else TrueâŒ âˆ—
+    âˆ€ Îº e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={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 "!>" (Îº e2 Ïƒ2 efs) "%". iMod "Hclose" as "_".
+  iMod ("H" $! Îº 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.
 
 Lemma twp_lift_pure_det_step `{Inhabited (state Î›)} {s E Î¦} e1 e2 efs :
-  (âˆ€ Ïƒ1, reducible e1 Ïƒ1) â†’
-  (âˆ€ Ïƒ1 e2' Ïƒ2 efs', prim_step e1 Ïƒ1 e2' Ïƒ2 efs' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs')â†’
+  (âˆ€ Ïƒ1, reducible_no_obs e1 Ïƒ1) â†’
+  (âˆ€ Ïƒ1 Îº e2' Ïƒ2 efs', prim_step e1 Ïƒ1 Îº e2' Ïƒ2 efs' â†’ Îº = [] /\ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs')â†’
   (|={E}=> WP e2 @ s; E [{ Î¦ }] âˆ— [âˆ— list] ef âˆˆ efs, WP ef @ s; âŠ¤ [{ _, True }])
   âŠ¢ WP e1 @ s; E [{ Î¦ }].
 Proof.
   iIntros (? Hpuredet) ">H". iApply (twp_lift_pure_step _ E); try done.
-  { by intros; eapply Hpuredet. }
-  by iIntros "!>" (e' efs' Ïƒ (_&->&->)%Hpuredet).
+  { by naive_solver. }
+  by iIntros "!>" (Îº e' efs' Ïƒ (->&_&->&->)%Hpuredet).
 Qed.
 
 Lemma twp_pure_step `{Inhabited (state Î›)} s E e1 e2 Ï† n Î¦ :
@@ -78,4 +80,5 @@ Proof.
   iApply twp_lift_pure_det_step; [done|naive_solver|].
   iModIntro. rewrite /= right_id. by iApply "IH".
 Qed.
+
 End lifting.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 9e8cf93ef64db490eef628c30a2c05887a4ef101..aa53b6716e1768554a86cb7a6d301e9def1ada62 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -9,11 +9,11 @@ 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 Î¦ âˆ—
-       [âˆ— list] ef âˆˆ efs, wp âŠ¤ ef (Î» _, True)
+  | None => âˆ€ Ïƒ1 Îºs,
+     state_interp Ïƒ1 Îºs ={E,âˆ…}=âˆ— âŒœif s is NotStuck then reducible_no_obs e1 Ïƒ1 else TrueâŒ âˆ—
+     âˆ€ Îº e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={âˆ…,E}=âˆ—
+       âŒœÎº = []âŒ âˆ— state_interp Ïƒ2 Îºs âˆ—
+       wp E e2 Î¦ âˆ— [âˆ— list] ef âˆˆ efs, wp âŠ¤ ef (Î» _, True)
   end%I.
 
 Lemma twp_pre_mono `{irisG Î› Î£} s
@@ -23,9 +23,10 @@ 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".
-  iMod ("Hwp" with "Hstep") as "($ & Hwp & Hfork)"; iModIntro; iSplitL "Hwp".
+  iIntros (Ïƒ1 Îºs) "HÏƒ". iMod ("Hwp" with "HÏƒ") as "($ & Hwp)"; iModIntro.
+  iIntros (Îº 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".
     by iApply "H".
@@ -44,7 +45,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 16 (f_equiv || done). by apply Hwp, pair_ne.
+    rewrite /uncurry3 /twp_pre. do 22 (f_equiv || done). by apply pair_ne.
 Qed.
 
 Definition twp_def `{irisG Î› Î£} (s : stuckness) (E : coPset)
@@ -105,10 +106,10 @@ 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).
-  iMod ("IH" with "[//]") as "($ & IH & IHefs)"; auto.
+  iModIntro; iSplit; [by destruct s1, s2|]. iIntros (Îº 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Î¦").
   - iApply (big_sepL_impl with "[$IHefs]"); iIntros "!#" (k ef _) "[IH _]".
@@ -119,7 +120,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,15 +131,16 @@ 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).
-  iMod ("H" with "[//]") as "(Hphy & H & $)". destruct s.
+  iIntros (Ïƒ1 Îºs) "HÏƒ". iMod "H". iMod ("H" $! Ïƒ1 with "HÏƒ") as "[$ H]".
+  iModIntro. iIntros (Îº 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.
     + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
-      by edestruct (atomic _ _ _ _ Hstep).
-  - destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
-    iMod (twp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply twp_value'.
+      by edestruct (atomic _ _ _ _ _ Hstep).
+  - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
+    iMod (twp_value_inv' with "H") as ">H". iModIntro. iSplit; first done.
+    iFrame "Hphy". by iApply twp_value'.
 Qed.
 
 Lemma twp_bind K `{!LanguageCtx K} s E e Î¦ :
@@ -152,12 +154,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.
-  { iPureIntro. unfold reducible in *.
+  iIntros (Ïƒ1 Îºs) "HÏƒ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
+  { iPureIntro. unfold reducible_no_obs in *.
     destruct s; naive_solver eauto using fill_step. }
-  iIntros (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)".
+  iIntros (Îº 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)".
   iModIntro; iSplitR "IHfork".
   - iDestruct "IH" as "[IH _]". by iApply "IH".
   - by setoid_rewrite and_elim_r.
@@ -173,10 +175,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.
-  { 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 (Ïƒ1 Îºs) "HÏƒ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
+  { destruct s; eauto using reducible_no_obs_fill. }
+  iIntros (Îº e2 Ïƒ2 efs Hstep).
+  iMod ("IH" $! Îº (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 +188,9 @@ 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 "!>". iSplitR.
+  { destruct s; last done. eauto using reducible_no_obs_reducible. }
+  iIntros (e2 Ïƒ2 efs Hstep). iMod ("H" $! _ _ _ _ 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 023966eb01f2494650a7a9d950d22c994434681b..bcaa16f4499b3f75b59e1f69e489241fe00f6128 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 â†’ 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âŒ âˆ—
+        âˆ€ e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 Îº e2 Ïƒ2 efsâŒ ={âˆ…,âˆ…,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 18 (f_contractive || f_equiv). apply IH; first lia.
+  do 22 (f_contractive || f_equiv). apply IH; first lia.
   intros v. eapply dist_le; eauto with lia.
 Qed.
 Global Instance wp_proper s E e :
@@ -79,7 +79,7 @@ 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).
   iMod ("H" with "[//]") as "H". iIntros "!> !>". iMod "H" as "($ & H & Hefs)".
@@ -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,14 +104,14 @@ 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]".
+  iIntros (Ïƒ1 Îº Îºs) "HÏƒ". iMod "H". iMod ("H" $! Ïƒ1 with "HÏƒ") as "[$ H]".
   iModIntro. iIntros (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.
-    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
-      by edestruct (atomic _ _ _ _ Hstep).
-  - destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
+    + iMod ("H" $! _ [] with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
+      by edestruct (atomic _ _ _ _ _ Hstep).
+  - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
     iMod (wp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply wp_value'.
 Qed.
 
@@ -120,7 +120,7 @@ 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 (Ïƒ1 Îº Îºs) "HÏƒ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
   iIntros "!>" (e2 Ïƒ2 efs Hstep). iMod ("H" $! e2 Ïƒ2 efs with "[% //]") as "H".
   iIntros "!>!>". iMod "H" as "($ & H & $)".
   iMod "HR". iModIntro. iApply (wp_strong_mono s s E2 with "H"); [done..|].
@@ -134,11 +134,11 @@ 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).
-  destruct (fill_step_inv e Ïƒ1 e2 Ïƒ2 efs) as (e2'&->&?); auto.
+  destruct (fill_step_inv e Ïƒ1 Îº e2 Ïƒ2 efs) as (e2'&->&?); auto.
   iMod ("H" $! e2' Ïƒ2 efs with "[//]") as "H". iIntros "!>!>".
   iMod "H" as "($ & H & $)". by iApply "IH".
 Qed.
@@ -150,7 +150,7 @@ 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|].