diff --git a/theories/simplang/examples/data_races.v b/theories/simplang/examples/data_races.v
index 492e49fc93efcfdd59afdc219f17f287b798681d..73b21e483f7dc9c5eb58f2f4546fabc4332349d8 100644
--- a/theories/simplang/examples/data_races.v
+++ b/theories/simplang/examples/data_races.v
@@ -27,7 +27,7 @@ Section data_race.
     )%E.
 
   Lemma remove_store_and_load_sim π:
-    ⊢ sim_ectx val_rel π remove_store_and_load_opt remove_store_and_load val_rel.
+    ⊢ sim_ectx (const val_rel) π remove_store_and_load_opt remove_store_and_load val_rel.
   Proof.
     iIntros (v_t v_s) "Hrel". sim_pures.
 
@@ -75,7 +75,7 @@ Section data_race.
     )%E.
 
   Lemma reg_promote_loop_sim π f:
-    ⊢ sim_ectx val_rel π (reg_promote_loop_opt f) (reg_promote_loop f) val_rel.
+    ⊢ sim_ectx (const val_rel) π (reg_promote_loop_opt f) (reg_promote_loop f) val_rel.
   Proof.
     iIntros (v_t v_s) "Hrel". sim_pures.
 
@@ -119,7 +119,7 @@ Section data_race.
     )%E.
 
   Lemma hoist_load_sim π:
-    ⊢ sim_ectx val_rel π hoist_load_opt hoist_load val_rel.
+    ⊢ sim_ectx (const val_rel) π hoist_load_opt hoist_load val_rel.
   Proof.
     iIntros (v_t v_s) "Hrel". sim_pures.
 
diff --git a/theories/simplang/examples/heap_test.v b/theories/simplang/examples/heap_test.v
index 50177ef9a90d85de75d87b6da3f2224cbf65301f..7124f5d429b6631a7889b0277d3e7a57c9f7b0ed 100644
--- a/theories/simplang/examples/heap_test.v
+++ b/theories/simplang/examples/heap_test.v
@@ -8,7 +8,7 @@ From simuliris.simplang Require heap_bij.
 
 Module fix_bi.
 Section a.
-Context `{sheapGS Σ}.
+Context `{sheapGS Σ} (π : thread_id).
 Program Instance : sheapInv Σ := {|
   sheap_inv _ _ _ _ _ := ⌜True⌝%I;
 |}.
@@ -18,44 +18,46 @@ Proof. done. Qed.
 
 Definition val_rel (v1 v2 : val) : iProp Σ := (⌜v1 = v2⌝)%I.
 
