diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index b61163b77ac4a583ebe3521d6d165d5ed122f83b..ecfe7a57488e51673d08e37fd679d35c348cbd01 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -53,14 +53,14 @@ Proof.
   iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
   match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
-  subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
+  subst v2. iSplit. iApply "HΦ"; by iSplit. by iApply big_sepL_nil.
 Qed.
 
 Lemma wp_load_pst E σ l v Φ :
   σ !! l = Some v →
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ v σ []) ?right_id; eauto 10.
+  intros. rewrite -(wp_lift_atomic_det_head_step' σ v σ); eauto 10.
   intros; inv_head_step; eauto 10.
 Qed.
 
@@ -69,8 +69,7 @@ Lemma wp_store_pst E σ l v v' Φ :
   ▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) ={E}=★ Φ (LitV LitUnit))
   ⊢ WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
 Proof.
-  intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) [])
-    ?right_id; eauto.
+  intros. rewrite-(wp_lift_atomic_det_head_step' σ (LitV LitUnit) (<[l:=v]>σ)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -79,8 +78,7 @@ Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ (LitV $ LitBool false))
   ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ [])
-    ?right_id; eauto.
+  intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool false) σ); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -89,8 +87,8 @@ Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
   ▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) ={E}=★ Φ (LitV $ LitBool true))
   ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
-    (<[l:=v2]>σ) []) ?right_id //; eauto 10.
+  intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
+    (<[l:=v2]>σ)); eauto 10.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -99,7 +97,7 @@ Lemma wp_fork E e Φ :
   ▷ (|={E}=> Φ (LitV LitUnit)) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite later_sep -(wp_value_pvs _ _ (Lit _)) // right_id.
+  - by rewrite later_sep -(wp_value_pvs _ _ (Lit _)) // big_sepL_singleton.
   - intros; inv_head_step; eauto.
 Qed.
 
@@ -109,8 +107,8 @@ Lemma wp_rec E f x erec e1 e2 Φ :
   Closed (f :b: x :b: []) erec →
   ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }} ⊢ WP App e1 e2 @ E {{ Φ }}.
 Proof.
-  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
-    (subst' x e2 (subst' f (Rec f x erec) erec)) []) //= ?right_id; eauto.
+  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step' (App _ _)
+    (subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -119,8 +117,8 @@ Lemma wp_un_op E op e v v' Φ :
   un_op_eval op v = Some v' →
   ▷ (|={E}=> Φ v') ⊢ WP UnOp op e @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (of_val v') [])
-    ?right_id -?wp_value_pvs'; eauto.
+  intros. rewrite -(wp_lift_pure_det_head_step' (UnOp op _) (of_val v'))
+    -?wp_value_pvs'; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -129,22 +127,22 @@ Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
   bin_op_eval op v1 v2 = Some v' →
   ▷ (|={E}=> Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (of_val v') [])
-    ?right_id -?wp_value_pvs'; eauto.
+  intros. rewrite -(wp_lift_pure_det_head_step' (BinOp op _ _) (of_val v'))
+    -?wp_value_pvs'; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_if_true E e1 e2 Φ :
   ▷ WP e1 @ E {{ Φ }} ⊢ WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 []) ?right_id; eauto.
+  rewrite -(wp_lift_pure_det_head_step' (If _ _ _) e1); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_if_false E e1 e2 Φ :
   ▷ WP e2 @ E {{ Φ }} ⊢ WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 []) ?right_id; eauto.
+  rewrite -(wp_lift_pure_det_head_step' (If _ _ _) e2); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -152,8 +150,8 @@ Lemma wp_fst E e1 v1 e2 Φ :
   to_val e1 = Some v1 → is_Some (to_val e2) →
   ▷ (|={E}=> Φ v1) ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
-  intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 [])
-    ?right_id -?wp_value_pvs; eauto.
+  intros ? [v2 ?].
+  rewrite -(wp_lift_pure_det_head_step' (Fst _) e1) -?wp_value_pvs; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -161,8 +159,8 @@ Lemma wp_snd E e1 e2 v2 Φ :
   is_Some (to_val e1) → to_val e2 = Some v2 →
   ▷ (|={E}=> Φ v2) ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
-  intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 [])
-    ?right_id -?wp_value_pvs; eauto.
+  intros [v1 ?] ?.
+  rewrite -(wp_lift_pure_det_head_step' (Snd _) e2) -?wp_value_pvs; eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -170,8 +168,8 @@ Lemma wp_case_inl E e0 e1 e2 Φ :
   is_Some (to_val e0) →
   ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
-    (App e1 e0) []) ?right_id; eauto.
+  intros [v0 ?].
+  rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (App e1 e0)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
@@ -179,8 +177,8 @@ Lemma wp_case_inr E e0 e1 e2 Φ :
   is_Some (to_val e0) →
   ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
