diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 2a39566e8f9fe5e7b45c3a8f41958d948a8bca69..2472bbd6f416ee4cb224daaae9aeca2497e6769f 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -18,7 +18,7 @@ Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
   iris_invG := heapG_invG;
   state_interp σ κs _ :=
     (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I;
-  fork_post := True%I;
+  fork_post _ := True%I;
 }.
 
 (** Override the notations so that scopes and coercions work out *)
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 4294e99404ad14ceb009740312b83366899a7bb2..8cfbfb39bd1d49f491d4d3909e6b21c29efffc7c 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -14,6 +14,6 @@ Proof.
   iModIntro.
   iExists
     (λ σ κs _, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I),
-    True%I; iFrame.
+    (λ _, True%I); iFrame.
   iApply (Hwp (HeapG _ _ _ _)).
 Qed.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 56bd99597fcff5344d60df54f4436dd031f06b0f..b448661ab9c05d8d98891cf58540f05f5c7d0cbd 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -39,7 +39,7 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
 
-Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, fork_post }})%I.
+Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ fork_post }})%I.
 
 Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
@@ -112,8 +112,8 @@ Lemma wptp_all_result φ κs' s n e1 t1 κs v2 vs2 σ1 σ2 :
   nsteps n (e1 :: t1, σ1) κs (of_val <$> v2 :: vs2, σ2) →
   state_interp σ1 (κs ++ κs') (length t1) -∗
   WP e1 @ s; ⊤ {{ v,
-    let m' := length vs2 in
-    state_interp σ2 κs' m' -∗ [∗] replicate m' fork_post ={⊤,∅}=∗ ⌜φ v ⌝ }} -∗
+    state_interp σ2 κs' (length vs2) -∗
+    ([∗ list] v ∈ vs2, fork_post v) ={⊤,∅}=∗ ⌜φ v ⌝ }} -∗
   wptp s t1
   ={⊤,∅}▷=∗^(S n) ⌜φ v2 ⌝.
 Proof.
@@ -122,7 +122,7 @@ Proof.
   iApply (step_fupdN_wand with "H").
   iDestruct 1 as (e2 t2' ?) "(Hσ & H & Hvs)"; simplify_eq/=.
   rewrite fmap_length. iMod (wp_value_inv' with "H") as "H".
-  iAssert ([∗] replicate (length vs2) fork_post)%I with "[> Hvs]" as "Hm".
+  iAssert ([∗ list] v ∈ vs2, fork_post v)%I with "[> Hvs]" as "Hm".
   { clear Hstep. iInduction vs2 as [|v vs] "IH"; csimpl; first by iFrame.
     iDestruct "Hvs" as "[Hv Hvs]".
     iMod (wp_value_inv' with "Hv") as "$". by iApply "IH". }
@@ -178,7 +178,7 @@ Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
   (∀ `{Hinv : invG Σ} κs,
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (fork_post : iProp Σ),
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        (* This could be strengthened so that φ also talks about the number 
        of forked-off threads *)
@@ -202,12 +202,12 @@ Qed.
 Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
   (∀ `{Hinv : invG Σ} κs,
      (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) True%I in
+       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) (λ _, True%I) in
        stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply (wp_strong_adequacy Σ _)=> Hinv κs.
-  iMod Hwp as (stateI) "[Hσ H]". iExists (λ σ κs _, stateI σ κs), True%I.
+  iMod Hwp as (stateI) "[Hσ H]". iExists (λ σ κs _, stateI σ κs), (λ _, True%I).
   iIntros "{$Hσ} !>".
   iApply (wp_wand with "H"). iIntros (v ? σ') "_".
   iIntros "_". by iApply fupd_mask_weaken.
@@ -217,11 +217,11 @@ Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
   (∀ `{Hinv : invG Σ} κs,
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (fork_post : iProp Σ),
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ v,
-         let m := length vs in
-         stateI σ2 [] m -∗ [∗] replicate m fork_post ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) →
+         stateI σ2 [] (length vs) -∗
+         ([∗ list] v ∈ vs, fork_post v) ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) →
   rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) →
   φ v.
 Proof.
@@ -237,7 +237,7 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ} κs κs',
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (fork_post : iProp Σ),
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        stateI σ1 (κs ++ κs') 0 ∗ WP e @ s; ⊤ {{ _, True }} ∗
        (stateI σ2 κs' (pred (length t2)) ={⊤,∅}=∗ ⌜φ⌝))%I) →
@@ -258,7 +258,7 @@ Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ} κs κs',
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (fork_post : iProp Σ),
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ _, True }} ∗
        (stateI σ2 κs' (pred (length t2)) -∗ ∃ E, |={⊤,E}=> ⌜φ⌝))%I) →
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 8272530755c9153a1254bc7254e4e97dfc4430ec..e27fe2059d7f54d586b631f33c95f75a7c835568 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -21,7 +21,7 @@ Lemma wp_lift_head_step_fupd {s E Φ} e1 :
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E {{ Φ }} ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs Qs) "Hσ".
@@ -37,7 +37,7 @@ Lemma wp_lift_head_step {s E Φ} e1 :
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E {{ Φ }} ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (????) "?".
@@ -72,7 +72,7 @@ Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
@@ -88,7 +88,7 @@ Lemma wp_lift_atomic_head_step {s E Φ} e1 :
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 30f3a36a74a9716b5b5cd27bf4f513e9091afa48..59068a5f290d13b0462ccb1587521efc5e2ef427 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -20,7 +20,7 @@ Lemma wp_lift_step_fupd s E Φ e1 :
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E {{ Φ }} ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs n) "Hσ".
@@ -46,7 +46,7 @@ Lemma wp_lift_step s E Φ e1 :
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E {{ Φ }} ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (????) "Hσ".
@@ -89,7 +89,7 @@ Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H".
@@ -111,7 +111,7 @@ Lemma wp_lift_atomic_step {s E Φ} e1 :
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 8e707f1028b5d833919fd56dee9ada8391317734..def044befacb837fd4211eeffcbd8100de7e3a67 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -14,7 +14,7 @@ Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
 Instance ownPG_irisG `{ownPG Λ Σ} : irisG Λ Σ := {
   iris_invG := ownP_invG;
   state_interp σ κs _ := own ownP_name (● (Excl' σ))%I;
-  fork_post := True%I;
+  fork_post _ := True%I;
 }.
 Global Opaque iris_invG.
 
@@ -60,7 +60,7 @@ Proof.
   intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
   iIntros (? κs κs').
   iMod (own_alloc (● (Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]"; first done.
-  iExists (λ σ κs' _, own γσ (● (Excl' σ)))%I, True%I.
+  iExists (λ σ κs' _, own γσ (● (Excl' σ)))%I, (λ _, True%I).
   iFrame "Hσ".
   iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
     first by rewrite /ownP; iFrame.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 4456805b1e079192ecc961e078e41ce40c2ad618..c742a636dc8e7c288049abf01b5de88b3a77d2bc 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -118,7 +118,7 @@ Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
   (∀ `{Hinv : invG Σ},
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (fork_post : iProp Σ),
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        stateI σ [] 0 ∗ WP e @ s; ⊤ [{ Φ }])%I) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
index c9c02d3e416602747b611fb21c8d8be6cfa85a16..281737f38d25ed83e808fbefb7299e270c3e8365 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -21,7 +21,7 @@ Lemma twp_lift_head_step {s E Φ} e1 :
       ⌜κ = []⌝ ∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E [{ Φ }] ∗
-      [∗ list] i ↦ ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
+      [∗ list] i ↦ ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H".
@@ -49,7 +49,7 @@ Lemma twp_lift_atomic_head_step {s E Φ} e1 :
       ⌜κ = []⌝ ∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index f36e18e950823c77ca53f3a6e923107ec581c7e4..9a9da9bd854a4862005995f2a30e7cceebeed54c 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -21,7 +21,7 @@ Lemma twp_lift_step s E Φ e1 :
       ⌜κ = []⌝ ∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E [{ Φ }] ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
 
@@ -52,7 +52,7 @@ Lemma twp_lift_atomic_step {s E Φ} e1 :
       ⌜κ = []⌝ ∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H".
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 6892cc1fc966cf379baa68a769d5f52e8e5fa3ce..e3da620ff1bbb625249f07a2de1dcb7432f3b8e4 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -16,7 +16,7 @@ Definition twp_pre `{irisG Λ Σ} (s : stuckness)
          ⌜κ = []⌝ ∗
          state_interp σ2 κs (length efs + n) ∗
          wp E e2 Φ ∗
-         [∗ list] ef ∈ efs, wp ⊤ ef (λ _, fork_post)
+         [∗ list] ef ∈ efs, wp ⊤ ef fork_post
   end%I.
 
 Lemma twp_pre_mono `{irisG Λ Σ} s
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 6e5598aef95a214e1fef5cf3fbda575da05ef3e1..8cfeea29fd756affef44c8502ca562afa8cdf345 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -18,7 +18,7 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
   (** A fixed postcondition for any forked-off thread. For most languages, e.g.
   heap_lang, this will simply be [True]. However, it is useful if one wants to
   keep track of resources precisely, as in e.g. Iron. *)
-  fork_post : iProp Σ;
+  fork_post : val Λ → iProp Σ;
 }.
 Global Opaque iris_invG.
 
@@ -33,7 +33,7 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
        ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
          state_interp σ2 κs (length efs + n) ∗
          wp E e2 Φ ∗
-         [∗ list] i ↦ ef ∈ efs, wp ⊤ ef (λ _, fork_post)
+         [∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
   end%I.
 
 Local Instance wp_pre_contractive `{irisG Λ Σ} s : Contractive (wp_pre s).