diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 881e486cc2d0b59fc0da2ec654792352496b8ab6..186439910c6b4597a37d46727aaa9cd6cb197f7c 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -225,53 +225,53 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
   | _, _, _ => None
   end.
 
-Inductive head_step : expr → state → expr → state → option (expr) → Prop :=
+Inductive head_step : expr → state → 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' σ None
+     head_step (App (Rec f x e1) e2) σ e' σ []
   | UnOpS op l l' σ :
      un_op_eval op l = Some l' → 
-     head_step (UnOp op (Lit l)) σ (Lit l') σ None
+     head_step (UnOp op (Lit l)) σ (Lit l') σ []
   | BinOpS op l1 l2 l' σ :
      bin_op_eval op l1 l2 = Some l' → 
-     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
+     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ []
   | IfTrueS e1 e2 σ :
-     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
+     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
   | IfFalseS e1 e2 σ :
-     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
+     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 σ None
+     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 σ None
+     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) σ None
+     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) σ None
+     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
   | ForkS e σ:
-     head_step (Fork e) σ (Lit LitUnit) σ (Some 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]>σ) None
+     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
   | LoadS l v σ :
      σ !! l = Some v →
-     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ None
+     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]>σ) None
+     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) []
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some vl → vl ≠ v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ None
+     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 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) [].
 
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -294,11 +294,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_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
+Lemma val_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 ef :
-  head_step (fill_item Ki e) σ1 e2 σ2 ef → 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 :
@@ -313,7 +313,7 @@ Qed.
 
 Lemma alloc_fresh e v σ :
   let l := fresh (dom _ σ) in