-    (App e2 e0) []) ?right_id; eauto.
+  intros [v0 ?].
+  rewrite -(wp_lift_pure_det_head_step' (Case _ _ _) (App e2 e0)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 End lifting.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 566f87234730652d3ad9357be689d4c77fce7088..b2480ac7ed9d2e702f47e0b82cc2640da20b790b 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -36,16 +36,11 @@ Implicit Types Φs : list (val Λ → iProp Σ).
 
 Notation world σ := (wsat ★ ownE ⊤ ★ ownP_auth σ)%I.
 
-Definition wptp (t : list (expr Λ)) := ([★] (flip (wp ⊤) (λ _, True) <$> t))%I.
-
-Lemma wptp_cons e t : wptp (e :: t) ⊣⊢ WP e {{ _, True }} ★ wptp t.
-Proof. done. Qed.
-Lemma wptp_app t1 t2 : wptp (t1 ++ t2) ⊣⊢ wptp t1 ★ wptp t2.
-Proof. by rewrite /wptp fmap_app big_sep_app. Qed.
+Notation wptp t := ([★ list] ef ∈ t, WP ef {{ _, True }})%I.
 
 Lemma wp_step e1 σ1 e2 σ2 efs Φ :
   prim_step e1 σ1 e2 σ2 efs →
-  world σ1 ★ WP e1 {{ Φ }} =r=> ▷ |=r=> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wp_fork efs).
+  world σ1 ★ WP e1 {{ Φ }} =r=> ▷ |=r=> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp efs).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]".
   { iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. }
@@ -64,9 +59,9 @@ 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.
-    rewrite wptp_app. iFrame "Ht". iApply wp_step; try iFrame; eauto.
+    rewrite big_sepL_app. iFrame "Ht". iApply wp_step; try iFrame; eauto.
   - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
-    rewrite !wptp_app !wptp_cons wptp_app.
+    rewrite !big_sepL_app !big_sepL_cons big_sepL_app.
     iDestruct "Ht" as "($ & He' & $)"; iFrame "He".
     iApply wp_step; try iFrame; eauto.
 Qed.
@@ -123,8 +118,7 @@ Proof.
   intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
   iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq.
   apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H").
-  iApply wp_safe. iFrame "Hw".
-  iApply (big_sep_elem_of with "Htp"); apply elem_of_list_fmap; eauto.
+  iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp").
 Qed.
 
 Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ :
@@ -153,12 +147,12 @@ Proof.
     eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
     rewrite Nat_iter_S. iVs (iris_alloc σ) as (?) "(?&?&?&Hσ)".
     iVsIntro. iNext. iApply wptp_result; eauto.