-Lemma test_load l l2 π :
+Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
+Local Notation "et '⪯' es [{ Φ }]" := (et ⪯{π, const val_rel} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
+
+
+Lemma test_load l l2 :
   l ↦t #4 -∗ l2 ↦s #4 -∗
-  ((! #l)%E ⪯{π, val_rel} ! #l2 {{ val_rel }}).
+  ((! #l)%E ⪯ ! #l2 {{ val_rel }}).
 Proof.
   iIntros "H H1". target_load. source_load. sim_val. eauto.
 Qed.
 
-Lemma test_store l l2 π :
+Lemma test_store l l2 :
   l ↦t #4 -∗ l2 ↦s #4 -∗
-  ((#l <- #42)%E ⪯{π, val_rel} #l2 <- #1337 {{ val_rel }}).
+  ((#l <- #42)%E ⪯ #l2 <- #1337 {{ val_rel }}).
 Proof.
   iIntros "H H1". target_store. source_store. sim_val. eauto.
 Qed.
 
 (* FIXME: fix precedences for ⪯ to make the parantheses unnecessary *)
-Lemma test_alloc π :
-  ⊢ (Alloc #2 ;; #()) ⪯{π, val_rel} (Alloc #4;;#()) {{ val_rel }}.
+Lemma test_alloc :
+  ⊢ (Alloc #2 ;; #()) ⪯ (Alloc #4;;#()) {{ val_rel }}.
 Proof.
   target_alloc l1 as "H" "_".
   source_alloc l2 as "H2" "_".
-  (*to_sim. *)
-  (*target_pures. source_pures. *)
   sim_pures; sim_val.
   eauto.
 Qed.
 
-Lemma test_free l l2 π :
+Lemma test_free l l2 :
   l ↦t #42 -∗ l2 ↦s #1337 -∗ †l …t 1 -∗ †l2 …s 1 -∗
-  Free #l ⪯{π, val_rel} Free #l2 {{ val_rel }}.
+  Free #l ⪯ Free #l2 {{ val_rel }}.
 Proof.
   iIntros "H1 H2 H3 H4".
   target_free. source_free. sim_val. eauto.
 Qed.
 
 (* FIXME: if we remove the parantheses around the first element, parsing is broken *)
-Lemma test_freeN l l2 π :
+Lemma test_freeN l l2 :
   l ↦t∗ [(#42); #99] -∗ l2 ↦s∗ [(#1337); #420; #666] -∗ †l …t 2 -∗ †l2 …s 3 -∗
-  FreeN #2 #l ⪯{π, val_rel} FreeN #3 #l2 {{ val_rel }}.
+  FreeN #2 #l ⪯ FreeN #3 #l2 {{ val_rel }}.
 Proof.
   iIntros "H1 H2 H3 H4".
   target_free; first done. source_free; first done. sim_val. eauto.
@@ -65,48 +67,50 @@ End fix_bi.
 
 Module bij_test.
   Import heap_bij.
-  Context `{sbijG Σ}.
+  Context `{sbijG Σ} (π : thread_id).
+  Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
+  Local Notation "et '⪯' es [{ Φ }]" := (et ⪯{π, const val_rel} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
 
-  Lemma test_load l l2 π:
+  Lemma test_load l l2:
     l ↦t #4 -∗ l2 ↦s #4 -∗
-    ((! #l)%E ⪯{π, val_rel} ! #l2 {{ val_rel }}).
+    ((! #l)%E ⪯ ! #l2 {{ val_rel }}).
   Proof.
     iIntros "H H1". target_load. source_load. sim_val. eauto.
   Qed.
 
-  Lemma test_store l l2 π:
+  Lemma test_store l l2:
     l ↦t #4 -∗ l2 ↦s #4 -∗
-    ((#l <- #42)%E ⪯{π, val_rel} #l2 <- #1337 {{ val_rel }}).
+    ((#l <- #42)%E ⪯ #l2 <- #1337 {{ val_rel }}).
   Proof.
     iIntros "H H1". target_store. source_store. sim_val. eauto.
   Qed.
 
-  Lemma test_insert l l2 π:
+  Lemma test_insert l l2:
     l ↦t #4 -∗ l2 ↦s #4 -∗ †l …t 1 -∗ †l2 …s 1 -∗
-    ((#l <- #42)%E ⪯{π, val_rel} #l2 <- #42 {{ val_rel }}).
+    ((#l <- #42)%E ⪯ #l2 <- #42 {{ val_rel }}).
   Proof.
     iIntros "H H1 H2 H3".
     iApply (sim_bij_insert _ _ l l2 with "H2 H3 H H1 "); first done; iIntros "Hb".
     iApply (sim_bij_store with "Hb []"); first done. by sim_val.
   Qed.
 
-  Lemma test_bij_store (l_t l_s : loc) π :
+  Lemma test_bij_store (l_t l_s : loc) :
     l_t ↔h l_s -∗
-    (#l_t <- #42)%E ⪯{π, val_rel} (#l_s <- #42)%E {{ val_rel }}.
+    (#l_t <- #42)%E ⪯ (#l_s <- #42)%E {{ val_rel }}.
   Proof.
     iIntros "H". sim_store; first done. by sim_val.
   Qed.
 
-  Lemma test_bij_load (l_t l_s : loc) π:
+  Lemma test_bij_load (l_t l_s : loc):
     l_t ↔h l_s -∗
-    ! #l_t ⪯{π, val_rel} ! #l_s {{ val_rel }}.
+    ! #l_t ⪯ ! #l_s {{ val_rel }}.
   Proof.
     iIntros "H". sim_load v_t v_s as "Ha"; sim_val. done.
   Qed.
 
-  Lemma test_bij_free (l_t l_s : loc) π:
+  Lemma test_bij_free (l_t l_s : loc):
     l_t ↔h l_s -∗
-    Free #l_t ⪯{π, val_rel} Free #l_s {{ val_rel }}.
+    Free #l_t ⪯ Free #l_s {{ val_rel }}.
   Proof.
     iIntros "#H". sim_free; sim_val. done.
   Qed.
diff --git a/theories/simplang/examples/reorder_malloc.v b/theories/simplang/examples/reorder_malloc.v
index 948e330158168d8c9a2e32856dcbc2e2547c5690..c06694a7f306bcfb6a555db040d3fafce04fd5d0 100644
--- a/theories/simplang/examples/reorder_malloc.v
+++ b/theories/simplang/examples/reorder_malloc.v
@@ -41,7 +41,8 @@ Section reorder.
     iApply (sim_bij_insert with "Ha1_t Ha2_s Hl1_t Hl2_s Hv1"); iIntros "#Hbij_1".
     iApply (sim_bij_insert with "Ha2_t Ha1_s Hl2_t Hl1_s Hv2"); iIntros "#Hbij_2".
 
-    iApply sim_call; [done | done | simpl; by eauto ].
+    iApply sim_wand; [ iApply sim_call; [done | done | simpl; by eauto ] |].
+    iIntros (??) "$".
   Qed.
 
 End reorder.
diff --git a/theories/simplang/examples/sum.v b/theories/simplang/examples/sum.v
index 45063095761eed5e9957ed004e7aa09161810225..60edbc662c6594d5fc153b5fc88f236fa8e1b644 100644
--- a/theories/simplang/examples/sum.v
+++ b/theories/simplang/examples/sum.v
@@ -33,7 +33,7 @@ Inductive val_rel_pure : val → val → Prop :=
 Local Hint Constructors val_rel_pure : core.
 Definition val_rel v1 v2 : iProp Σ := (⌜val_rel_pure v1 v2⌝)%I.
 
-Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{π, val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
+Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
 
 Definition mul2_source :=
   (λ: "x",
@@ -84,6 +84,7 @@ Lemma client_sim (n : Z) :
 Proof.
   iIntros "Htarget Hsource Hinj1_t".
   target_call. target_call. source_call. sim_pures.
-  iApply sim_call; eauto.
+  iApply sim_wand; [ iApply sim_call; [done..|]; eauto |].
+  eauto.
 Qed.
 End fix_bi.
diff --git a/theories/simplang/examples/while.v b/theories/simplang/examples/while.v
index 37d9cc10c0f0c1c7c0c335d5fb28d520d6a91f5e..8ae37f56fdd92e2cc902dc3a2cac62d282782b2e 100644
--- a/theories/simplang/examples/while.v
+++ b/theories/simplang/examples/while.v
@@ -4,14 +4,17 @@ From simuliris.simulation Require Import slsls lifting.
 From simuliris.simplang Require Import log_rel.
 
 Section fix_bi.
-  Context `{sbijG Σ}.
+  Context `{sbijG Σ} (π : thread_id).
+  Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
+  Local Notation "et '⪯' es [{ Φ }]" := (et ⪯{π, const val_rel} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
+
 
   Definition loop_test n : expr :=
     let: "n" := Alloc #n in
     While (#0 < ! "n") ("n" <- ! "n" - #1).
 
-  Lemma loop (n : nat) π :
-    ⊢ loop_test n ⪯{π, val_rel} #() {{ val_rel }}.
+  Lemma loop (n : nat) :
+    ⊢ loop_test n ⪯ #() {{ val_rel }}.
   Proof.
     rewrite /loop_test.
     target_alloc l as "Hl" "_". sim_pures.
@@ -49,8 +52,8 @@ Section fix_bi.
       + by assert ((n0 - S n) * m + m = (n0 - n) * m)%Z as -> by lia.
   Qed.
 
-  Lemma mul_sim (n m : nat) π :
-    ⊢ mul_loop #n #m ⪯{π, val_rel} #n * #m {{ val_rel }}.
+  Lemma mul_sim (n m : nat) :
+    ⊢ mul_loop #n #m ⪯ #n * #m {{ val_rel }}.
   Proof.
     rewrite /mul_loop.
     sim_pures. target_alloc l_n as "Hln" "Ha_n". target_alloc l_acc as "Hlacc" "Ha_acc".
@@ -88,7 +91,7 @@ Section fix_bi.
     "rec" @s input_rec -∗
     log_rel input_loop (Call ##"rec" #true).
   Proof.
-    iIntros "#Hs". log_rel. iIntros "!#" (Ï€).
+    iIntros "#Hs". log_rel. iIntros "!#" (Ï€').
     rewrite /input_loop. target_alloc lc_t as "Hlc_t" "_". sim_pures.
     iApply (sim_while_rec _ _ _ _ _ _ (λ v_s, ∃ v_t, val_rel v_t v_s ∗ lc_t ↦t v_t)%I with "[Hlc_t] Hs").
     { iExists #true. eauto. }
@@ -108,7 +111,7 @@ Section fix_bi.
     "rec" @t input_rec -∗
     log_rel (Call ##"rec" #true) input_loop.
   Proof.
-    iIntros "#Hs". log_rel. iIntros "!#" (Ï€).
+    iIntros "#Hs". log_rel. iIntros "!#" (Ï€').
     rewrite /input_loop. source_alloc lc_s as "Hlc_s" "Ha_s". sim_pures.
     iApply (sim_rec_while _ _ _ _ _ _ (λ v_t, ∃ v_s, val_rel v_t v_s ∗ lc_s ↦s v_s)%I with "[Hlc_s] Hs").
     { iExists #true. eauto. }
diff --git a/theories/simplang/heap_bij.v b/theories/simplang/heap_bij.v
index c0940b0f0cb4835d4d918b007197b6fae513bfbf..a8432c5b3f3f838b1109b73d5a9a81ab68202721 100644
--- a/theories/simplang/heap_bij.v
+++ b/theories/simplang/heap_bij.v
@@ -253,8 +253,8 @@ Section fix_heap.
   Global Instance : sheapInvConst.
   Proof. done. Qed.
 
-  Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{π, val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
-  Local Notation "et '⪯' es [{ Φ }]" := (et ⪯{π, val_rel} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
+  Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
+  Local Notation "et '⪯' es [{ Φ }]" := (et ⪯{π, const val_rel} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
 
   Lemma sim_bij_load_sc l_t l_s Φ :
     l_t ↔h l_s -∗
@@ -633,7 +633,7 @@ Section sim.
 
   Import bi.
 
-  Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{π, val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
+  Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{π, const val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
 
   Implicit Types
     (K_t K_s : ectx)
@@ -652,10 +652,10 @@ Section sim.
     (∀ v_t v_s,
       match envs_app true (Esnoc Enil j (val_rel v_t v_s)) Δ with
       | Some Δ' =>
-          envs_entails Δ' (sim_expr val_rel Φ π (fill K_t (Val v_t)) (fill K_s (Val v_s)))
+          envs_entails Δ' (sim_expr (const val_rel) Φ π (fill K_t (Val v_t)) (fill K_s (Val v_s)))
       | None => False
       end) →
-    envs_entails Δ (sim_expr val_rel Φ π (fill K_t (Load o (LitV l_t))) (fill K_s (Load o (LitV l_s))))%I.
+    envs_entails Δ (sim_expr (const val_rel) Φ π (fill K_t (Load o (LitV l_t))) (fill K_s (Load o (LitV l_s))))%I.
   Proof using val_rel_pers.
     rewrite envs_entails_eq=> ? Hi.
     rewrite -sim_expr_bind. eapply wand_apply; first exact: sim_bij_load.
@@ -671,8 +671,8 @@ Section sim.
   Lemma tac_bij_store Δ i K_t K_s b l_t l_s v_t' v_s' o Φ :
     envs_lookup i Δ = Some (b, l_t ↔h l_s)%I →
     envs_entails Δ (val_rel v_t' v_s') →
-    envs_entails Δ (sim_expr val_rel Φ π (fill K_t (Val $ LitV LitUnit)) (fill K_s (Val $ LitV LitUnit))) →
-    envs_entails Δ (sim_expr val_rel Φ π (fill K_t (Store o (LitV l_t) (Val v_t'))) (fill K_s (Store o (LitV l_s) (Val v_s')))).
+    envs_entails Δ (sim_expr (const val_rel) Φ π (fill K_t (Val $ LitV LitUnit)) (fill K_s (Val $ LitV LitUnit))) →
+    envs_entails Δ (sim_expr (const val_rel) Φ π (fill K_t (Store o (LitV l_t) (Val v_t'))) (fill K_s (Store o (LitV l_s) (Val v_s')))).
   Proof using val_rel_pers.
     rewrite envs_entails_eq => HΔ.
     rewrite (persistent_persistently_2 (val_rel _ _)).
@@ -691,8 +691,8 @@ Section sim.
     *)
   Lemma tac_bij_freeN Δ i K_t K_s b l_t l_s n Φ :
     envs_lookup i Δ = Some (b, l_t ↔h l_s)%I →
-    envs_entails (envs_delete true i b Δ) (sim_expr val_rel Φ π (fill K_t (Val $ LitV LitUnit)) (fill K_s (Val $ LitV LitUnit))) →
-    envs_entails Δ (sim_expr val_rel Φ π (fill K_t (FreeN (Val $ LitV $ LitInt n) (LitV l_t))) (fill K_s (FreeN (Val $ LitV $ LitInt n) (LitV l_s)))).
+    envs_entails (envs_delete true i b Δ) (sim_expr (const val_rel) Φ π (fill K_t (Val $ LitV LitUnit)) (fill K_s (Val $ LitV LitUnit))) →
+    envs_entails Δ (sim_expr (const val_rel) Φ π (fill K_t (FreeN (Val $ LitV $ LitInt n) (LitV l_t))) (fill K_s (FreeN (Val $ LitV $ LitInt n) (LitV l_s)))).
   Proof using val_rel_pers.
     rewrite envs_entails_eq => Hl HΔ.
     rewrite -sim_expr_bind. rewrite (envs_lookup_sound _ _ _ _ Hl).
diff --git a/theories/simplang/heapbij_refl.v b/theories/simplang/heapbij_refl.v
index ff540612d9859300962a25c3356f07bff5c040bc..a70a818b35f6df51db2e6960577d34c84778cc29 100644
--- a/theories/simplang/heapbij_refl.v
+++ b/theories/simplang/heapbij_refl.v
@@ -145,7 +145,7 @@ Section refl.
     { iApply (subst_map_rel_weaken with "[$]"). set_solver. }
     iIntros (v_t2 v_s2) "#Hv2".
     discr_source; first by apply call_not_val. val_discr_source "Hv2".
-    iApply sim_call; done.
+    iApply sim_wand; [ by iApply sim_call|]. iIntros (??) "$".
   Qed.
 
   Lemma log_rel_unop e_t e_s o :
diff --git a/theories/simplang/log_rel.v b/theories/simplang/log_rel.v
index fe5d09df84706e1b464339eb73621fcc05b625f1..b6ff9a4c10243a13526e8c2395116d30e80caa84 100644
--- a/theories/simplang/log_rel.v
+++ b/theories/simplang/log_rel.v
@@ -65,12 +65,12 @@ Section open_rel.
   Definition log_rel e_t e_s : iProp Σ :=
     □ ∀ π (map : gmap string (val * val)),
       subst_map_rel (free_vars e_t ∪ free_vars e_s) map -∗
-      subst_map (fst <$> map) e_t ⪯{π, val_rel} subst_map (snd <$> map) e_s {{ val_rel }}.
+      subst_map (fst <$> map) e_t ⪯{π, const val_rel} subst_map (snd <$> map) e_s {{ val_rel }}.
 
   Lemma log_rel_closed e_t e_s :
     free_vars e_t = ∅ →
     free_vars e_s = ∅ →
-    log_rel e_t e_s ⊣⊢ (□ ∀ π, e_t ⪯{π, val_rel} e_s {{ val_rel }}).
+    log_rel e_t e_s ⊣⊢ (□ ∀ π, e_t ⪯{π, const val_rel} e_s {{ val_rel }}).
   Proof.
     intros Hclosed_t Hclosed_s. iSplit.
     - iIntros "#Hrel !#" (π). iSpecialize ("Hrel" $! π ∅).
diff --git a/theories/simplang/primitive_laws.v b/theories/simplang/primitive_laws.v
index 0e3509818469b1da1e90d0210f73b4f1edc26bba..efc581e20f32f0acfd53dcbbd04d90523348886c 100644
--- a/theories/simplang/primitive_laws.v
+++ b/theories/simplang/primitive_laws.v
@@ -115,7 +115,7 @@ Implicit Types l : loc.
 Implicit Types f : fname.
 Implicit Types π : thread_id.
 
-Context (Ω : val → val → iProp Σ) (π : thread_id).
+Context (Ω : thread_id → val → val → iProp Σ) (π : thread_id).
 Local Notation "et '⪯' es [{ Φ }]" := (et ⪯{π, Ω} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
 
 (** Program for target *)
@@ -432,7 +432,7 @@ Qed.
 Lemma sim_call e_t e_s v_t v_s f :
   to_val e_t = Some v_t →
   to_val e_s = Some v_s →
-  ⊢ Ω v_t v_s -∗ Call (## f) e_t ⪯{π, Ω} Call (## f) e_s {{ Ω }}.
+  ⊢ Ω π v_t v_s -∗ Call (## f) e_t ⪯{π, Ω} Call (## f) e_s {{ Ω π }}.
 Proof.
   intros <-%of_to_val <-%of_to_val.
   (* FIXME use lifting lemma for this *)
@@ -446,7 +446,7 @@ Qed.
 (** fork *)
 Lemma sim_fork e_t e_s Ψ `{!sheapInvConst} :
   #() ⪯ #() [{ Ψ }] -∗
-  (∀ π', e_t ⪯{π', Ω} e_s [{ lift_post Ω }]) -∗
+  (∀ π', e_t ⪯{π', Ω} e_s [{ lift_post (Ω π') }]) -∗
   Fork e_t ⪯ Fork e_s [{ Ψ }].
 Proof.
   iIntros "Hval Hsim". iApply sim_lift_head_step_both.
diff --git a/theories/simplang/proofmode.v b/theories/simplang/proofmode.v
index efff43e95c3630d823fcb5e0cff10b90e9d1d867..da5ab4239f18fc07b93776046003e699355ff99d 100644
--- a/theories/simplang/proofmode.v
+++ b/theories/simplang/proofmode.v
@@ -12,7 +12,7 @@ From iris.prelude Require Import options.
 
 Section sim.
 Context `{!sheapGS Σ} `{sheapInv Σ}.
-Context (Ω : val → val → iProp Σ) (π : thread_id).
+Context (Ω : thread_id → val → val → iProp Σ) (π : thread_id).
 Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{π, Ω} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.
 Local Notation "et '⪯' es [{ Φ }]" := (et ⪯{π, Ω} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.
 
diff --git a/theories/simulation/adequacy.v b/theories/simulation/adequacy.v
index 16bc012a74b3a662a165660b877c480e5921355e..d0dc1f0c2ae71507cc25db16ca9a0abac872d738 100644
--- a/theories/simulation/adequacy.v
+++ b/theories/simulation/adequacy.v
@@ -11,7 +11,7 @@ Section meta_level_simulation.
 
   Context {PROP : bi}.
   Context {Λ : language}.
-  Context (Ω : val Λ → val Λ → PROP).
+  Context (Ω : thread_id → val Λ → val Λ → PROP).
   Context {s : simulirisG PROP Λ}.
   Context {PROP_bupd : BiBUpd PROP}.
   Context {PROP_affine : BiAffine PROP}.
@@ -24,7 +24,7 @@ Section meta_level_simulation.
   (* we pull out the simulation to a meta-level simulation,
      the set V tracks which threads are already values in both target and source *)
   Definition msim (T_t: tpool Λ) (σ_t: state Λ)  (T_s: tpool Λ) (σ_s: state Λ) (V: gset nat) :=
-    sat (state_interp p_t σ_t p_s σ_s T_s ∗ ⌜∀ i, i ∈ V → ∃ v_t v_s, T_t !! i = Some (of_val v_t) ∧ T_s !! i = Some (of_val v_s)⌝ ∗ [∗ list] i↦e_t; e_s ∈ T_t;T_s, gsim_expr Ω (lift_post Ω) i e_t e_s).
+    sat (state_interp p_t σ_t p_s σ_s T_s ∗ ⌜∀ i, i ∈ V → ∃ v_t v_s, T_t !! i = Some (of_val v_t) ∧ T_s !! i = Some (of_val v_s)⌝ ∗ [∗ list] i↦e_t; e_s ∈ T_t;T_s, gsim_expr Ω (lift_post (Ω i)) i e_t e_s).
 
   Lemma msim_length T_t T_s σ_t σ_s V:
     msim T_t σ_t T_s σ_s V → length T_t = length T_s.
@@ -79,7 +79,7 @@ Section meta_level_simulation.
     ∃ v_t v_s,
       T_t !! i = Some (of_val v_t) ∧
       T_s !! i = Some (of_val v_s) ∧
-      sat (state_interp p_t σ_t p_s σ_s T_s ∗ Ω v_t v_s).
+      sat (state_interp p_t σ_t p_s σ_s T_s ∗ Ω i v_t v_s).
   Proof.
     intros Hel Hsafe Hsim. rewrite /msim in Hsim. eapply sat_mono in Hsim.
     - eapply sat_bupd in Hsim.
@@ -266,7 +266,7 @@ Section meta_level_simulation.
       pool_steps p_s T_s σ_s J T_s' σ_s' ∧
       msim T_t' σ_t' T_s' σ_s' U ∧
       (∀ i v_t, T_t' !! i = Some (of_val v_t) →
-      ∃ v_s, T_s' !! i = Some (of_val v_s) ∧ sat (state_interp p_t σ_t' p_s σ_s' T_s' ∗ Ω v_t v_s)).
+      ∃ v_s, T_s' !! i = Some (of_val v_s) ∧ sat (state_interp p_t σ_t' p_s σ_s' T_s' ∗ Ω i v_t v_s)).
   Proof.
     (* first we exectute the simulation to v_t *)
     intros Hsim Hstuck Htgt; eapply msim_steps in Hsim as (T_s' & σ_s' & J1 & Hsrc & Hsim); [|eauto..].
@@ -304,7 +304,7 @@ End meta_level_simulation.
 Section adequacy_statement.
   Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
   Context {Λ : language}.
-  Context (Ω : val Λ → val Λ → PROP).
+  Context (Ω : thread_id → val Λ → val Λ → PROP).
   Context {s : simulirisG PROP Λ}.
   Context {sat: PROP → Prop} {Sat: Satisfiable sat}.
   Arguments sat _%I.
@@ -320,9 +320,9 @@ Section adequacy_statement.
     sat (local_rel Ω p_t p_s ∗
       (∀ σ_t σ_s, ⌜I σ_t σ_s⌝ -∗ state_interp p_t σ_t p_s σ_s [of_call main u]) ∗
       progs_are p_t p_s ∗
-      Ω u u) →
+      Ω 0 u u) →
     (* post *)
-    (∀ v_t v_s σ_t σ_s T_s, sat (state_interp p_t σ_t p_s σ_s T_s ∗ Ω v_t v_s) → O v_t v_s) →
+    (∀ π v_t v_s σ_t σ_s T_s, sat (state_interp p_t σ_t p_s σ_s T_s ∗ Ω π v_t v_s) → O v_t v_s) →
     B p_t p_s.
   Proof.
     intros Hpre Hpost σ_t σ_s HI Hsafe.
@@ -352,7 +352,7 @@ Section adequacy_statement_alt.
 
   Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
   Context {Λ : language}.
-  Context (Ω : val Λ → val Λ → PROP).
+  Context (Ω : thread_id → val Λ → val Λ → PROP).
   Context {s : simulirisG PROP Λ}.
   Context {sat: PROP → Prop} {Sat: Satisfiable sat}.
   Arguments sat _%I.
@@ -373,16 +373,16 @@ Section adequacy_statement_alt.
       (* The programs are in the state *)
       progs_are p_t p_s ∗
       (* The "unit" argument to main is related *)
-      Ω u u ∗
+      Ω 0 u u ∗
       (* Logically related values are observationally related *)
-      ∀ v_s v_t, Ω v_t v_s -∗ ⌜O v_t v_s⌝) →
+      ∀ π v_s v_t, Ω π v_t v_s -∗ ⌜O v_t v_s⌝) →
     B p_t p_s.
   Proof.
     intros Hsat. eapply sat_frame_intro in Hsat; last first.
     { iIntros "(H1 & H2 & H3 & H4 & F)". iSplitL "F"; first iExact "F".
       iCombine "H1 H2 H3 H4" as "H". iExact "H". }
     eapply (@adequacy PROP _ _ _ _ _ _ (sat_frame _) _); first apply Hsat.
-    intros v_t v_s σ_t σ_s T_s Hsat_post. eapply sat_elim, sat_mono, Hsat_post.
+    intros π v_t v_s σ_t σ_s T_s Hsat_post. eapply sat_elim, sat_mono, Hsat_post.
     iIntros "(H & _ & Hval)". by iApply "H".
   Qed.
 
diff --git a/theories/simulation/fairness_adequacy.v b/theories/simulation/fairness_adequacy.v
index 182d8104d337584775e303e992aa1b8e9057d7f1..8d4560296ced055d9ed04851c7a01efd3f078482 100644
--- a/theories/simulation/fairness_adequacy.v
+++ b/theories/simulation/fairness_adequacy.v
@@ -25,7 +25,7 @@ Implicit Types
   (D: gmap nat nat)
   (i j k: nat)
   (σ_s σ_t σ : state Λ)
-  (Ω: val Λ → val Λ → PROP).
+  (Ω: thread_id → val Λ → val Λ → PROP).
 
 (* Language Setup *)
 Notation "P '.(tgt)'" := (P.*1) (at level 5).
@@ -184,7 +184,7 @@ Qed.
 *)
 
 
-Definition gsim_expr_all Ω π (P: list (expr Λ * expr Λ)) := ([∗ list] i↦p ∈ P, gsim_expr Ω (lift_post Ω) (π + i) (fst p) (snd p))%I.
+Definition gsim_expr_all Ω π (P: list (expr Λ * expr Λ)) := ([∗ list] i↦p ∈ P, gsim_expr Ω (lift_post (Ω (π + i))) (π + i) (fst p) (snd p))%I.
 Notation must_step_all Ω π := (must_step (gsim_expr_all Ω π)).
 
 
@@ -252,19 +252,19 @@ Proof.
 Qed.
 
 Definition gsim_expr_all_wo Ω π P O :=
-  ([∗ list] k ↦ p ∈ P, if (decide (k ∈ O)) then emp else gsim_expr Ω (lift_post Ω) (π + k) (fst p) (snd p))%I.
+  ([∗ list] k ↦ p ∈ P, if (decide (k ∈ O)) then emp else gsim_expr Ω (lift_post (Ω (π + k))) (π + k) (fst p) (snd p))%I.
 
 Lemma gsim_expr_all_to_wo Ω P π:
   gsim_expr_all Ω π P ≡ gsim_expr_all_wo Ω π P ∅.
 Proof.
   rewrite /gsim_expr_all /gsim_expr_all_wo. f_equiv.
-  intros k [e_t e_s]. destruct (decide (k ∈ ∅)); set_solver.
+  intros k [e_t e_s]. case_decide; set_solver.
 Qed.
 
 Lemma gsim_expr_all_wo_split Ω P O i e_t e_s π:
   P !! i = Some (e_t, e_s) →
   i ∉ O →
-  gsim_expr_all_wo Ω π P O ≡ (gsim_expr Ω (lift_post Ω) (π + i) e_t e_s ∗ gsim_expr_all_wo Ω π P (O ∪ {[i]}))%I.
+  gsim_expr_all_wo Ω π P O ≡ (gsim_expr Ω (lift_post (Ω (π + i))) (π + i) e_t e_s ∗ gsim_expr_all_wo Ω π P (O ∪ {[i]}))%I.
 Proof.
   intros Hlook Hel. rewrite /gsim_expr_all_wo.
   rewrite (big_sepL_delete _ _ i); last done.
@@ -299,7 +299,7 @@ Proof.
   intros Hlt; rewrite /gsim_expr_all_wo /gsim_expr_all.
   rewrite big_sepL_app. f_equiv. f_equiv.
   intros k [e_t e_s]; simpl.
-  destruct (decide) as [Hel|]; last done.
+  case_decide as Hel; last done.
   eapply Hlt in Hel.
   change (length P1 + k) with (length (P1: list (expr Λ * expr Λ)) + k) in Hel.
   lia.
@@ -318,8 +318,8 @@ Lemma gsim_expr_target_step_unfold Ω T i p_t p_s σ_t σ_s e_t e_s e_t' σ_t' e
   prim_step p_t e_t σ_t e_t' σ_t' efs_t →
   pool_safe p_s T σ_s →
   state_interp p_t σ_t p_s σ_s T -∗
-  gsim_expr Ω (lift_post Ω) i e_t e_s ==∗
-  ∃ e_s' σ_s' efs_s I, gsim_expr Ω (lift_post Ω) i e_t' e_s' ∗ state_interp p_t σ_t' p_s σ_s' (<[i := e_s']> T ++ efs_s) ∗
+  gsim_expr Ω (lift_post (Ω i)) i e_t e_s ==∗
+  ∃ e_s' σ_s' efs_s I, gsim_expr Ω (lift_post (Ω i)) i e_t' e_s' ∗ state_interp p_t σ_t' p_s σ_s' (<[i := e_s']> T ++ efs_s) ∗
       ⌜pool_steps p_s T σ_s I (<[i := e_s']> T ++ efs_s) σ_s'⌝ ∗ ⌜length efs_t = length efs_s⌝ ∗ gsim_expr_all Ω (length T) (zip efs_t efs_s).
 Proof.
   intros Hlook Hprim Hsafe. iIntros "SI Hsim". rewrite gsim_expr_unfold.
@@ -355,7 +355,7 @@ Proof.
   replace (∅ ∪ {[i]}: gset nat) with ({[i]}: gset nat) by set_solver.
   iDestruct "Hall" as "[Hsim Hall]".
   rewrite gsim_expr_eq global_greatest_def_unfold.
-  iApply (global_least_def_strong_ind _ (λ Ψ π e_t e_s, ∀ P D, ⌜P !! i = Some (e_t, e_s)⌝ -∗ ⌜i = π⌝ -∗ ⌜O ⊆ threads P.(tgt)⌝ -∗ gsim_expr_all_wo Ω 0 P {[i]} -∗ (∀ e_t e_s, Ψ e_t e_s -∗ lift_post Ω e_t e_s) -∗ must_step_all Ω 0 P O D)%I with "[] Hsim [] [] [] Hall"); eauto.
+  iApply (global_least_def_strong_ind _ (λ Ψ π e_t e_s, ∀ P D, ⌜P !! i = Some (e_t, e_s)⌝ -∗ ⌜i = π⌝ -∗ ⌜O ⊆ threads P.(tgt)⌝ -∗ gsim_expr_all_wo Ω 0 P {[i]} -∗ (∀ e_t e_s, Ψ e_t e_s -∗ lift_post (Ω i) e_t e_s) -∗ must_step_all Ω 0 P O D)%I with "[] Hsim [] [] [] Hall"); eauto.
   { intros n ?? Heq ???. repeat f_equiv. by apply Heq. }
   clear P D Hsub e_t e_s Hlook. iModIntro. iIntros (Ψ π e_t e_s) "Hsim".
   iIntros (P D Hlook ? Hsub) "Hall Hpost". subst π.
diff --git a/theories/simulation/global_sim.v b/theories/simulation/global_sim.v
index a354787e3c668446d432b782f125ce9765e6cd5d..908e22b9af2b7f8e3910aeff73e3d5d6362032cd 100644
--- a/theories/simulation/global_sim.v
+++ b/theories/simulation/global_sim.v
@@ -33,7 +33,7 @@ Section fix_lang.
   (** Global simulation relation with stuttering *)
 
   Section sim_def.
-  Context (val_rel : val Λ → val Λ → PROP).
+  Context (val_rel : thread_id → val Λ → val Λ → PROP).
   Definition gsim_expr_inner (greatest_rec : expr_rel -d> thread_id -d> expr_rel) (least_rec : expr_rel -d> thread_id -d> expr_rel) : expr_rel -d> thread_id -d> expr_rel :=
     λ Φ π e_t e_s,
     (∀ P_t σ_t P_s σ_s T_s K_s,
@@ -53,7 +53,7 @@ Section fix_lang.
           ⌜prim_step P_s e_s' σ_s' e_s'' σ_s'' efs_s⌝ ∗
           ⌜length efs_t = length efs_s⌝ ∗
           state_interp P_t σ_t' P_s σ_s'' (<[π := fill K_s e_s'']> T_s ++ efs_s) ∗ greatest_rec Φ π e_t' e_s'' ∗
-          [∗ list] π'↦e_t; e_s ∈ efs_t; efs_s, greatest_rec (lift_post val_rel) (length T_s + π') e_t e_s))
+          [∗ list] π'↦e_t; e_s ∈ efs_t; efs_s, greatest_rec (lift_post (val_rel (length T_s + π'))) (length T_s + π') e_t e_s))
     )%I.
 
   Lemma gsim_expr_inner_mono l1 l2 g1 g2:
@@ -216,7 +216,7 @@ Section fix_lang.
 
   End sim_def.
 
-  Implicit Types (Ω : val Λ → val Λ → PROP).
+  Implicit Types (Ω : thread_id → val Λ → val Λ → PROP).
 
   Definition gsim_expr_aux : seal (λ Ω, global_greatest_def Ω).
   Proof. by eexists. Qed.
@@ -250,7 +250,7 @@ Section fix_lang.
           ⌜length efs_t = length efs_s⌝ ∗
           state_interp P_t σ_t' P_s σ_s'' (<[π := fill K_s e_s'']> T_s ++ efs_s) ∗
           gsim_expr Ω Φ π e_t' e_s'' ∗
-          [∗ list] π'↦e_t; e_s ∈ efs_t; efs_s, gsim_expr Ω (lift_post Ω) (length T_s + π') e_t e_s))
+          [∗ list] π'↦e_t; e_s ∈ efs_t; efs_s, gsim_expr Ω (lift_post (Ω (length T_s + π'))) (length T_s + π') e_t e_s))
     )%I.
   Proof.
     rewrite gsim_expr_fixpoint /gsim_expr_inner //.
@@ -636,7 +636,7 @@ Section fix_lang.
 
   (* we show that the local simulation for all functions in the program implies the global simulation *)
   Definition local_rel Ω P_t P_s : PROP :=
-    (□ ∀ f K_s π, ⌜P_s !! f = Some K_s⌝ → ∃ K_t, ⌜P_t !! f = Some K_t⌝ ∗ sim_ectx Ω π K_t K_s Ω)%I.
+    (□ ∀ f K_s π, ⌜P_s !! f = Some K_s⌝ → ∃ K_t, ⌜P_t !! f = Some K_t⌝ ∗ sim_ectx Ω π K_t K_s (Ω π))%I.
   Typeclasses Opaque local_rel.
 
   Global Instance local_rel_persistent Ω P_s P_t : Persistent (local_rel Ω P_s P_t).
@@ -697,8 +697,8 @@ Section fix_lang.
     is_Some (P_s !! f) →
     local_rel Ω P_t P_s -∗
     progs_are P_t P_s -∗
-    Ω v_t v_s -∗
-    gsim_expr Ω (lift_post Ω) π (of_call f v_t) (of_call f v_s).
+    Ω π v_t v_s -∗
+    gsim_expr Ω (lift_post (Ω π)) π (of_call f v_t) (of_call f v_s).
   Proof.
     iIntros ([K_s Hlook]) "#Hloc #Hprogs Hval".
     iApply (local_to_global with "Hloc Hprogs").
diff --git a/theories/simulation/lifting.v b/theories/simulation/lifting.v
index 61f98b2c6fe00a3c74c288ca425a7424319bd584..b063a33143ca2bd8b36b42d67441cfe10965da1a 100644
--- a/theories/simulation/lifting.v
+++ b/theories/simulation/lifting.v
@@ -117,7 +117,7 @@ Hint Mode PureExec - - - + - : core.
 Section fix_sim.
   Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
   Context {Λ : language} {s : simulirisG PROP Λ}.
-  Context (Ω : val Λ → val Λ → PROP) (π : thread_id).
+  Context (Ω : thread_id → val Λ → val Λ → PROP) (π : thread_id).
 
   Implicit Types
     (e_s e_t e: expr Λ)
@@ -173,7 +173,7 @@ Section fix_sim.
         ⌜prim_step P_t e_t σ_t e_t' σ_t' efs_t⌝ ==∗
           ∃ e_s' efs_s σ_s', ⌜prim_step P_s e_s σ_s e_s' σ_s' efs_s⌝ ∗
             state_interp P_t σ_t' P_s σ_s' (<[π:=K_s e_s']>T_s ++ efs_s) ∗ e_t' ⪯{π, Ω} e_s' [{ Φ }] ∗
-            ([∗ list] π'↦e_t0;e_s0 ∈ efs_t;efs_s, e_t0 ⪯{length T_s + π', Ω} e_s0 [{lift_post Ω}])) -∗
+            ([∗ list] π'↦e_t0;e_s0 ∈ efs_t;efs_s, e_t0 ⪯{length T_s + π', Ω} e_s0 [{lift_post (Ω (length T_s + π'))}])) -∗
     e_t ⪯{π, Ω} e_s [{ Φ }].
   Proof.
     iIntros "Hsim".
@@ -261,7 +261,7 @@ Section fix_sim.
         ⌜head_step P_t e_t σ_t e_t' σ_t' efs_t⌝ ==∗
           ∃ e_s' efs_s σ_s', ⌜head_step P_s e_s σ_s e_s' σ_s' efs_s⌝ ∗
           state_interp P_t σ_t' P_s σ_s' (<[π:=fill K_s e_s']>T_s ++ efs_s) ∗ e_t' ⪯{π, Ω} e_s' [{ Φ }] ∗
-          ([∗ list] π'↦e_t0;e_s0 ∈ efs_t;efs_s, e_t0 ⪯{length T_s + π', Ω} e_s0 [{lift_post Ω}])) -∗
+          ([∗ list] π'↦e_t0;e_s0 ∈ efs_t;efs_s, e_t0 ⪯{length T_s + π', Ω} e_s0 [{lift_post (Ω (length T_s + π'))}])) -∗
     e_t ⪯{π, Ω} e_s [{ Φ }].
   Proof.
     iIntros "Hsim". iApply sim_lift_prim_step_both. iIntros (??????) "[Hstate %Hnreach]".
@@ -347,8 +347,8 @@ Section fix_sim.
 
   (** Call *)
   Lemma sim_lift_call Φ fn v_t v_s :
-    Ω v_t v_s -∗
-    (∀ v_t v_s, Ω v_t v_s -∗ Φ (of_val v_t) (of_val v_s)) -∗
+    Ω π v_t v_s -∗
+    (∀ v_t v_s, Ω π v_t v_s -∗ Φ (of_val v_t) (of_val v_s)) -∗
     (of_call fn v_t) ⪯{π, Ω} (of_call fn v_s) [{ Φ }].
   Proof.
     iIntros "Hom Hv".
diff --git a/theories/simulation/simulation.v b/theories/simulation/simulation.v
index 7e84a7c0c0d59e79e208c029df82e528ea419fbb..8cae70bb9f07378a29ed705f899b56be0ebcd2ae 100644
--- a/theories/simulation/simulation.v
+++ b/theories/simulation/simulation.v
@@ -32,12 +32,12 @@ Proof. rewrite /progs_are; apply _. Qed.
 (** Typeclass for the simulation relation so we can use the definitions with
    greatest+least fp (stuttering) or just greatest fp (no stuttering). *)
 Class Sim {PROP : bi} {Λ : language} (s : simulirisG PROP Λ) :=
-  sim : (val Λ → val Λ → PROP) → (val Λ → val Λ → PROP) → thread_id → expr Λ → expr Λ → PROP.
+  sim : (thread_id → val Λ → val Λ → PROP) → (val Λ → val Λ → PROP) → thread_id → expr Λ → expr Λ → PROP.
 #[global]
 Hint Mode Sim - - - : typeclass_instances.
 
 Class SimE {PROP : bi} {Λ : language} (s : simulirisG PROP Λ) :=
-  sim_expr : (val Λ → val Λ → PROP) → (expr Λ → expr Λ → PROP) → thread_id → expr Λ → expr Λ → PROP.
+  sim_expr : (thread_id → val Λ → val Λ → PROP) → (expr Λ → expr Λ → PROP) → thread_id → expr Λ → expr Λ → PROP.
 #[global]
 Hint Mode SimE - - - : typeclass_instances.
 
@@ -67,7 +67,7 @@ Instance thread_id_equiv : Equiv thread_id. apply thread_idO. Defined.
 Section fix_lang.
   Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
   Context {Λ : language}.
-  Context (Ω : val Λ → val Λ → PROP).
+  Context (Ω : thread_id → val Λ → val Λ → PROP).
   Context {s : simulirisG PROP Λ}.
 
   Set Default Proof Using "Type*".
@@ -75,7 +75,7 @@ Section fix_lang.
   Implicit Types (e_s e_t e: expr Λ).
 
   Definition sim_ectx `{!Sim s} π K_t K_s Φ :=
-    (∀ v_t v_s, Ω v_t v_s -∗ sim Ω Φ π (fill K_t (of_val v_t)) (fill K_s (of_val v_s)))%I.
+    (∀ v_t v_s, Ω π v_t v_s -∗ sim Ω Φ π (fill K_t (of_val v_t)) (fill K_s (of_val v_s)))%I.
   Definition sim_expr_ectx `{!SimE s} π K_t K_s Φ :=
-    (∀ v_t v_s, Ω v_t v_s -∗ sim_expr Ω Φ π (fill K_t (of_val v_t)) (fill K_s (of_val v_s)))%I.
+    (∀ v_t v_s, Ω π v_t v_s -∗ sim_expr Ω Φ π (fill K_t (of_val v_t)) (fill K_s (of_val v_s)))%I.
 End fix_lang.
diff --git a/theories/simulation/slsls.v b/theories/simulation/slsls.v
index dfe840b559d9def1e3ba2ca82065780c653b7238..b2b72237b33e72944a353b77f7dcbac8c87c8dc4 100644
--- a/theories/simulation/slsls.v
+++ b/theories/simulation/slsls.v
@@ -98,7 +98,7 @@ Section fix_lang.
     (λ e_t e_s, ∃ v_t v_s, ⌜e_t = of_val v_t⌝ ∗ ⌜e_s = of_val v_s⌝ ∗ Φ v_t v_s)%I.
 
   Section sim_def.
-  Context (val_rel : val Λ → val Λ → PROP).
+  Context (val_rel : thread_id → val Λ → val Λ → PROP).
 
   (* Thread id must come after postcondition as otherwise NonExpansive
   applies to the thread id instead of the post-condition. *)
@@ -121,14 +121,14 @@ Section fix_lang.
           ⌜prim_step P_s e_s' σ_s' e_s'' σ_s'' efs_s⌝ ∗
           ⌜length efs_t = length efs_s⌝ ∗
           state_interp P_t σ_t' P_s σ_s'' (<[π := fill K_s e_s'']> T_s ++ efs_s) ∗ greatest_rec Φ π e_t' e_s'' ∗
-          [∗ list] π'↦e_t; e_s ∈ efs_t; efs_s, greatest_rec (lift_post val_rel) (length T_s + π') e_t e_s))
+          [∗ list] π'↦e_t; e_s ∈ efs_t; efs_s, greatest_rec (lift_post (val_rel (length T_s + π'))) (length T_s + π') e_t e_s))
 
       ∨ (* call case *)
       (∃ f K_t v_t K_s' v_s σ_s',
         ⌜e_t = fill K_t (of_call f v_t)⌝ ∗
         ⌜no_forks P_s e_s σ_s (fill K_s' (of_call f v_s)) σ_s'⌝ ∗
-        val_rel v_t v_s ∗ state_interp P_t σ_t P_s σ_s' (<[π := fill K_s (fill K_s' (of_call f v_s))]> T_s) ∗
-        (∀ v_t v_s, val_rel v_t v_s -∗ greatest_rec Φ π (fill K_t (of_val v_t)) (fill K_s' (of_val v_s)) ))
+        val_rel π v_t v_s ∗ state_interp P_t σ_t P_s σ_s' (<[π := fill K_s (fill K_s' (of_call f v_s))]> T_s) ∗
+        (∀ v_t v_s, val_rel π  v_t v_s -∗ greatest_rec Φ π (fill K_t (of_val v_t)) (fill K_s' (of_val v_s)) ))
     )%I.
 
 
@@ -299,7 +299,7 @@ Section fix_lang.
 
   End sim_def.
 
-  Implicit Types (Ω : val Λ → val Λ → PROP).
+  Implicit Types (Ω : thread_id → val Λ → val Λ → PROP).
 
   Definition sim_expr_aux : seal (λ Ω, greatest_def Ω).
   Proof. by eexists. Qed.
@@ -339,13 +339,13 @@ Section fix_lang.
           ⌜length efs_t = length efs_s⌝ ∗
           state_interp P_t σ_t' P_s σ_s'' (<[π := fill K_s e_s'']> T_s ++ efs_s) ∗
           sim_expr Ω Φ π e_t' e_s'' ∗
-          [∗ list] π'↦e_t; e_s ∈ efs_t; efs_s, sim_expr Ω (lift_post Ω) (length T_s + π') e_t e_s))
+          [∗ list] π'↦e_t; e_s ∈ efs_t; efs_s, sim_expr Ω (lift_post (Ω (length T_s + π'))) (length T_s + π') e_t e_s))
 
       ∨ (* call case *)
       (∃ f K_t v_t K_s' v_s σ_s',
         ⌜e_t = fill K_t (of_call f v_t)⌝ ∗
         ⌜no_forks P_s e_s σ_s (fill K_s' (of_call f v_s)) σ_s'⌝ ∗
-        Ω v_t v_s ∗ state_interp P_t σ_t P_s σ_s' (<[π := fill K_s (fill K_s' (of_call f v_s))]> T_s) ∗
+        Ω π v_t v_s ∗ state_interp P_t σ_t P_s σ_s' (<[π := fill K_s (fill K_s' (of_call f v_s))]> T_s) ∗
         sim_expr_ectx Ω π K_t K_s' Φ)
     )%I.
   Proof.
@@ -764,7 +764,7 @@ Section fix_lang.
   Lemma sim_call_inline Ω P_t P_s v_t v_s K_t K_s f Φ π :
     P_t !! f = Some K_t →
     P_s !! f = Some K_s →
-    ⊢ progs_are P_t P_s ∗ Ω v_t v_s ∗ sim_expr_ectx Ω π K_t K_s Φ -∗ (of_call f v_t) ⪯{π, Ω} (of_call f v_s) [{ Φ }].
+    ⊢ progs_are P_t P_s ∗ Ω π v_t v_s ∗ sim_expr_ectx Ω π K_t K_s Φ -∗ (of_call f v_t) ⪯{π, Ω} (of_call f v_s) [{ Φ }].
   Proof.
     intros Htgt Hsrc. iIntros "(#Prog & Val & Sim)".
     rewrite sim_expr_unfold. iIntros (P_t' σ_t P_s' σ_s T_s K_s') "[SI [% %]]".