-  to_val e = Some v → head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
+  to_val e = Some v → head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
 
 (** Closed expressions *)
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 6926c97bace4eeca96642454e1961ef153fb16a3..44a1dec2630e7d647a41161a2e31273a366e4606 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -10,7 +10,7 @@ Section lifting.
 Context `{irisG heap_lang Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
-Implicit Types ef : option expr.
+Implicit Types efs : list expr.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :
@@ -38,7 +38,7 @@ 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 σ None) ?right_id //;
+  intros. rewrite -(wp_lift_atomic_det_head_step σ v σ []) ?right_id //;
     last (by intros; inv_head_step; eauto using to_of_val). solve_atomic.
 Qed.
 
@@ -48,7 +48,7 @@ Lemma wp_store_pst E σ l v v' Φ :
   ⊢ WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
 Proof.
   intros ?.
-  rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
+  rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) [])
     ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
@@ -58,7 +58,7 @@ Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
   ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
   intros ??.
-  rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
+  rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ [])
     ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
@@ -68,7 +68,7 @@ Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
   ⊢ 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]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto).
+    (<[l:=v2]>σ) []) ?right_id //; last (by intros; inv_head_step; eauto).
   solve_atomic.
 Qed.
 
@@ -76,9 +76,9 @@ Qed.
 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) (Some e)) //=;
+  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=;
     last by intros; inv_head_step; eauto.
-  rewrite later_sep -(wp_value_pvs _ _ (Lit _)) //.
+  by rewrite later_sep -(wp_value_pvs _ _ (Lit _)) // right_id.
 Qed.
 
 Lemma wp_rec E f x erec e1 e2 Φ :
@@ -88,7 +88,7 @@ Lemma wp_rec E f x erec e1 e2 Φ :
   ▷ 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)) None) //= ?right_id;
+    (subst' x e2 (subst' f (Rec f x erec) erec)) []) //= ?right_id;
     intros; inv_head_step; eauto.
 Qed.
 
@@ -96,7 +96,7 @@ Lemma wp_un_op E op l l' Φ :
   un_op_eval op l = Some l' →
   ▷ (|={E}=> Φ (LitV l')) ⊢ WP UnOp op (Lit l) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
+  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
@@ -104,21 +104,21 @@ Lemma wp_bin_op E op l1 l2 l' Φ :
   bin_op_eval op l1 l2 = Some l' →
   ▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
 Proof.
-  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
+  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') [])
     ?right_id -?wp_value_pvs //; 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 None)
+  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 [])
     ?right_id //; 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 None)
+  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 [])
     ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
@@ -126,7 +126,7 @@ 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 None)
+  intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
@@ -134,7 +134,7 @@ 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 None)
+  intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
@@ -143,7 +143,7 @@ Lemma wp_case_inl E e0 e1 e2 Φ :
   ▷ 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) None) ?right_id //; intros; inv_head_step; eauto.
+    (App e1 e0) []) ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_case_inr E e0 e1 e2 Φ :
@@ -151,6 +151,6 @@ Lemma wp_case_inr E e0 e1 e2 Φ :
   ▷ 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) None) ?right_id //; intros; inv_head_step; eauto.
+    (App e2 e0) []) ?right_id //; intros; inv_head_step; eauto.
 Qed.
 End lifting.
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index dbe50971a7de1be0598f64ece4dc4490c5799e76..7118b4af2fb2cda83003b4384c9a18dff2c5ebe9 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -312,7 +312,7 @@ Tactic Notation "do_head_step" tactic3(tac) :=
   try match goal with |- head_reducible _ _ => eexists _, _, _ end;
   simpl;
   match goal with
-  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
+  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?efs =>
      first [apply alloc_fresh|econstructor];
        (* solve [to_val] side-conditions *)
        first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 688a02079f3b055c43780b1a2dbc7a40f984f0e2..b7d729a87dbf07ab59c644ba47c2426c5abe8bbd 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -20,11 +20,11 @@ Proof.
   intros Had ?.
   destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
   apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
-  destruct (adequate_safe e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&ef&?)];
+  destruct (adequate_safe 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'' ++ option_list ef), σ3; econstructor; eauto.
+  right; exists (t2' ++ e3 :: t2'' ++ efs), σ3; econstructor; eauto.
 Qed.
 
 Section adequacy.
@@ -42,19 +42,17 @@ 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.
-Lemma wptp_fork ef : wptp (option_list ef) ⊣⊢ wp_fork ef.
-Proof. destruct ef; by rewrite /wptp /= ?right_id. Qed.
 
-Lemma wp_step e1 σ1 e2 σ2 ef Φ :
-  prim_step e1 σ1 e2 σ2 ef →
-  world σ1 ★ WP e1 {{ Φ }} =r=> ▷ |=r=> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wp_fork ef).
+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).
 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. }
   rewrite pvs_eq /pvs_def.
   iVs ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
   iVsIntro; iNext.
-  iVs ("H" $! e2 σ2 ef with "[%] [Hw HE]")
+  iVs ("H" $! e2 σ2 efs with "[%] [Hw HE]")
     as ">($ & $ & $ & $)"; try iFrame; eauto.
 Qed.
 
@@ -64,11 +62,11 @@ Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
   =r=> ∃ e2 t2', t2 = e2 :: t2' ★ ▷ |=r=> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp t2').
 Proof.
   iIntros (Hstep) "(HW & He & Ht)".
-  destruct Hstep as [e1' σ1' e2' σ2' ef [|? t1'] t2' ?? Hstep]; simplify_eq/=.
-  - iExists e2', (t2' ++ option_list ef); iSplitR; first eauto.
-    rewrite wptp_app wptp_fork. iFrame "Ht". iApply wp_step; try iFrame; eauto.
-  - iExists e, (t1' ++ e2' :: t2' ++ option_list ef); iSplitR; first eauto.
-    rewrite !wptp_app !wptp_cons wptp_app wptp_fork.
+  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.
+  - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
+    rewrite !wptp_app !wptp_cons wptp_app.
     iDestruct "Ht" as "($ & He' & $)"; iFrame "He".
     iApply wp_step; try iFrame; eauto.
 Qed.
diff --git a/program_logic/ectx_language.v b/program_logic/ectx_language.v
index d7b58df92eac2bd6fbc9ce115420f19454bfd68b..28657bbaeef74d8fde127f87f0c3df8fe2bae3fa 100644
--- a/program_logic/ectx_language.v
+++ b/program_logic/ectx_language.v
@@ -11,11 +11,11 @@ Class EctxLanguage (expr val ectx state : Type) := {
   empty_ectx : ectx;
   comp_ectx : ectx → ectx → ectx;
   fill : ectx → expr → expr;
-  head_step : expr → state → expr → state → option expr → Prop;
+  head_step : expr → state → expr → state → list expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
-  val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None;
+  val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
 
   fill_empty e : fill empty_ectx e = e;
   fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
@@ -28,10 +28,10 @@ Class EctxLanguage (expr val ectx state : Type) := {
   ectx_positive K1 K2 :
     comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx;
 
-  step_by_val K K' e1 e1' σ1 e2 σ2 ef :
+  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 ef →
+    head_step e1' σ1 e2 σ2 efs →
     exists K'', K' = comp_ectx K K'';
 }.
 
@@ -57,16 +57,16 @@ Section ectx_language.
   Implicit Types (e : expr) (K : ectx).
 
   Definition head_reducible (e : expr) (σ : state) :=
-    ∃ e' σ' ef, head_step e σ e' σ' ef.
+    ∃ e' σ' efs, head_step e σ e' σ' efs.
 
   Inductive prim_step (e1 : expr) (σ1 : state)
-      (e2 : expr) (σ2 : state) (ef : option expr) : Prop :=
+      (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 ef → prim_step e1 σ1 e2 σ2 ef.
+      head_step e1' σ1 e2' σ2 efs → prim_step e1 σ1 e2 σ2 efs.
 
-  Lemma val_prim_stuck e1 σ1 e2 σ2 ef :
-    prim_step e1 σ1 e2 σ2 ef → to_val e1 = None.
+  Lemma val_prim_stuck e1 σ1 e2 σ2 efs :
+    prim_step e1 σ1 e2 σ2 efs → to_val e1 = None.
   Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.
 
   Canonical Structure ectx_lang : language := {|
@@ -78,29 +78,29 @@ Section ectx_language.
   |}.
 
   (* Some lemmas about this language *)
-  Lemma head_prim_step e1 σ1 e2 σ2 ef :
-    head_step e1 σ1 e2 σ2 ef → prim_step e1 σ1 e2 σ2 ef.
+  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_prim_reducible e σ : head_reducible e σ → reducible e σ.
-  Proof. intros (e'&σ'&ef&?). eexists e', σ', ef. by apply head_prim_step. Qed.
+  Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
 
   Lemma ectx_language_atomic e :
-    (∀ σ e' σ' ef, head_step e σ e' σ' ef → is_Some (to_val e')) →
+    (∀ σ e' σ' efs, head_step e σ e' σ' efs → is_Some (to_val e')) →
     (∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx) →
     atomic e.
   Proof.
-    intros Hatomic_step Hatomic_fill σ e' σ' ef [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_stuck.
     rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
   Qed.
 
-  Lemma head_reducible_prim_step e1 σ1 e2 σ2 ef :
-    head_reducible e1 σ1 → prim_step e1 σ1 e2 σ2 ef →
-    head_step e1 σ1 e2 σ2 ef.
+  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.
   Proof.
-    intros (e2''&σ2''&ef''&?) [K e1' e2' -> -> Hstep].
-    destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 e2'' σ2'' ef'')
+    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_stuck.
     by rewrite !fill_empty.
@@ -114,7 +114,7 @@ Section ectx_language.
     - 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 ef) as [K' ->]; eauto.
+      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.
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index d298f34b219caf202f24e7bebbbc444f9b5a9df1..cff6e639645aadd5e153db00174185e585733062 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -19,21 +19,21 @@ Proof. apply: weakestpre.wp_bind. Qed.
 Lemma wp_lift_head_step E Φ e1 :
   to_val e1 = None →
   (|={E,∅}=> ∃ σ1, ■ head_reducible e1 σ1 ★ ▷ ownP σ1 ★
-     ▷ ∀ e2 σ2 ef, ■ head_step e1 σ1 e2 σ2 ef ★ ownP σ2
-          ={∅,E}=★ WP e2 @ E {{ Φ }} ★ wp_fork ef)
+    ▷ ∀ e2 σ2 efs, ■ head_step e1 σ1 e2 σ2 efs ★ ownP σ2
+          ={∅,E}=★ WP e2 @ E {{ Φ }} ★ wp_fork efs)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply (wp_lift_step E); try done.
   iVs "H" as (σ1) "(%&Hσ1&Hwp)". iVsIntro. iExists σ1.
-  iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 ef) "[% ?]".
+  iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "[% ?]".
   iApply "Hwp". by eauto.
 Qed.
 
 Lemma wp_lift_pure_head_step E Φ e1 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → σ1 = σ2) →
-  (▷ ∀ e2 ef σ, ■ head_step e1 σ e2 σ ef → WP e2 @ E {{ Φ }} ★ wp_fork ef)
+  (∀ σ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)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (???) "H". iApply wp_lift_pure_step; eauto. iNext.
@@ -43,26 +43,26 @@ Qed.
 Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
   atomic e1 →
   head_reducible e1 σ1 →
-  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef,
-  ■ head_step e1 σ1 (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs,
+  ■ head_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork efs)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
   iIntros (???) "[% ?]". iApply "H". eauto.
 Qed.
 
-Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
+Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
   atomic e1 →
   head_reducible e1 σ1 →
-  (∀ e2' σ2' ef', head_step e1 σ1 e2' σ2' ef' →
-    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
-  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+  (∀ 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 {{ Φ }}.
 Proof. eauto using wp_lift_atomic_det_step. Qed.
 
-Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 ef :
+Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 e2' σ2 ef', head_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
-  ▷ (WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+  (∀ σ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 {{ Φ }}.
 Proof. eauto using wp_lift_pure_det_step. Qed.
 End wp.
diff --git a/program_logic/ectxi_language.v b/program_logic/ectxi_language.v
index 4a8f62fd85863f80c4946907b42602a29e98fc3d..cbc159d2dbebcd221087794cb87a4c7f2deb8afa 100644
--- a/program_logic/ectxi_language.v
+++ b/program_logic/ectxi_language.v
@@ -9,11 +9,11 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
   of_val : val → expr;
   to_val : expr → option val;
   fill_item : ectx_item → expr → expr;
-  head_step : expr → state → expr → state → option expr → Prop;
+  head_step : expr → state → expr → state → list expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
-  val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None;
+  val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
 
   fill_item_inj Ki :> Inj (=) (=) (fill_item Ki);
   fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
@@ -21,8 +21,8 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
     to_val e1 = None → to_val e2 = None →
     fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2;
 
-  head_ctx_step_val Ki e σ1 e2 σ2 ef :
-    head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e);
+  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);
 }.
 
 Arguments of_val {_ _ _ _ _} _.
@@ -60,8 +60,8 @@ Section ectxi_language.
   (* When something does a step, and another decomposition of the same expression
   has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
   other words, [e] also contains the reducible expression *)
-  Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
-    fill K e1 = fill K' e1' → to_val e1 = None → head_step e1' σ1 e2 σ2 ef →
+  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 →
     exists K'', K' = K ++ K''. (* K `prefix_of` K' *)
   Proof.
     intros Hfill Hred Hnval; revert K' Hfill.
diff --git a/program_logic/language.v b/program_logic/language.v
index 33600f6dfce705774c1a66d601f6bfcb7c46e4ae..04bba2a4a4dc635d74a676aebd8b8f650c327afe 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -6,10 +6,10 @@ Structure language := Language {
   state : Type;
   of_val : val → expr;
   to_val : expr → option val;
-  prim_step : expr → state → expr → state → option expr → Prop;
+  prim_step : expr → state → expr → state → list expr → Prop;
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
-  val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None
+  val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs → to_val e = None
 }.
 Arguments of_val {_} _.
 Arguments to_val {_} _.
@@ -29,31 +29,31 @@ Section language.
   Implicit Types v : val Λ.
 
   Definition reducible (e : expr Λ) (σ : state Λ) :=
-    ∃ e' σ' ef, prim_step e σ e' σ' ef.
+    ∃ e' σ' efs, prim_step e σ e' σ' efs.
   Definition atomic (e : expr Λ) : Prop :=
-    ∀ σ e' σ' ef, prim_step e σ e' σ' ef → is_Some (to_val e').
+    ∀ σ e' σ' efs, prim_step e σ e' σ' efs → is_Some (to_val e').
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
-    | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
+    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
-       ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
-       prim_step e1 σ1 e2 σ2 ef →
+       ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) →
+       prim_step e1 σ1 e2 σ2 efs →
        step ρ1 ρ2.
 
   Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
   Proof. intros <-. by rewrite to_of_val. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
-  Global Instance: Inj (=) (=) (@of_val Λ).
+  Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 End language.
 
 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 ef :
-    prim_step e1 σ1 e2 σ2 ef →
-    prim_step (K e1) σ1 (K e2) σ2 ef;
-  fill_step_inv e1' σ1 e2 σ2 ef :
-    to_val e1' = None → prim_step (K e1') σ1 e2 σ2 ef →
-    ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 ef
+  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
 }.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 6fd4ecc6b6d390eab610602f999a1819ab18e1cd..12584487babb9284de89af4a80f59d601c839a03 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -13,14 +13,14 @@ Implicit Types Φ : val Λ → iProp Σ.
 Lemma wp_lift_step E Φ e1 :
   to_val e1 = None →
   (|={E,∅}=> ∃ σ1, ■ reducible e1 σ1 ★ ▷ ownP σ1 ★
-     ▷ ∀ e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ★ ownP σ2
-          ={∅,E}=★ WP e2 @ E {{ Φ }} ★ wp_fork ef)
+    ▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ★ ownP σ2
+          ={∅,E}=★ WP e2 @ E {{ Φ }} ★ wp_fork efs)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
   iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
   iDestruct (ownP_agree σ1 σ1' with "[#]") as %<-; first by iFrame.
-  iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 ef Hstep).
+  iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
   iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
   iApply "H"; eauto.
 Qed.
@@ -28,14 +28,14 @@ Qed.
 Lemma wp_lift_pure_step E Φ e1 :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
-  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2) →
-  (▷ ∀ e2 ef σ, ■ prim_step e1 σ e2 σ ef → WP e2 @ E {{ Φ }} ★ wp_fork ef)
+  (∀ σ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)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
   iIntros (σ1) "Hσ". iApply pvs_intro'; [set_solver|iIntros "Hclose"].
-  iSplit; [done|]; iNext; iIntros (e2 σ2 ef ?).
-  destruct (Hstep σ1 e2 σ2 ef); auto; subst.
+  iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+  destruct (Hstep σ1 e2 σ2 efs); auto; subst.
   iVs "Hclose"; iVsIntro. iFrame "Hσ". iApply "H"; auto.
 Qed.
 
@@ -43,39 +43,39 @@ Qed.
 Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
   atomic e1 →
   reducible e1 σ1 →
-  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 ef,
-    ■ prim_step e1 σ1 (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs,
+    ■ prim_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork efs)
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
   iIntros (Hatomic ?) "[Hσ H]".
   iApply (wp_lift_step E _ e1); eauto using reducible_not_val.
   iApply pvs_intro'; [set_solver|iIntros "Hclose"].
   iExists σ1. iFrame "Hσ"; iSplit; eauto.
-  iNext; iIntros (e2 σ2 ef) "[% Hσ]".
-  edestruct (Hatomic σ1 e2 σ2 ef) as [v2 <-%of_to_val]; eauto.
-  iDestruct ("H" $! v2 σ2 ef with "[Hσ]") as "[HΦ $]"; first by eauto.
+  iNext; iIntros (e2 σ2 efs) "[% Hσ]".
+  edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
+  iDestruct ("H" $! v2 σ2 efs with "[Hσ]") as "[HΦ $]"; first by eauto.
   iVs "Hclose". iVs "HΦ". iApply wp_value; auto using to_of_val.
 Qed.
 
-Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
+Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
   atomic e1 →
   reducible e1 σ1 →
-  (∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' →
-                  σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
-  ▷ ownP σ1 ★ ▷ (ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+  (∀ 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 {{ Φ }}.
 Proof.
   iIntros (?? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
-  iFrame. iNext. iIntros (v2' σ2' ef') "[% Hσ2']".
+  iFrame. iNext. iIntros (v2' σ2' efs') "[% Hσ2']".
   edestruct Hdet as (->&->%of_to_val%(inj of_val)&->). done. by iApply "Hσ2".
 Qed.
 
-Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
+Lemma wp_lift_pure_det_step {E Φ} e1 e2 efs :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
-  (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
-  ▷ (WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+  (∀ σ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 {{ Φ }}.
 Proof.
   iIntros (?? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
-  by intros; eapply Hpuredet. iNext. by iIntros (e' ef' σ (_&->&->)%Hpuredet).
+  by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 End lifting.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index b1ddc167952b3c1ba765f977c90648876109500c..3026e7e71e16e0f04f8f1d957b565270c67c9d90 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Export pviewshifts.
 From iris.program_logic Require Import ownership.
+From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics pviewshifts.
 Import uPred.
@@ -12,18 +13,18 @@ Definition wp_pre `{irisG Λ Σ}
   (* step case *)
   (to_val e1 = None ∧ ∀ σ1,
      ownP_auth σ1 ={E,∅}=★ ■ reducible e1 σ1 ★
-     ▷ ∀ e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ={∅,E}=★
+     ▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ={∅,E}=★
        ownP_auth σ2 ★ wp E e2 Φ ★
-       from_option (flip (wp ⊤) (λ _, True)) True ef))%I.
+       [★] (flip (wp ⊤) (λ _, True) <$> efs)))%I.
 
 Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
 Proof.
   rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
   apply or_ne, and_ne, forall_ne; auto=> σ1; apply wand_ne; auto.
   apply pvs_ne, sep_ne, later_contractive; auto=> i ?.