-    iFrame. iSplitL; auto. by iApply Hwp.
+    iFrame. iSplitL. by iApply Hwp. by iApply big_sepL_nil.
   - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
     eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
     rewrite Nat_iter_S. iVs (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
     iVsIntro. iNext. iApply wptp_safe; eauto.
-    iFrame "Hw HE Hσ". iSplitL; auto. by iApply Hwp.
+    iFrame "Hw HE Hσ". iSplitL. by iApply Hwp. by iApply big_sepL_nil.
 Qed.
 
 Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ :
@@ -172,5 +166,5 @@ Proof.
   rewrite Nat_iter_S. iVs (iris_alloc σ1) as (?) "(Hw & HE & ? & Hσ)".
   rewrite pvs_eq in Hwp.
   iVs (Hwp _ with "Hσ [Hw HE]") as ">(? & ? & ? & ?)"; first by iFrame.
-  iVsIntro. iNext. iApply wptp_invariance; eauto. by iFrame.
+  iVsIntro. iNext. iApply wptp_invariance; eauto. iFrame. by iApply big_sepL_nil.
 Qed.
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index cff6e639645aadd5e153db00174185e585733062..0c35491a598320365077a68331d4ecbd3164f033 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -20,7 +20,7 @@ Lemma wp_lift_head_step E Φ e1 :
   to_val e1 = None →
   (|={E,∅}=> ∃ σ1, ■ head_reducible e1 σ1 ★ ▷ ownP σ1 ★
     ▷ ∀ e2 σ2 efs, ■ head_step e1 σ1 e2 σ2 efs ★ ownP σ2
-          ={∅,E}=★ WP e2 @ E {{ Φ }} ★ wp_fork efs)
+          ={∅,E}=★ WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply (wp_lift_step E); try done.
@@ -33,7 +33,8 @@ Lemma wp_lift_pure_head_step E Φ e1 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
-  (▷ ∀ e2 efs σ, ■ head_step e1 σ e2 σ efs → WP e2 @ E {{ Φ }} ★ wp_fork efs)
+  (▷ ∀ e2 efs σ, ■ head_step e1 σ e2 σ efs →
+    WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (???) "H". iApply wp_lift_pure_step; eauto. iNext.
@@ -44,7 +45,8 @@ Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
   atomic e1 →
   head_reducible e1 σ1 →
   ▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs,
-  ■ head_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork efs)
+  ■ head_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★
+    (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
@@ -56,13 +58,36 @@ Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 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 -★ (|={E}=> Φ v2) ★ wp_fork efs) ⊢ WP e1 @ E {{ Φ }}.
+  ▷ ownP σ1 ★ ▷ (ownP σ2 -★
+    (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+  ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_atomic_det_step. Qed.
 
+Lemma wp_lift_atomic_det_head_step' {E Φ e1} σ1 v2 σ2 :
+  atomic e1 →
+  head_reducible e1 σ1 →
+  (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
+    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
+  ▷ ownP σ1 ★ ▷ (ownP σ2 ={E}=★ Φ v2) ⊢ WP e1 @ E {{ Φ }}.
+Proof.
+  intros. rewrite -(wp_lift_atomic_det_head_step σ1 v2 σ2 [])
+    ?big_sepL_nil ?right_id; eauto.
+Qed.
+
 Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-  ▷ (WP e2 @ E {{ Φ }} ★ wp_fork efs) ⊢ WP e1 @ E {{ Φ }}.
+  (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+  ▷ (WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+  ⊢ WP e1 @ E {{ Φ }}.
 Proof. eauto using wp_lift_pure_det_step. Qed.
+
+Lemma wp_lift_pure_det_head_step' {E Φ} e1 e2 :
+  to_val e1 = None →
+  (∀ σ1, head_reducible e1 σ1) →
+  (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+  ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+Proof.
+  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
+Qed.
 End wp.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 12584487babb9284de89af4a80f59d601c839a03..1dcd9a8b070e1170939df6d504072b4e0e9efd20 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ownership.
+From iris.algebra Require Export upred_big_op.
 From iris.proofmode Require Import pviewshifts.
 
 Section lifting.
@@ -14,7 +15,7 @@ Lemma wp_lift_step E Φ e1 :
   to_val e1 = None →
   (|={E,∅}=> ∃ σ1, ■ reducible e1 σ1 ★ ▷ ownP σ1 ★
     ▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ★ ownP σ2
-          ={∅,E}=★ WP e2 @ E {{ Φ }} ★ wp_fork efs)
+          ={∅,E}=★ WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
@@ -29,7 +30,8 @@ Lemma wp_lift_pure_step E Φ e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
-  (▷ ∀ e2 efs σ, ■ prim_step e1 σ e2 σ efs → WP e2 @ E {{ Φ }} ★ wp_fork efs)
+  (▷ ∀ e2 efs σ, ■ prim_step e1 σ e2 σ efs →
+    WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
@@ -43,8 +45,8 @@ Qed.
 Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
   atomic e1 →
   reducible e1 σ1 →
-  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs,
-    ■ prim_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork efs)
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs, ■ prim_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★
+    (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (Hatomic ?) "[Hσ H]".
@@ -62,7 +64,9 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
   reducible e1 σ1 →
   (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
                    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
-  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork efs) ⊢ WP e1 @ E {{ Φ }}.
+  ▷ ownP σ1 ★ ▷ (ownP σ2 -★
+    (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+  ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (?? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
   iFrame. iNext. iIntros (v2' σ2' efs') "[% Hσ2']".
@@ -73,7 +77,8 @@ Lemma wp_lift_pure_det_step {E Φ} e1 e2 efs :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-  ▷ (WP e2 @ E {{ Φ }} ★ wp_fork efs) ⊢ WP e1 @ E {{ Φ }}.
+  ▷ (WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
+  ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (?? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
   by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 2e94c9ccd23e192a8bdc22aac665e5bd83f2e409..b805f323962d873e45ae20f90e88dd1d509fb4a5 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -15,7 +15,7 @@ Definition wp_pre `{irisG Λ Σ}
      ownP_auth σ1 ={E,∅}=★ ■ reducible e1 σ1 ★
      ▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ={∅,E}=★
        ownP_auth σ2 ★ wp E e2 Φ ★
-       [★] (flip (wp ⊤) (λ _, True) <$> efs)))%I.
+       [★ list] ef ∈ efs, wp ⊤ ef (λ _, True)))%I.
 
 Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
 Proof.
@@ -24,7 +24,7 @@ Proof.
   apply pvs_ne, sep_ne, later_contractive; auto=> i ?.
   apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> efs.
   apply wand_ne, pvs_ne, sep_ne, sep_ne; auto; first by apply Hwp.
-  eapply big_sep_ne, list_fmap_ext_ne=> ef. by apply Hwp.
+  apply big_sepL_ne=> ? ef. by apply Hwp.
 Qed.
 
 Definition wp_def `{irisG Λ Σ} :
@@ -50,8 +50,6 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
 
-Notation wp_fork efs := ([★] (flip (wp ⊤) (λ _, True) <$> efs))%I.
-
 Section wp.
 Context `{irisG Λ Σ}.
 Implicit Types P : iProp Σ.