From 4ec14182f7b176373965e50c8b8a06ca7f0be40c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 4 Oct 2018 17:01:59 +0200
Subject: [PATCH] tweak WP def.n and fix eauto in heap_lang

---
 theories/heap_lang/lang.v                 |  1 +
 theories/heap_lang/lifting.v              | 89 +++++++++--------------
 theories/program_logic/adequacy.v         |  6 +-
 theories/program_logic/ectx_lifting.v     | 66 ++++++++---------
 theories/program_logic/lifting.v          | 48 ++++++------
 theories/program_logic/ownp.v             | 15 ++--
 theories/program_logic/total_weakestpre.v |  4 +-
 theories/program_logic/weakestpre.v       | 40 +++++-----
 8 files changed, 124 insertions(+), 145 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 2630b441e..7a7f28361 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -167,6 +167,7 @@ Definition val_is_unboxed (v : val) : Prop :=
 
 (** The state: heaps of vals. *)
 Definition state : Type := gmap loc val * gset proph.
+Implicit Type σ : state.
 
 (** Equality and other typeclass stuff *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 835ee9bc8..7d701ae81 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -48,11 +48,15 @@ Ltac inv_head_step :=
   end.
 
 Local Hint Extern 0 (atomic _ _) => solve_atomic.
-Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
-Local Hint Extern 0 (head_reducible_no_obs _ _) => 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_fresh.
 Local Hint Resolve to_of_val.
 
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
@@ -134,10 +138,8 @@ Lemma wp_alloc s E e v :
   {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
   iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
-  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
-  { iPureIntro. repeat eexists. by apply alloc_fresh. }
-  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
+  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Φ".
 Qed.
@@ -146,9 +148,7 @@ 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 κs) "[Hσ Hκs] !>"; iSplit.
-  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
-  { iPureIntro. repeat eexists. by apply alloc_fresh. }
+  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=> //. iSplit; first done. iFrame. by iApply "HΦ".
@@ -158,9 +158,8 @@ 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 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto.
-  iNext; iIntros (κ κs' 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 :
@@ -168,8 +167,7 @@ Lemma twp_load s E l q v :
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   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.
+  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
@@ -179,11 +177,8 @@ Lemma wp_store s E l v' e v :
 Proof.
   iIntros (<- Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit.
-  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
-  { iPureIntro. repeat eexists. constructor; eauto. }
-  iNext; iIntros (κ κs' 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.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
@@ -194,10 +189,7 @@ Proof.
   iIntros (<- Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit.
-  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
-  { iPureIntro. repeat eexists. constructor; eauto. }
-  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
@@ -209,8 +201,8 @@ Lemma wp_cas_fail s E l q v' e1 v1 e2 :
 Proof.
   iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iNext; iIntros (κ κs' 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_cas_fail s E l q v' e1 v1 e2 :
@@ -232,11 +224,8 @@ Lemma wp_cas_suc s E l e1 v1 e2 v2 :
 Proof.
   iIntros (<- <- ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit.
-  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
-  { iPureIntro. repeat eexists. by econstructor. }
-  iNext; iIntros (κ κs' 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.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
@@ -248,10 +237,7 @@ Proof.
   iIntros (<- <- ? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit.
-  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
-  { iPureIntro. repeat eexists. by econstructor. }
-  iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
@@ -263,11 +249,8 @@ Lemma wp_faa s E l i1 e2 i2 :
 Proof.
   iIntros (<- Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit.
-  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
-  { iPureIntro. repeat eexists. by constructor. }
-  iNext; iIntros (κ κs' 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.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
@@ -279,10 +262,7 @@ Proof.
   iIntros (<- Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit.
-  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
-  { iPureIntro. repeat eexists. by constructor. }
-  iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
@@ -292,12 +272,10 @@ Lemma wp_new_proph :
   {{{ True }}} NewProph {{{ v (p : proph), RET (LitV (LitProphecy p)); 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.
-  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
-  { iPureIntro. repeat eexists. by apply new_proph_fresh. }
-  unfold cons_obs. simpl.
-  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]). inv_head_step.
-  iMod ((@proph_map_alloc _ _ _ _ _ _ _ p) with "HR") as "[HR Hp]".
+  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.
@@ -313,12 +291,11 @@ Lemma wp_resolve_proph e1 e2 p v w:
   {{{ 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.
-  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
-  { iPureIntro. repeat eexists. by constructor. }
   unfold cons_obs. simpl.
-  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step. iApply fupd_frame_l.
+  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Φ".
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index b5e3cf856..c48f569d6 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -78,8 +78,8 @@ Lemma wp_step s E e1 σ1 κ κs e2 σ2 efs Φ :
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
   rewrite (val_stuck e1 σ1 κ e2 σ2 efs) // uPred_fupd_eq.
-  iMod ("H" $! σ1 _ with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
-  iMod ("H" $! κ κs e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
+  iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
+  iMod ("H" $! e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
   iIntros "!> !>". by iMod ("H" with "[$Hw $HE]") as ">($ & $ & $)".
 Qed.
 
@@ -145,7 +145,7 @@ 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" $! _ None with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
   iIntros "!> !> !%". by right.
 Qed.
 
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index f1d2cdb24..6b24aa902 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -16,28 +16,28 @@ Hint Resolve head_stuck_stuck.
 
 Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
+  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,∅,E}▷=∗
-      state_interp σ2 κs' ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ∀ 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 κs) "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 (κ κs' e2 σ2 efs [Hstep ->]).
+  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 κs, state_interp σ1 κs ={E,∅}=∗
+  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
-      state_interp σ2 κs' ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ▷ ∀ 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 (??) "?".
-  iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (κ κs' e2 σ2 efs ?) "!> !>". by iApply "H".
+  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 :
@@ -76,61 +76,61 @@ Qed.
 
 Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs, state_interp σ1 κs ={E1}=∗
+  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E1,E2}▷=∗
-      state_interp σ2 κs' ∗
+    ∀ 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 κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; auto. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
+  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 κs, state_interp σ1 κs ={E}=∗
+  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
-      state_interp σ2 κs' ∗
+    ▷ ∀ 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 κs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; auto. iNext. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
+  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 κs, state_interp σ1 κs ={E1}=∗
+  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E1,E2}▷=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 κs' ∗ from_option Φ False (to_val e2))
+    ∀ 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 κs) "Hσ1". iMod ("H" $! σ1 κs with "Hσ1") as "[$ H]"; iModIntro.
-  iIntros (κ κs' v2 σ2 efs [Hstep ->]).
-  iMod ("H" $! κ κs' v2 σ2 efs with "[# //]") as "H".
+  iIntros (σ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 κs, state_interp σ1 κs ={E}=∗
+  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 κs' ∗ from_option Φ False (to_val e2))
+    ▷ ∀ 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 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
-  iNext; iIntros (κ κs' v2 σ2 efs Hstep).
-  iMod ("H" $! κ κs' v2 σ2 efs with "[# //]") as "(% & $ & $)". subst; auto.
+  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 :
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 493da34c5..42d4b7272 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -15,15 +15,15 @@ Hint Resolve reducible_no_obs_reducible.
 
 Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
+  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,∅,E}▷=∗
-      state_interp σ2 κs' ∗ WP 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 κs) "Hσ".
+  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.
+  iIntros (????). iApply "H". eauto.
 Qed.
 
 Lemma wp_lift_stuck E Φ e :
@@ -31,21 +31,21 @@ Lemma wp_lift_stuck E Φ e :
   (∀ σ κs, state_interp σ κs ={E,∅}=∗ ⌜stuck e σ⌝)
   ⊢ WP e @ E ?{{ Φ }}.
 Proof.
-  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κs) "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 κs, state_interp σ1 κs ={E,∅}=∗
+  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
-      state_interp σ2 κs' ∗ WP 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.
 
@@ -59,10 +59,10 @@ Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
   { specialize (Hsafe inhabitant). destruct s; last done.
       by eapply reducible_not_val. }
-  iIntros (σ1 κs) "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 (κ κs' e2 σ2 efs [Hstep' ->]).
+  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.
@@ -82,18 +82,18 @@ Qed.
    use the generic lemmas here. *)
 Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs, state_interp σ1 κs ={E1}=∗
+  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E1,E2}▷=∗
-      state_interp σ2 κs' ∗
+    ∀ 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 κs) "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 "!>" (κ  κs' e2 σ2 efs ?). iMod "Hclose" as "_".
-  iMod ("H" $! κ κs' e2 σ2 efs with "[#]") as "H"; [done|].
+  iIntros "!>" (e2 σ2 efs ?). iMod "Hclose" as "_".
+  iMod ("H" $! e2 σ2 efs with "[#]") as "H"; [done|].
   iMod (fupd_intro_mask' E2 ∅) as "Hclose"; [set_solver|]. iIntros "!> !>".
   iMod "Hclose" as "_". iMod "H" as "($ & HΦ & $)".
   destruct (to_val e2) eqn:?; last by iExFalso.
@@ -102,16 +102,16 @@ Qed.
 
 Lemma wp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κs, state_interp σ1 κs ={E}=∗
+  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
-      state_interp σ2 κs' ∗
+    ▷ ∀ 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 ([Hstep ->]) "!> !>".
+  iIntros (???) "?". iMod ("H" with "[$]") as "[$ H]".
+  iIntros "!> *". iIntros (Hstep) "!> !>".
   by iApply "H".
 Qed.
 
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 0038df660..27d605146 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -128,17 +128,18 @@ Section lifting.
       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 κ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 (κ κs'' e2 σ2 efs [Hstep ->]).
+    - 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).
       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)). }
+         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 _))). }
+        by apply: (exclusive_local_update _ (Excl (κs:leibnizC _))). }
       iFrame "Hσ Hκs". iApply ("H" with "[]"); eauto with iFrame.
   Qed.
 
@@ -165,8 +166,8 @@ Section lifting.
     iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
     { specialize (Hsafe inhabitant). destruct s; last done.
       by eapply reducible_not_val. }
-    iIntros (σ1 κs) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-    iModIntro; iSplit; [by destruct s|]; iNext; iIntros (κ κs' e2 σ2 efs [??]).
+    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.
     by iMod "Hclose"; iModIntro; iFrame; iApply "H".
   Qed.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 0921d0b5a..6b47d468a 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -188,9 +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 κs) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
+  iIntros (σ1 κ κs) "Hσ". iMod ("H" with "Hσ") as "[% H]". iIntros "!>". iSplitR.
   { destruct s; last done. eauto using reducible_no_obs_reducible. }
-  iIntros (κ κs' e2 σ2 efs [Hstep ->]). iMod ("H" $! _ _ _ _ Hstep) as "(% & Hst & H & Hfork)".
+  iIntros (e2 σ2 efs Hstep). iMod ("H" $! _ _ _ _ Hstep) as "(% & Hst & H & Hfork)".
   subst κ. iFrame "Hst".
   iApply step_fupd_intro; [set_solver+|]. iNext.
   iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]").
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index dd29e8dbd..7ba7ec99e 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -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 κs,
-      state_interp σ1 κs ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-      ∀ κ (κs' : list (observation Λ)) e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,∅,E}▷=∗
-      state_interp σ2 κs' ∗ wp E e2 Φ ∗
-      [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
+  | None => ∀ σ1 κ κs,
+      state_interp σ1 (cons_obs κ κ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 24 (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,9 +79,9 @@ Proof.
   rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 κs) "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 (κ κs' e2 σ2 efs Hstep).
+  iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "H". iIntros "!> !>". iMod "H" as "($ & H & Hefs)".
   iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
   - iApply ("IH" with "[//] H HΦ").
@@ -93,7 +93,7 @@ Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ }}
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
-  iIntros (σ1 κs) "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,12 +104,12 @@ Proof.
   iIntros "H". rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
-  iIntros (σ1 κs) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
-  iModIntro. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
+  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 %(? & ? & ? & ? & ?).
+    + iMod ("H" $! _ None 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'.
@@ -120,8 +120,8 @@ Lemma wp_step_fupd s E1 E2 e P Φ :
   (|={E1,E2}▷=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; E1 {{ Φ }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
-  iIntros (σ1 κs) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
-  iIntros "!>" (κ κs' e2 σ2 efs Hstep). iMod ("H" $! κ κs' e2 σ2 efs with "[% //]") as "H".
+  iIntros (σ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..|].
   iIntros (v) "H". by iApply "H".
@@ -134,12 +134,12 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by iApply fupd_wp. }
   rewrite wp_unfold /wp_pre fill_not_val //.
-  iIntros (σ1 κs) "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 (κ κs' e2 σ2 efs [Hstep ->]).
+  iIntros (e2 σ2 efs Hstep).
   destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
-  iMod ("H" $! κ κs' e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
+  iMod ("H" $! e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
   iMod "H" as "($ & H & $)". by iApply "IH".
 Qed.
 
@@ -150,10 +150,10 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
   rewrite fill_not_val //.
-  iIntros (σ1 κs) "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 (κ κs' e2 σ2 efs [Hstep ->]).
-  iMod ("H" $! κ κs' (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
+  iIntros (e2 σ2 efs Hstep).
+  iMod ("H" $! (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
   iIntros "!>!>". iMod "H" as "($ & H & $)". by iApply "IH".
 Qed.
 
-- 
GitLab