-  apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> ef.
+  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.
-  destruct ef; first apply Hwp; auto.
+  eapply big_sep_ne, list_fmap_ext_ne=> ef. by apply Hwp.
 Qed.
 
 Definition wp_def `{irisG Λ Σ} :
@@ -49,7 +50,7 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
 
-Notation wp_fork ef := (from_option (flip (wp ⊤) (λ _, True)) True ef)%I.
+Notation wp_fork efs := ([★] (flip (wp ⊤) (λ _, True) <$> efs))%I.
 
 Section wp.
 Context `{irisG Λ Σ}.
@@ -99,8 +100,8 @@ Proof.
   iSplit; [done|]; iIntros (σ1) "Hσ".
   iApply (pvs_trans _ E1); iApply pvs_intro'; auto. iIntros "Hclose".
   iVs ("H" $! σ1 with "Hσ") as "[$ H]".
-  iVsIntro. iNext. iIntros (e2 σ2 ef Hstep).
-  iVs ("H" $! _ σ2 ef with "[#]") as "($ & H & $)"; auto.
+  iVsIntro. iNext. iIntros (e2 σ2 efs Hstep).
+  iVs ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
   iVs "Hclose" as "_". by iApply ("IH" with "HΦ").
 Qed.
 
@@ -127,9 +128,9 @@ Proof.
   iIntros (σ1) "Hσ". iVs "H" as "[H|[_ H]]".
   { iDestruct "H" as (v') "[% ?]"; simplify_eq. }
   iVs ("H" $! σ1 with "Hσ") as "[$ H]".
-  iVsIntro. iNext. iIntros (e2 σ2 ef Hstep).
+  iVsIntro. iNext. iIntros (e2 σ2 efs Hstep).
   destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
-  iVs ("H" $! _ σ2 ef with "[#]") as "($ & H & $)"; auto.
+  iVs ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
   iVs (wp_value_inv with "H") as "==> H". by iApply wp_value'.
 Qed.
 
@@ -141,8 +142,8 @@ Proof.
   { iDestruct "Hv" as (v) "[% Hv]"; simplify_eq. }
   iRight; iSplit; [done|]. iIntros (σ1) "Hσ".
   iVs "HR". iVs ("H" $! _ with "Hσ") as "[$ H]".
-  iVsIntro; iNext; iIntros (e2 σ2 ef Hstep).
-  iVs ("H" $! e2 σ2 ef with "[%]") as "($ & H & $)"; auto.
+  iVsIntro; iNext; iIntros (e2 σ2 efs Hstep).
+  iVs ("H" $! e2 σ2 efs with "[%]") as "($ & H & $)"; auto.
   iVs "HR". iVsIntro. iApply (wp_strong_mono E2 _ _ Φ); try iFrame; eauto.
 Qed.
 
@@ -157,9 +158,9 @@ Proof.
   iIntros (σ1) "Hσ". iVs ("H" $! _ with "Hσ") as "[% H]".
   iVsIntro; iSplit.
   { iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
-  iNext; iIntros (e2 σ2 ef Hstep).
-  destruct (fill_step_inv e σ1 e2 σ2 ef) as (e2'&->&?); auto.
-  iVs ("H" $! e2' σ2 ef with "[%]") as "($ & H & $)"; auto.
+  iNext; iIntros (e2 σ2 efs Hstep).
+  destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
+  iVs ("H" $! e2' σ2 efs with "[%]") as "($ & H & $)"; auto.
   by iApply "IH".
 Qed.
 
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 68707dfc5a460dec2e445a280d4403dc96821ebc..fecf44a345180c76daf1c3495833886b485e3d09 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -7,13 +7,13 @@ From iris.heap_lang Require Import proofmode notation.
 
 Section LangTests.
   Definition add : expr := #21 + #21.
-  Goal ∀ σ, head_step add σ (#42) σ None.
+  Goal ∀ σ, head_step add σ (#42) σ [].
   Proof. intros; do_head_step done. Qed.
   Definition rec_app : expr := (rec: "f" "x" := "f" "x") #0.
-  Goal ∀ σ, head_step rec_app σ rec_app σ None.
+  Goal ∀ σ, head_step rec_app σ rec_app σ [].
   Proof. intros. rewrite /rec_app. do_head_step done. Qed.
   Definition lam : expr := λ: "x", "x" + #21.
-  Goal ∀ σ, head_step (lam #21)%E σ add σ None.
+  Goal ∀ σ, head_step (lam #21)%E σ add σ [].
   Proof. intros. rewrite /lam. do_head_step done. Qed.
 End LangTests.