diff --git a/_CoqProject b/_CoqProject
index efee60834b33999924a9e40afd0b649a5db5bed4..3c8ac837e6ad727b726e0050d562c4d9678aed94 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -37,7 +37,6 @@ theories/simplang/gen_refl.v
 theories/simplang/pure_refl.v
 theories/simplang/heapbij.v
 theories/simplang/globalbij.v
-theories/simplang/parallel_subst.v
 theories/simplang/gen_log_rel.v
 theories/simplang/gen_adequacy.v
 theories/simplang/behavior.v
diff --git a/theories/simplang/behavior.v b/theories/simplang/behavior.v
index ad91931f9a8d9c238e237f87862e4a022da93186..07d111213b38973f66ad3c3c05f5389f13f75aa3 100644
--- a/theories/simplang/behavior.v
+++ b/theories/simplang/behavior.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
 
 From simuliris.logic Require Import satisfiable.
 From simuliris.simulation Require Import behavior.
-From simuliris.simplang Require Import lang notation parallel_subst wf gen_val_rel.
+From simuliris.simplang Require Import lang notation wf gen_val_rel.
 
 (** Define "observable behavior" and a generic notion of contextual refinement.
 *)
@@ -42,10 +42,15 @@ Section ctx_rel.
       <hole> will be the function argument. *)
   Definition gen_ctx_rel (e_t e_s : expr) :=
     ∀ (C : ctx) (fname x : string) (p : prog),
-      map_Forall (λ _ K, gen_ectx_wf expr_head_wf K ∧ free_vars_ectx K = ∅) p →
+      (* The other functions need to be well-formed and closed *)
+      map_Forall (λ _ '(arg, body), gen_expr_wf expr_head_wf body ∧ free_vars body ⊆ {[arg]}) p →
+      (* The context needs to be well-formed *)
       gen_ctx_wf expr_head_wf C →
+      (* The context needs to close our expressions *)
       free_vars (fill_ctx C e_t) ∪ free_vars (fill_ctx C e_s) ⊆ {[x]} →
-      beh_rel (<[fname := (λ: x, fill_ctx C e_t)%E]> p) (<[fname := (λ: x, fill_ctx C e_s)%E]> p).
+      (* Then we demand [beh_rel] if putting our expressions into a context to
+         obtain a whole function and that function into a program *)
+      beh_rel (<[fname := (x, fill_ctx C e_t)]> p) (<[fname := (x, fill_ctx C e_s)]> p).
 
   Lemma gen_val_rel_obs {Σ} loc_rel v_t v_s :
     gen_val_rel loc_rel v_t v_s ⊢@{iPropI Σ} ⌜obs_val v_t v_s⌝.
diff --git a/theories/simplang/gen_adequacy.v b/theories/simplang/gen_adequacy.v
index a6d81658771eed73ba2fd953bc2d25a18aaac76e..0cbad5f143eb5d6f3ebd412616497151e4ae1a0e 100644
--- a/theories/simplang/gen_adequacy.v
+++ b/theories/simplang/gen_adequacy.v
@@ -1,7 +1,6 @@
 From simuliris.logic Require Import satisfiable.
 From simuliris.simulation Require Import slsls global_sim adequacy.
-From simuliris.simplang Require Import proofmode tactics behavior.
-From simuliris.simplang Require Import parallel_subst gen_val_rel wf.
+From simuliris.simplang Require Import proofmode tactics behavior gen_val_rel wf.
 From iris.prelude Require Import options.
 
 (** Generic adequacy theorem for sheap-based logical relations. *)
diff --git a/theories/simplang/gen_log_rel.v b/theories/simplang/gen_log_rel.v
index 1f3bcfff23941b4acb16a9ecd318454243676184..3b3a853c6dd989ed08265093588f71f30b1b0a50 100644
--- a/theories/simplang/gen_log_rel.v
+++ b/theories/simplang/gen_log_rel.v
@@ -1,6 +1,6 @@
 From simuliris.simulation Require Import slsls lifting.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import parallel_subst primitive_laws gen_val_rel wf.
+From simuliris.simplang Require Import primitive_laws gen_val_rel wf.
 From iris.prelude Require Import options.
 
 (** * Logical relation
@@ -39,11 +39,21 @@ Section open_rel.
     destruct (map !! x) as [[v_t v_s]|]; last done. eauto.
   Qed.
 
-  Lemma subst_map_rel_weaken {X1} X2 map :
+  Lemma subst_map_rel_weaken X1 X2 map :
     X2 ⊆ X1 →
     subst_map_rel X1 map -∗ subst_map_rel X2 map.
   Proof. iIntros (HX). iApply big_sepS_subseteq. done. Qed.
 
+  Lemma subst_map_rel_singleton X x v_t v_s :
+    X ⊆ {[x]} →
+    val_rel v_t v_s -∗
+    subst_map_rel X {[x:=(v_t, v_s)]}.
+  Proof.
+    iIntros (?) "Hrel".
+    iApply (subst_map_rel_weaken {[x]}); first done.
+    rewrite /subst_map_rel big_sepS_singleton lookup_singleton. done.
+  Qed.
+
   (* TODO: use [binder_delete], once we can [delete] on [gset]. *)
   Definition binder_delete_gset (b : binder) (X : gset string) :=
     match b with BAnon => X | BNamed x => X ∖ {[x]} end.
@@ -95,6 +105,20 @@ Section open_rel.
     rewrite !subst_map_closed //; set_solver.
   Qed.
 
+  Lemma gen_log_rel_singleton e_t e_s v_t v_s arg π :
+    free_vars e_t ∪ free_vars e_s ⊆ {[ arg ]} →
+    gen_log_rel e_t e_s -∗
+    val_rel v_t v_s -∗
+    thread_own π -∗ 
+    subst_map {[arg := v_t]} e_t ⪯{π} subst_map {[arg := v_s]} e_s
+      {{ λ v_t v_s, thread_own π ∗ val_rel v_t v_s }}.
+  Proof.
+    iIntros (?) "Hlog Hval Hπ".
+    iDestruct ("Hlog" $! _ {[arg := (v_t, v_s)]} with "[Hval] Hπ") as "Hsim".
+    { by iApply subst_map_rel_singleton. }
+    rewrite !fmap_insert !fmap_empty. done.
+  Qed.
+
   (** Substitute away a single variable in an [gen_log_rel].
       Use the [gen_log_rel] tactic below to automatically apply this for all free variables. *)
   Lemma gen_log_rel_subst x e_t e_s `{!∀ vt vs, Persistent (val_rel vt vs)}:
diff --git a/theories/simplang/gen_refl.v b/theories/simplang/gen_refl.v
index eab4d520083b9e8ed5799a765b0a78fb45bd4eb3..2db91cfb864e07313c1211d81cc951f1c166f822 100644
--- a/theories/simplang/gen_refl.v
+++ b/theories/simplang/gen_refl.v
@@ -1,6 +1,6 @@
 From simuliris.simulation Require Import slsls lifting.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import parallel_subst primitive_laws gen_val_rel gen_log_rel wf.
+From simuliris.simplang Require Import primitive_laws gen_val_rel gen_log_rel wf.
 From iris.prelude Require Import options.
 
 (** * Lemmas for proving [log_rel]
diff --git a/theories/simplang/gen_val_rel.v b/theories/simplang/gen_val_rel.v
index 21f552074562ab5e399f4fb0d62684ef69e42a5b..e0721baa2284b8d0671b7929406cc61c6f3d892c 100644
--- a/theories/simplang/gen_val_rel.v
+++ b/theories/simplang/gen_val_rel.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import iprop.
 From simuliris.simulation Require Import slsls lifting.
-From simuliris.simplang Require Import notation parallel_subst.
+From simuliris.simplang Require Import notation.
 From iris.prelude Require Import options.
 
 (** * Structural value relation
diff --git a/theories/simplang/globalbij.v b/theories/simplang/globalbij.v
index def804421fcf5f25879be57fd462f52919f6f04d..66f64d02b739f09b33e261da483ed472c488d859 100644
--- a/theories/simplang/globalbij.v
+++ b/theories/simplang/globalbij.v
@@ -1,6 +1,6 @@
 From simuliris.simulation Require Import slsls lifting.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import parallel_subst primitive_laws gen_log_rel gen_val_rel.
+From simuliris.simplang Require Import primitive_laws gen_log_rel gen_val_rel.
 From iris.prelude Require Import options.
 
 (** * Bijection between global variables
diff --git a/theories/simplang/lang.v b/theories/simplang/lang.v
index e1b8d44633d9724f5e54fb06a94a080ef7352e69..45dbcdf0416288287467c25707d315c268d284e9 100644
--- a/theories/simplang/lang.v
+++ b/theories/simplang/lang.v
@@ -831,7 +831,7 @@ Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K2 (fill K1 e).
 Proof. apply foldl_app. Qed.
 
 (** Programs *)
-Definition prog := gmap fname ectx.
+Definition prog := gmap fname (string * expr).
 
 Notation "e1 ;; e2" := (Let BAnon e1%E e2%E)
   (at level 100, e2 at level 200,
@@ -909,9 +909,9 @@ Inductive head_step (P : prog) : expr → state → expr → state → list expr
       σ.(heap) !! l = Some (WSt, v) →
       head_step P (Store Na2Ord (Val $ LitV $ LitLoc l) (Val v')) σ
                 (Val $ LitV LitUnit) (state_upd_heap <[l:=(RSt 0, v')]> σ) []
-  | CallS f v K σ :
-     P !! f = Some K →
-     head_step P (Call (Val $ LitV $ LitFn f) (Val v)) σ (fill K (Val v)) σ [].
+  | CallS f v x e σ :
+     P !! f = Some (x, e) →
+     head_step P (Call (Val $ LitV $ LitFn f) (Val v)) σ (subst x v e) σ [].
 
 
 Definition of_class (m : mixin_expr_class val) : expr :=
@@ -1063,17 +1063,223 @@ Proof.
   exists K''. unfold ectx_compose. cbn. by rewrite assoc.
 Qed.
 
+
+(** * Parallel substitution for SimpLang *)
+(** Definitions and proofs mostly yoinked from https://gitlab.mpi-sws.org/FP/stacked-borrows/-/blob/master/theories/lang/subst_map.v *)
+
+Fixpoint subst_map (xs : gmap string val) (e : expr) : expr :=
+  match e with
+  | Var y => if xs !! y is Some v then Val v else Var y
+  | Val v => Val v
+  | GlobalVar n => GlobalVar n
+  | Let x1 e1 e2 => Let x1 (subst_map xs e1) (subst_map (binder_delete x1 xs) e2)
+  | UnOp op e => UnOp op (subst_map xs e)
+  | BinOp op e1 e2 => BinOp op (subst_map xs e1) (subst_map xs e2)
+  | If e0 e1 e2 => If (subst_map xs e0) (subst_map xs e1) (subst_map xs e2)
+  | While e0 e1 => While (subst_map xs e0) (subst_map xs e1)
+  | Pair e1 e2 => Pair (subst_map xs e1) (subst_map xs e2)
+  | Fst e => Fst (subst_map xs e)
+  | Snd e => Snd (subst_map xs e)
+  | InjL e => InjL (subst_map xs e)
+  | InjR e => InjR (subst_map xs e)
+  | Match e0 x1 e1 x2 e2 => Match (subst_map xs e0) x1 (subst_map (binder_delete x1 xs) e1)
+      x2 (subst_map (binder_delete x2 xs) e2)
+  | Fork e => Fork (subst_map xs e)
+  | AllocN e1 e2 => AllocN (subst_map xs e1) (subst_map xs e2)
+  | FreeN e1 e2 => FreeN (subst_map xs e1) (subst_map xs e2)
+  | Load o e => Load o (subst_map xs e)
+  | Store o e1 e2 => Store o (subst_map xs e1) (subst_map xs e2)
+  | CmpXchg e0 e1 e2 => CmpXchg (subst_map xs e0) (subst_map xs e1) (subst_map xs e2)
+  | FAA e1 e2 => FAA (subst_map xs e1) (subst_map xs e2)
+  | Call e1 e2 => Call (subst_map xs e1) (subst_map xs e2)
+  end.
+
+Lemma subst_map_empty e :
+  subst_map ∅ e = e.
+Proof.
+  induction e; simpl; f_equal; eauto.
+  all: match goal with |- context[binder_delete ?x ∅] => destruct x; first done end.
+  all: simpl; rewrite delete_empty; done.
+Qed.
+
+Lemma subst_map_subst map x (v : val) (e : expr) :
+  subst_map map (subst x v e) = subst_map (<[x:=v]>map) e.
+Proof.
+  revert x v map; induction e; intros xx r map; simpl;
+  try (f_equal; eauto).
+  all: try match goal with |- context[binder_delete ?x _] => destruct x; simpl; first done end.
+  - case_decide.
+    + simplify_eq/=. by rewrite lookup_insert.
+    + rewrite lookup_insert_ne; done.
+  - case_decide.
+    + rewrite delete_insert_ne; last by congruence. done.
+    + simplify_eq/=. by rewrite delete_insert_delete.
+  - case_decide.
+    + rewrite delete_insert_ne; last by congruence. done.
+    + simplify_eq/=. by rewrite delete_insert_delete.
+  - case_decide.
+    + rewrite delete_insert_ne; last by congruence. done.
+    + simplify_eq/=. by rewrite delete_insert_delete.
+Qed.
+
+Lemma subst_subst_map x (v : val) map e :
+  subst x v (subst_map (delete x map) e) =
+  subst_map (<[x:=v]>map) e.
+Proof.
+  revert map v x; induction e; intros map v0 xx; simpl;
+  try (f_equal; eauto).
+  all: try match goal with |- context[binder_delete ?x _] => destruct x; simpl; first by auto end.
+  - match goal with |- context[delete _ _ !! ?s] => rename s into x end.
+    destruct (decide (xx=x)) as [->|Hne].
+    + rewrite lookup_delete // lookup_insert //. simpl.
+      rewrite decide_True //.
+    + rewrite lookup_delete_ne // lookup_insert_ne //.
+      destruct (map !! x) as [rr|].
+      * by destruct rr.
+      * simpl. rewrite decide_False //.
+  - case_decide.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. eauto.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+  - case_decide.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. eauto.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+  - case_decide.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. eauto.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+Qed.
+
+Lemma subst_map_singleton x v e :
+  subst_map {[x:=v]} e = subst x v e.
+Proof. rewrite -subst_map_subst subst_map_empty //. Qed.
+
+Lemma subst'_subst_map b (v : val) map e :
+  subst' b v (subst_map (binder_delete b map) e) =
+  subst_map (binder_insert b v map) e.
+Proof.
+  destruct b; first done.
+  exact: subst_subst_map.
+Qed.
+
+Lemma subst_map_subst_map xs ys e :
+  subst_map xs (subst_map ys e) = subst_map (ys ∪ xs) e.
+Proof.
+  revert e.
+  induction ys as [|x v ys HNone IH] using map_ind => e.
+  { by rewrite left_id subst_map_empty. }
+  by rewrite -insert_union_l -[in X in _ = X]subst_map_subst -IH subst_map_subst.
+Qed.
+
+(** "Free variables" and their interaction with subst_map *)
+Local Definition binder_to_ctx (x : binder) : gset string :=
+  if x is BNamed s then {[s]} else ∅.
+
+Fixpoint free_vars (e : expr) : gset string :=
+  match e with
+  | Val v => ∅
+  | GlobalVar n => ∅
+  | Var x => {[x]}
+  | Let x e1 e2 => free_vars e1 ∪ (free_vars e2 ∖ binder_to_ctx x)
+  | Match e0 x1 e1 x2 e2 =>
+    free_vars e0 ∪
+    (free_vars e1 ∖ binder_to_ctx x1) ∪
+    (free_vars e2 ∖ binder_to_ctx x2)
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Load _ e =>
+     free_vars e
+  | Call e1 e2 | While e1 e2 | BinOp _ e1 e2 | Pair e1 e2
+  | AllocN e1 e2 | FreeN e1 e2 | Store _ e1 e2 | FAA e1 e2 =>
+     free_vars e1 ∪ free_vars e2
+  | If e0 e1 e2 | CmpXchg e0 e1 e2 =>
+     free_vars e0 ∪ free_vars e1 ∪ free_vars e2
+  end.
+
+(* Just fill with any value, it does not make a difference. *)
+Definition free_vars_ectx (K : ectx) : gset string :=
+  free_vars (fill K (Val (LitV LitUnit))).
+
+Local Lemma binder_delete_eq x y (xs1 xs2 : gmap string val) :
+  (if y is BNamed s then s ≠ x → xs1 !! x = xs2 !! x else xs1 !! x = xs2 !! x) →
+  binder_delete y xs1 !! x = binder_delete y xs2 !! x.
+Proof.
+  destruct y as [|s]; first done. simpl.
+  destruct (decide (s = x)) as [->|Hne].
+  - rewrite !lookup_delete //.
+  - rewrite !lookup_delete_ne //. eauto.
+Qed.
+
+Lemma subst_map_free_vars (xs1 xs2 : gmap string val) (e : expr) :
+  (∀ x, x ∈ free_vars e → xs1 !! x = xs2 !! x) →
+  subst_map xs1 e = subst_map xs2 e.
+Proof.
+  revert xs1 xs2; induction e=>/= xs1 xs2 Heq;
+  solve [
+    (* trivial cases *)
+    done
+  | (* variable case *)
+    rewrite Heq; [done|set_solver]
+  | (* recursive cases *)
+    f_equal;
+    repeat lazymatch goal with x : binder |- _ => destruct x end;
+    intuition eauto using binder_delete_eq with set_solver
+  ].
+Qed.
+
+Lemma subst_map_closed xs e :
+  free_vars e = ∅ →
+  subst_map xs e = e.
+Proof.
+  intros Hclosed.
+  trans (subst_map ∅ e).
+  - apply subst_map_free_vars. rewrite Hclosed. done.
+  - apply subst_map_empty.
+Qed.
+
+Lemma subst_free_vars x v e :
+  x ∉ free_vars e →
+  subst x v e = e.
+Proof.
+  intros Hfree.
+  rewrite -(subst_map_empty (subst x v e)).
+  rewrite subst_map_subst.
+  rewrite (subst_map_free_vars _ ∅); first by apply subst_map_empty.
+  intros y ?. rewrite lookup_insert_ne //. set_solver.
+Qed.
+
+Lemma free_vars_subst x v e :
+  free_vars (subst x v e) = free_vars e ∖ {[x]}.
+Proof.
+  induction e=>/=; repeat case_decide; set_solver.
+Qed.
+
+Lemma free_vars_subst_map xs e :
+  free_vars (subst_map xs e) = free_vars e ∖ (dom _ xs).
+Proof.
+  induction xs as [| x v xs HNone IH] using map_ind.
+  - rewrite subst_map_empty. set_solver.
+  - rewrite -subst_subst_map delete_notin // free_vars_subst IH. set_solver.
+Qed.
+
+Lemma free_vars_fill K e :
+  free_vars (fill K e) = free_vars_ectx K ∪ free_vars e.
+Proof.
+  revert e. induction K as [|Ki K IH] using rev_ind; intros e; simpl.
+  { simpl. rewrite /free_vars_ectx /= left_id_L. done. }
+  rewrite /free_vars_ectx !fill_app /=. destruct Ki; simpl.
+  all: rewrite !IH; set_solver+.
+Qed.
+
+
 (* Proving the mixin *)
 
-Lemma simp_lang_mixin : LanguageMixin of_class to_class empty_ectx ectx_compose fill head_step.
+Lemma simp_lang_mixin : LanguageMixin of_class to_class empty_ectx ectx_compose fill subst_map free_vars head_step.
 Proof.
   constructor.
   - apply to_of_class.
   - apply of_to_class.
   - intros p v ???? H%val_head_stuck. cbn in H. congruence.
-  - intros p f v ???. split.
-    + cbn. inversion 1; subst. eauto.
-    + intros (K & ? & -> & -> & ->). cbn. by constructor.
+  - intros p f v ????. split.
+    + cbn. inversion 1; subst. eexists _, _. rewrite subst_map_singleton. eauto.
+    + intros (x & e & ? & -> & -> & ->). cbn. rewrite subst_map_singleton. by constructor.
+  - eapply subst_map_free_vars.
   - done.
   - intros ???. by rewrite -fill_app.
   - apply fill_inj.
diff --git a/theories/simplang/na_inv/adequacy.v b/theories/simplang/na_inv/adequacy.v
index c41302347981962414d7d3d33fd8a7ab4294acce..3b1623faf0031fcd204c9ab00fa0435854c6c159 100644
--- a/theories/simplang/na_inv/adequacy.v
+++ b/theories/simplang/na_inv/adequacy.v
@@ -7,7 +7,7 @@ From iris.prelude Require Import options.
 From simuliris.logic Require Import satisfiable.
 From simuliris.simulation Require Import slsls global_sim.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import gen_adequacy behavior wf parallel_subst gen_refl.
+From simuliris.simplang Require Import gen_adequacy behavior wf gen_refl.
 From simuliris.simplang.na_inv Require Import inv refl.
 
 (** Instantiate our notion of contextual refinement. *)
@@ -67,25 +67,27 @@ Proof.
   apply (prog_rel_adequacy Σ). eapply isat_intro.
   iIntros (? gs Hgs) "_ _ _ _ !#".
   iSplit. { iApply big_sepM_intro. iIntros "!>" (???). iApply val_wf_sound. by apply: Hgs. }
-  iIntros "!# %f %K_s %π".
+  rewrite /prog_rel.
+  iIntros "!# %f %arg %body".
   iDestruct (Hrel _) as "Hrel". clear Hrel.
   destruct (decide (f = fname)) as [->|Hne].
   - rewrite !lookup_insert.
-    iIntros ([= <-]). iExists _. iSplitR; first done.
+    iIntros ([= <- <-]). iExists _, _. iSplitR; first done.
     (* TODO Factor this into a general lemma? *)
-    iIntros (v_t v_s) "[Hc #Hval] /=".
-    iApply (log_rel_closed_1 with "[] Hc").
-    { simpl. set_solver. }
-    iApply log_rel_let.
-    { iApply log_rel_val. done. }
-    iApply log_rel_ctx; done.
+    iIntros (v_t v_s π) "[Hc #Hval] /=".
+    iApply (sim_wand with "[Hc]").
+    + iApply (gen_log_rel_singleton with "[Hrel] Hval [Hc]"); first done.
+      * by iApply log_rel_ctx.
+      * done.
+    + simpl. iIntros (??). auto.
   - rewrite !lookup_insert_ne //.
-    iIntros (Hf). rename K_s into K. iExists K. iSplit; first done.
+    iIntros (Hf). iExists arg, body. iSplit; first done.
     specialize (Hpwf _ _ Hf). destruct Hpwf as [HKwf HKclosed].
     (* TODO Factor this into a lemma? *)
-    iIntros (v_t v_s) "[Hc #Hval] /=".
-    iApply (log_rel_closed_1 with "[] Hc").
-    { rewrite !free_vars_fill HKclosed. set_solver+. }
-    iApply log_rel_ectx; first done.
-    iApply log_rel_val; done.
+    iIntros (v_t v_s π) "[Hc #Hval] /=".
+    iApply (sim_wand with "[Hc]").
+    + iApply (gen_log_rel_singleton with "[Hrel] Hval [Hc]"); first set_solver.
+      * by iApply log_rel_refl.
+      * done.
+    + simpl. iIntros (??). auto.
 Qed.
diff --git a/theories/simplang/na_inv/examples/data_races.v b/theories/simplang/na_inv/examples/data_races.v
index 3c71a32947f47829ab34fa14971a064041e08fa5..b7d07fadaed985b6924fa0d2868742d5c628a1ea 100644
--- a/theories/simplang/na_inv/examples/data_races.v
+++ b/theories/simplang/na_inv/examples/data_races.v
@@ -1,4 +1,4 @@
-From simuliris.simplang Require Import lang notation tactics class_instances proofmode gen_log_rel parallel_subst wf.
+From simuliris.simplang Require Import lang notation tactics class_instances proofmode gen_log_rel wf.
 From iris Require Import bi.bi.
 From iris.proofmode Require Import tactics.
 From simuliris.simulation Require Import slsls lifting.
diff --git a/theories/simplang/na_inv/examples/remove_alloc.v b/theories/simplang/na_inv/examples/remove_alloc.v
index 398d22c2b34edddf8f65145d8884430e72a79e3e..2d90e29beb982cd29fc0cd9e2b1daff65d2c6287 100644
--- a/theories/simplang/na_inv/examples/remove_alloc.v
+++ b/theories/simplang/na_inv/examples/remove_alloc.v
@@ -1,4 +1,4 @@
-From simuliris.simplang Require Import lang notation tactics class_instances proofmode gen_log_rel parallel_subst wf.
+From simuliris.simplang Require Import lang notation tactics class_instances proofmode gen_log_rel wf.
 From iris Require Import bi.bi.
 From iris.proofmode Require Import tactics.
 From simuliris.simulation Require Import slsls lifting.
diff --git a/theories/simplang/na_inv/readonly_refl.v b/theories/simplang/na_inv/readonly_refl.v
index f6d80bc251264305ff97da8e3ecabe88d87b81c3..b40fff4732df4b2699029667fe5f6ebbdfb1731f 100644
--- a/theories/simplang/na_inv/readonly_refl.v
+++ b/theories/simplang/na_inv/readonly_refl.v
@@ -1,6 +1,6 @@
 From simuliris.simulation Require Import slsls lifting.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import parallel_subst gen_log_rel gen_refl pure_refl wf.
+From simuliris.simplang Require Import gen_log_rel gen_refl pure_refl wf.
 From simuliris.simplang.na_inv Require Export inv.
 From iris.prelude Require Import options.
 
diff --git a/theories/simplang/na_inv/refl.v b/theories/simplang/na_inv/refl.v
index 2cf74375158001b5f6df284aa6f37638d3b23adf..b996a7ac5a7192642e252c47ea0392a21438001f 100644
--- a/theories/simplang/na_inv/refl.v
+++ b/theories/simplang/na_inv/refl.v
@@ -1,6 +1,6 @@
 From simuliris.simulation Require Import slsls lifting.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import parallel_subst gen_log_rel gen_refl pure_refl wf.
+From simuliris.simplang Require Import gen_log_rel gen_refl pure_refl wf.
 From simuliris.simplang.na_inv Require Export inv.
 From iris.prelude Require Import options.
 
@@ -9,8 +9,8 @@ From iris.prelude Require Import options.
 Definition expr_head_wf (e : expr_head) : Prop :=
   match e with
   | ValHead v => val_wf v
-  (* Na2Ord is an intermediate ordering that should only arise during
-  execution and programs should not use it directly. *)
+  (* Na2Ord is an intermediate (administrative) ordering that should only arise
+  during execution and programs should not use it directly. *)
   | LoadHead o => o ≠ Na2Ord
   | StoreHead o => o ≠ Na2Ord
   | CmpXchgHead => False   (* currently not supported *)
@@ -80,19 +80,4 @@ Section refl.
     intros ?. iApply gen_log_rel_ctx; first by apply na_log_rel_structural. done.
   Qed.
 
-  Corollary log_rel_ectx K e_t e_s :
-    ectx_wf K →
-    log_rel e_t e_s -∗ log_rel (fill K e_t) (fill K e_s).
-  Proof.
-    intros ?. iApply gen_log_rel_ectx; first by apply na_log_rel_structural. done.
-  Qed.
-
-  Lemma log_rel_closed_1 e_t e_s π :
-    free_vars e_t ∪ free_vars e_s = ∅ →
-    log_rel e_t e_s -∗ na_locs π ∅ -∗ e_t ⪯{π} e_s {{ λ v_t v_s, na_locs π ∅ ∗ val_rel v_t v_s }}.
-  Proof.
-    iIntros (?) "#Hrel Hc".
-    iApply sim_mono; last iApply (gen_log_rel_closed_1 with "Hrel Hc"); [|done].
-    iIntros (v_t v_s) "[$ $]".
-  Qed.
 End refl.
diff --git a/theories/simplang/parallel_subst.v b/theories/simplang/parallel_subst.v
deleted file mode 100644
index c4889910fbe76ac5956e1d6f63ae7453b66bc4a9..0000000000000000000000000000000000000000
--- a/theories/simplang/parallel_subst.v
+++ /dev/null
@@ -1,203 +0,0 @@
-From stdpp Require Export gmap.
-From simuliris.simplang Require Export lang notation.
-From iris.prelude Require Import options.
-
-
-(** * Parallel substitution for SimpLang *)
-(** Definitions and proofs mostly yoinked from https://gitlab.mpi-sws.org/FP/stacked-borrows/-/blob/master/theories/lang/subst_map.v *)
-
-Fixpoint subst_map (xs : gmap string val) (e : expr) : expr :=
-  match e with
-  | Var y => if xs !! y is Some v then Val v else Var y
-  | Val v => Val v
-  | GlobalVar n => GlobalVar n
-  | Let x1 e1 e2 => Let x1 (subst_map xs e1) (subst_map (binder_delete x1 xs) e2)
-  | UnOp op e => UnOp op (subst_map xs e)
-  | BinOp op e1 e2 => BinOp op (subst_map xs e1) (subst_map xs e2)
-  | If e0 e1 e2 => If (subst_map xs e0) (subst_map xs e1) (subst_map xs e2)
-  | While e0 e1 => While (subst_map xs e0) (subst_map xs e1)
-  | Pair e1 e2 => Pair (subst_map xs e1) (subst_map xs e2)
-  | Fst e => Fst (subst_map xs e)
-  | Snd e => Snd (subst_map xs e)
-  | InjL e => InjL (subst_map xs e)
-  | InjR e => InjR (subst_map xs e)
-  | Match e0 x1 e1 x2 e2 => Match (subst_map xs e0) x1 (subst_map (binder_delete x1 xs) e1)
-      x2 (subst_map (binder_delete x2 xs) e2)
-  | Fork e => Fork (subst_map xs e)
-  | AllocN e1 e2 => AllocN (subst_map xs e1) (subst_map xs e2)
-  | FreeN e1 e2 => FreeN (subst_map xs e1) (subst_map xs e2)
-  | Load o e => Load o (subst_map xs e)
-  | Store o e1 e2 => Store o (subst_map xs e1) (subst_map xs e2)
-  | CmpXchg e0 e1 e2 => CmpXchg (subst_map xs e0) (subst_map xs e1) (subst_map xs e2)
-  | FAA e1 e2 => FAA (subst_map xs e1) (subst_map xs e2)
-  | Call e1 e2 => Call (subst_map xs e1) (subst_map xs e2)
-  end.
-
-Lemma subst_map_empty e :
-  subst_map ∅ e = e.
-Proof.
-  induction e; simpl; f_equal; eauto.
-  all: match goal with |- context[binder_delete ?x ∅] => destruct x; first done end.
-  all: simpl; rewrite delete_empty; done.
-Qed.
-
-Lemma subst_map_subst map x (v : val) (e : expr) :
-  subst_map map (subst x v e) = subst_map (<[x:=v]>map) e.
-Proof.
-  revert x v map; induction e; intros xx r map; simpl;
-  try (f_equal; eauto).
-  all: try match goal with |- context[binder_delete ?x _] => destruct x; simpl; first done end.
-  - case_decide.
-    + simplify_eq/=. by rewrite lookup_insert.
-    + rewrite lookup_insert_ne; done.
-  - case_decide.
-    + rewrite delete_insert_ne; last by congruence. done.
-    + simplify_eq/=. by rewrite delete_insert_delete.
-  - case_decide.
-    + rewrite delete_insert_ne; last by congruence. done.
-    + simplify_eq/=. by rewrite delete_insert_delete.
-  - case_decide.
-    + rewrite delete_insert_ne; last by congruence. done.
-    + simplify_eq/=. by rewrite delete_insert_delete.
-Qed.
-
-Lemma subst_subst_map x (v : val) map e :
-  subst x v (subst_map (delete x map) e) =
-  subst_map (<[x:=v]>map) e.
-Proof.
-  revert map v x; induction e; intros map v0 xx; simpl;
-  try (f_equal; eauto).
-  all: try match goal with |- context[binder_delete ?x _] => destruct x; simpl; first by auto end.
-  - match goal with |- context[delete _ _ !! ?s] => rename s into x end.
-    destruct (decide (xx=x)) as [->|Hne].
-    + rewrite lookup_delete // lookup_insert //. simpl.
-      rewrite decide_True //.
-    + rewrite lookup_delete_ne // lookup_insert_ne //.
-      destruct (map !! x) as [rr|].
-      * by destruct rr.
-      * simpl. rewrite decide_False //.
-  - case_decide.
-    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. eauto.
-    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
-  - case_decide.
-    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. eauto.
-    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
-  - case_decide.
-    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. eauto.
-    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
-Qed.
-
-Lemma subst'_subst_map b (v : val) map e :
-  subst' b v (subst_map (binder_delete b map) e) =
-  subst_map (binder_insert b v map) e.
-Proof.
-  destruct b; first done.
-  exact: subst_subst_map.
-Qed.
-
-Lemma subst_map_subst_map xs ys e :
-  subst_map xs (subst_map ys e) = subst_map (ys ∪ xs) e.
-Proof.
-  revert e.
-  induction ys as [|x v ys HNone IH] using map_ind => e.
-  { by rewrite left_id subst_map_empty. }
-  by rewrite -insert_union_l -[in X in _ = X]subst_map_subst -IH subst_map_subst.
-Qed.
-
-(** "Free variables" and their interaction with subst_map *)
-Local Definition binder_to_ctx (x : binder) : gset string :=
-  if x is BNamed s then {[s]} else ∅.
-
-Fixpoint free_vars (e : expr) : gset string :=
-  match e with
-  | Val v => ∅
-  | GlobalVar n => ∅
-  | Var x => {[x]}
-  | Let x e1 e2 => free_vars e1 ∪ (free_vars e2 ∖ binder_to_ctx x)
-  | Match e0 x1 e1 x2 e2 =>
-    free_vars e0 ∪
-    (free_vars e1 ∖ binder_to_ctx x1) ∪
-    (free_vars e2 ∖ binder_to_ctx x2)
-  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Load _ e =>
-     free_vars e
-  | Call e1 e2 | While e1 e2 | BinOp _ e1 e2 | Pair e1 e2
-  | AllocN e1 e2 | FreeN e1 e2 | Store _ e1 e2 | FAA e1 e2 =>
-     free_vars e1 ∪ free_vars e2
-  | If e0 e1 e2 | CmpXchg e0 e1 e2 =>
-     free_vars e0 ∪ free_vars e1 ∪ free_vars e2
-  end.
-
-(* Just fill with any value, it does not make a difference. *)
-Definition free_vars_ectx (K : ectx) : gset string :=
-  free_vars (fill K #()).
-
-Local Lemma binder_delete_eq x y (xs1 xs2 : gmap string val) :
-  (if y is BNamed s then s ≠ x → xs1 !! x = xs2 !! x else xs1 !! x = xs2 !! x) →
-  binder_delete y xs1 !! x = binder_delete y xs2 !! x.
-Proof.
-  destruct y as [|s]; first done. simpl.
-  destruct (decide (s = x)) as [->|Hne].
-  - rewrite !lookup_delete //.
-  - rewrite !lookup_delete_ne //. eauto.
-Qed.
-
-Lemma subst_map_free_vars (xs1 xs2 : gmap string val) (e : expr) :
-  (∀ x, x ∈ free_vars e → xs1 !! x = xs2 !! x) →
-  subst_map xs1 e = subst_map xs2 e.
-Proof.
-  revert xs1 xs2; induction e=>/= xs1 xs2 Heq;
-  solve [
-    (* trivial cases *)
-    done
-  | (* variable case *)
-    rewrite Heq; [done|set_solver]
-  | (* recursive cases *)
-    f_equal;
-    repeat lazymatch goal with x : binder |- _ => destruct x end;
-    intuition eauto using binder_delete_eq with set_solver
-  ].
-Qed.
-
-Lemma subst_map_closed xs e :
-  free_vars e = ∅ →
-  subst_map xs e = e.
-Proof.
-  intros Hclosed.
-  trans (subst_map ∅ e).
-  - apply subst_map_free_vars. rewrite Hclosed. done.
-  - apply subst_map_empty.
-Qed.
-
-Lemma subst_free_vars x v e :
-  x ∉ free_vars e →
-  subst x v e = e.
-Proof.
-  intros Hfree.
-  rewrite -(subst_map_empty (subst x v e)).
-  rewrite subst_map_subst.
-  rewrite (subst_map_free_vars _ ∅); first by apply subst_map_empty.
-  intros y ?. rewrite lookup_insert_ne //. set_solver.
-Qed.
-
-Lemma free_vars_subst x v e :
-  free_vars (subst x v e) = free_vars e ∖ {[x]}.
-Proof.
-  induction e=>/=; repeat case_decide; set_solver.
-Qed.
-
-Lemma free_vars_subst_map xs e :
-  free_vars (subst_map xs e) = free_vars e ∖ (dom _ xs).
-Proof.
-  induction xs as [| x v xs HNone IH] using map_ind.
-  - rewrite subst_map_empty. set_solver.
-  - rewrite -subst_subst_map delete_notin // free_vars_subst IH. set_solver.
-Qed.
-
-Lemma free_vars_fill K e :
-  free_vars (fill K e) = free_vars_ectx K ∪ free_vars e.
-Proof.
-  revert e. induction K as [|Ki K IH] using rev_ind; intros e; simpl.
-  { simpl. rewrite /free_vars_ectx /= left_id_L. done. }
-  rewrite /free_vars_ectx !fill_app /=. destruct Ki; simpl.
-  all: rewrite !IH; set_solver+.
-Qed.
diff --git a/theories/simplang/primitive_laws.v b/theories/simplang/primitive_laws.v
index 40b85ef7a3ab2e612f7f9e478309108c353de35d..3b5a883b7607b0c975e52acb7e4bc0a639dd59a8 100644
--- a/theories/simplang/primitive_laws.v
+++ b/theories/simplang/primitive_laws.v
@@ -20,16 +20,16 @@ Class sheapGS (Σ: gFunctors) := SHeapGS {
   (* These instances need to have a lower priority than the sheapGpreS
   instances as otherwise the statement of [simplang_adequacy] uses the
   wrong instance. *)
-  sheapG_gen_progG :> gen_sim_progGS string ectx ectx Σ | 1;
+  sheapG_gen_progG :> gen_sim_progGS string (string*expr) (string*expr) Σ | 1;
   sheapG_heapG :> heapG Σ | 1;
   sheapG_heap_target : heap_names;
   sheapG_heap_source : heap_names;
 }.
 Class sheapGpreS (Σ: gFunctors) := SHeapGpreS {
   sbij_pre_heapG :> heapG Σ | 10;
-  sbij_pre_progG :> gen_progGpreS Σ string ectx | 10;
+  sbij_pre_progG :> gen_progGpreS Σ string (string*expr) | 10;
 }.
-Definition sheapΣ := #[heapΣ; gen_progΣ string ectx].
+Definition sheapΣ := #[heapΣ; gen_progΣ string (string*expr)].
 Global Instance subG_sheapΣ Σ :
   subG sheapΣ Σ → sheapGpreS Σ.
 Proof. solve_inG. Qed.
@@ -216,9 +216,9 @@ Lemma sheap_init `{!sheapGpreS Σ} P_t gs_t P_s gs_s T_s :
   ⊢@{iPropI Σ} |==> ∃ `(!sheapGS Σ), ∀ `(!sheapInv Σ),
     (sheap_inv P_s (state_init gs_s) T_s -∗
       state_interp P_t (state_init gs_t) P_s (state_init gs_s) T_s) ∗
-    ([∗ map] f ↦ K ∈ P_t, f @t K) ∗
+    ([∗ map] f ↦ fn ∈ P_t, f @t fn) ∗
     ([∗ map] n ↦ v ∈ gs_t, global_loc n ↦t v ∗ target_block_size (global_loc n) (Some 1)) ∗
-    ([∗ map] f ↦ K ∈ P_s, f @s K) ∗
+    ([∗ map] f ↦ fn ∈ P_s, f @s fn) ∗
     ([∗ map] n ↦ v ∈ gs_s, global_loc n ↦s v ∗ source_block_size (global_loc n) (Some 1)) ∗
     source_globals (dom _ gs_s) ∗ target_globals (dom _ gs_t) ∗
     progs_are P_t P_s.
@@ -547,9 +547,9 @@ Proof.
 Qed.
 
 (** operational lemmas for calls *)
-Lemma target_red_call f K_t v Ψ :
-  f @t K_t -∗
-  target_red (fill K_t (Val v)) Ψ -∗
+Lemma target_red_call f x e v Ψ :
+  f @t (x, e) -∗
+  target_red (subst x v e) Ψ -∗
   target_red (Call (Val $ LitV $ LitFn f) (Val v)) Ψ.
 Proof.
   iIntros "Hf Hred". iApply target_red_lift_head_step.
@@ -560,9 +560,9 @@ Proof.
   iModIntro. by iFrame.
 Qed.
 
-Lemma source_red_call π f K_s v Ψ :
-  f @s K_s -∗
-  source_red (fill K_s (Val v)) π Ψ -∗
+Lemma source_red_call π f x e v Ψ :
+  f @s (x, e) -∗
+  source_red (subst x v e) π Ψ -∗
   source_red (Call (Val $ LitV $ LitFn f) (Val v)) π Ψ.
 Proof.
   iIntros "Hf Hred". iApply source_red_lift_head_step.
@@ -634,11 +634,11 @@ Proof.
 Qed.
 
 
-Lemma sim_while_rec b_t c_t v_s (K_s : ectx) (inv : val → iProp Σ) Ψ rec_n π :
+Lemma sim_while_rec b_t c_t v_s x_s (body_s : expr) (inv : val → iProp Σ) Ψ rec_n π :
   inv v_s -∗
-  rec_n @s K_s -∗
+  rec_n @s (x_s, body_s) -∗
   □ (∀ v_s', inv v_s' -∗
-    (if: c_t then b_t ;; while: c_t do b_t od else #())%E ⪯{π} (fill K_s v_s')%E
+    (if: c_t then b_t ;; while: c_t do b_t od else #())%E ⪯{π} (subst x_s v_s' body_s)%E
     [{ λ e_t e_s , Ψ e_t e_s ∨ (∃ v_s', ⌜e_t = while: c_t do b_t od%E⌝ ∗ ⌜e_s = Call f#rec_n (Val v_s')⌝ ∗ inv v_s') }]) -∗
   (while: c_t do b_t od ⪯{π} Call f#rec_n v_s [{ Ψ }])%E.
 Proof.
@@ -648,7 +648,7 @@ Proof.
   iSpecialize ("Hstep" with "Hinv").
   iModIntro. iSplitR; first by eauto with head_step.
   iIntros (e_t' efs σ_t') "%Hhead"; inv_head_step.
-  iModIntro. iExists (fill K_s v_s'), σ_s.
+  iModIntro. iExists (subst x_s v_s' body_s), σ_s.
 
   iDestruct (has_prog_has_fun_agree with "HP_s Hrec") as %?.
   iFrame. iSplitR; [done|].
@@ -657,11 +657,11 @@ Proof.
   apply: fill_prim_step. apply: head_prim_step. by constructor.
 Qed.
 
-Lemma sim_rec_while b_s c_s v_t (K_t : ectx) (inv : val → iProp Σ) Ψ rec_n π :
+Lemma sim_rec_while b_s c_s v_t x_t (body_t : expr) (inv : val → iProp Σ) Ψ rec_n π :
   inv v_t -∗
-  rec_n @t K_t -∗
+  rec_n @t (x_t, body_t) -∗
   □ (∀ v_t', inv v_t' -∗
-    (fill K_t v_t')%E ⪯{π}  (if: c_s then b_s ;; while: c_s do b_s od else #())%E
+    (subst x_t v_t' body_t)%E ⪯{π}  (if: c_s then b_s ;; while: c_s do b_s od else #())%E
     [{ λ e_t e_s , Ψ e_t e_s ∨ (∃ v_t', ⌜e_t = Call f#rec_n (Val v_t')⌝ ∗ ⌜e_s = while: c_s do b_s od%E⌝ ∗  inv v_t') }]) -∗
   ( Call f#rec_n v_t ⪯{π} while: c_s do b_s od [{ Ψ }])%E.
 Proof.
@@ -682,12 +682,12 @@ Proof.
   apply: fill_prim_step. apply: head_prim_step. by constructor.
 Qed.
 
-Lemma sim_rec_rec v_t v_s (K_t K_s : ectx) (inv : val → val → iProp Σ) Ψ rec_t rec_s π :
+Lemma sim_rec_rec v_t v_s x_t x_s (body_t body_s : expr) (inv : val → val → iProp Σ) Ψ rec_t rec_s π :
   inv v_t v_s -∗
-  rec_t @t K_t -∗
-  rec_s @s K_s -∗
+  rec_t @t (x_t, body_t) -∗
+  rec_s @s (x_s, body_s) -∗
   □ (∀ v_t' v_s', inv v_t' v_s' -∗
-    (fill K_t v_t')%E ⪯{π} (fill K_s v_s')%E
+    (subst x_t v_t' body_t)%E ⪯{π} (subst x_s v_s' body_s)%E
     [{ λ e_t e_s , Ψ e_t e_s ∨ (∃ v_t' v_s', ⌜e_t = Call f#rec_t (Val v_t')⌝ ∗ ⌜e_s = Call f#rec_s (Val v_s')⌝ ∗ inv v_t' v_s') }]) -∗
   ( Call f#rec_t v_t ⪯{π} Call f#rec_s v_s [{ Ψ }])%E.
 Proof.
diff --git a/theories/simplang/proofmode.v b/theories/simplang/proofmode.v
index 1e4dcaee0c9df884941e8072afcacb94b6269f3c..d6bca0d238e3f0222093f2363b623e99d64b7dc1 100644
--- a/theories/simplang/proofmode.v
+++ b/theories/simplang/proofmode.v
@@ -372,9 +372,9 @@ Proof.
   rewrite Hi. iIntros "Hs". iApply source_red_base; eauto.
 Qed.
 
-Lemma tac_target_red_call Δ i K b f v K_t Ψ :
-  envs_lookup i Δ = Some (b, f @t K_t)%I →
-  envs_entails Δ (target_red (fill K (fill K_t (Val v))) Ψ) →
+Lemma tac_target_red_call Δ i K b f v x e Ψ :
+  envs_lookup i Δ = Some (b, f @t (x, e))%I →
+  envs_entails Δ (target_red (fill K (subst x v e)) Ψ) →
   envs_entails Δ (target_red (fill K (Call (Val $ LitV $ LitFn f) (Val v))) Ψ).
 Proof.
   rewrite envs_entails_eq=> ? Hi.
@@ -387,9 +387,9 @@ Proof.
     iApply target_red_base. iSpecialize ("Hs" with "Hf"); eauto.
 Qed.
 
-Lemma tac_source_red_call π Δ i K b f v K_s Ψ :
-  envs_lookup i Δ = Some (b, f @s K_s)%I →
-  envs_entails Δ (source_red (fill K (fill K_s (Val v))) π Ψ) →
+Lemma tac_source_red_call π Δ i K b f v x e Ψ :
+  envs_lookup i Δ = Some (b, f @s (x, e))%I →
+  envs_entails Δ (source_red (fill K (subst x v e)) π Ψ) →
   envs_entails Δ (source_red (fill K (Call (Val $ LitV $ LitFn f) (Val v))) π Ψ).
 Proof.
   rewrite envs_entails_eq=> ? Hi.
diff --git a/theories/simplang/pure_refl.v b/theories/simplang/pure_refl.v
index dde6648967f6f1af6869bbab0adc4dff931127c9..7b2a818ce13508dabe04a47141dc59bf6f0945c8 100644
--- a/theories/simplang/pure_refl.v
+++ b/theories/simplang/pure_refl.v
@@ -1,6 +1,6 @@
 From simuliris.simulation Require Import slsls lifting.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import parallel_subst primitive_laws gen_val_rel gen_log_rel wf gen_refl globalbij.
+From simuliris.simplang Require Import primitive_laws gen_val_rel gen_log_rel wf gen_refl globalbij.
 From iris.prelude Require Import options.
 
 (** * Reflexivity theorem for pure expressions
diff --git a/theories/simplang/simple_inv/adequacy.v b/theories/simplang/simple_inv/adequacy.v
index 035fbe8ba1e977ccf1d201bcf70d8d823c514548..b51705efa90f4b1eea28453c5129c878e4140efc 100644
--- a/theories/simplang/simple_inv/adequacy.v
+++ b/theories/simplang/simple_inv/adequacy.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import gset_bij.
 From simuliris.logic Require Import satisfiable.
 From simuliris.simulation Require Import slsls global_sim.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import gen_adequacy behavior wf parallel_subst gen_refl.
+From simuliris.simplang Require Import gen_adequacy behavior wf gen_refl.
 From simuliris.simplang.simple_inv Require Import inv refl.
 From iris.prelude Require Import options.
 
@@ -58,25 +58,27 @@ Proof.
   apply (prog_rel_adequacy Σ). eapply isat_intro.
   iIntros (? gs Hgs) "_ _ _ _ !#".
   iSplit. { iApply big_sepM_intro. iIntros "!>" (???). iApply val_wf_sound. by apply: Hgs. }
-  iIntros "!# %f %K_s %π".
+  rewrite /prog_rel.
+  iIntros "!# %f %arg %body".
   iDestruct (Hrel _) as "Hrel". clear Hrel.
   destruct (decide (f = fname)) as [->|Hne].
   - rewrite !lookup_insert.
-    iIntros ([= <-]). iExists _. iSplitR; first done.
+    iIntros ([= <- <-]). iExists _, _. iSplitR; first done.
     (* TODO Factor this into a general lemma? *)
-    iIntros (v_t v_s) "#Hval /=".
-    iApply log_rel_closed_1.
-    { simpl. set_solver. }
-    iApply log_rel_let.
-    { iApply log_rel_val. done. }
-    iApply log_rel_ctx; done.
+    iIntros (v_t v_s π) "#Hval /=".
+    iApply sim_wand.
+    + iApply (gen_log_rel_singleton with "[Hrel] Hval []"); first done.
+      * by iApply log_rel_ctx.
+      * done.
+    + simpl. iIntros (??). rewrite left_id. auto.
   - rewrite !lookup_insert_ne //.
-    iIntros (Hf). rename K_s into K. iExists K. iSplit; first done.
+    iIntros (Hf). iExists arg, body. iSplit; first done.
     specialize (Hpwf _ _ Hf). destruct Hpwf as [HKwf HKclosed].
     (* TODO Factor this into a lemma? *)
-    iIntros (v_t v_s) "#Hval /=".
-    iApply log_rel_closed_1.
-    { rewrite !free_vars_fill HKclosed. set_solver+. }
-    iApply log_rel_ectx; first done.
-    iApply log_rel_val; done.
+    iIntros (v_t v_s π) "#Hval /=".
+    iApply sim_wand.
+    + iApply (gen_log_rel_singleton with "[Hrel] Hval []"); first set_solver.
+      * by iApply log_rel_refl.
+      * done.
+    + simpl. iIntros (??). rewrite left_id. auto.
 Qed.
diff --git a/theories/simplang/simple_inv/refl.v b/theories/simplang/simple_inv/refl.v
index 22a8a14ce6d762baba097cd73e6420c8dfe65821..c26db7900447901bf84021b3d4e647085ab288f5 100644
--- a/theories/simplang/simple_inv/refl.v
+++ b/theories/simplang/simple_inv/refl.v
@@ -1,6 +1,6 @@
 From simuliris.simulation Require Import slsls lifting.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import parallel_subst gen_log_rel wf gen_refl pure_refl.
+From simuliris.simplang Require Import gen_log_rel wf gen_refl pure_refl.
 From simuliris.simplang.simple_inv Require Import inv.
 From iris.prelude Require Import options.
 
@@ -74,20 +74,4 @@ Section refl.
     intros ?. iApply gen_log_rel_ctx; first by apply simple_log_rel_structural. done.
   Qed.
 
-  Corollary log_rel_ectx K e_t e_s :
-    ectx_wf K →
-    log_rel e_t e_s -∗ log_rel (fill K e_t) (fill K e_s).
-  Proof.
-    intros ?. iApply gen_log_rel_ectx; first by apply simple_log_rel_structural. done.
-  Qed.
-
-  Lemma log_rel_closed_1 e_t e_s π :
-    free_vars e_t ∪ free_vars e_s = ∅ →
-    log_rel e_t e_s ⊢ e_t ⪯{π} e_s {{ λ v_t v_s, val_rel v_t v_s }}.
-  Proof.
-    iIntros (?) "#Hrel".
-    iApply sim_mono; last iApply (gen_log_rel_closed_1 with "Hrel"); [|done..].
-    iIntros (v_t v_s) "[_ $]".
-  Qed.
-
 End refl.
diff --git a/theories/simplang/tactics.v b/theories/simplang/tactics.v
index e76dd32c0a7ab36f1e0ba75d04afbb02752052b5..05de56a767f0ca64022261546b42a3470407b0db 100644
--- a/theories/simplang/tactics.v
+++ b/theories/simplang/tactics.v
@@ -1,5 +1,5 @@
-From stdpp Require Import fin_maps.
-From simuliris.simplang Require Import lang parallel_subst notation.
+From stdpp Require Import fin_maps fin_map_dom.
+From simuliris.simplang Require Import lang notation.
 From iris.prelude Require Import options.
 
 
@@ -349,7 +349,7 @@ Module W.
   end.
 
   Lemma to_expr_is_closed xs e:
-    is_closed xs e → parallel_subst.free_vars (to_expr e) ⊆ list_to_set xs.
+    is_closed xs e → language.free_vars (to_expr e) ⊆ list_to_set xs.
   Proof.
     elim: e xs => [^ e] //= xs Hx.
     all: destruct_and?.
@@ -360,7 +360,7 @@ Module W.
   Qed.
 
   Lemma to_expr_is_closed_empty e:
-    is_closed [] e → parallel_subst.free_vars (to_expr e) = ∅.
+    is_closed [] e → language.free_vars (to_expr e) = ∅.
   Proof. move => /to_expr_is_closed. set_solver. Qed.
 
 End W.
diff --git a/theories/simulation/adequacy.v b/theories/simulation/adequacy.v
index 7cceb804e5928e7fcf213a7a51bfd7e1fce1f9f7..bd1ba68f64102f98bce9269afd1b2ec3e614ee13 100644
--- a/theories/simulation/adequacy.v
+++ b/theories/simulation/adequacy.v
@@ -329,7 +329,7 @@ Section adequacy_statement.
   Proof.
     intros Hsat σ_t σ_s HI Hsafe.
     eapply (safe_call_in_prg p_s empty_ectx _ _ _ main) in Hsafe as Hlook; last (rewrite fill_empty; constructor).
-    destruct Hlook as [K_s Hlook].
+    destruct Hlook as (x_s & e_s & Hlook).
     eapply (sat_forall _ σ_t) in Hsat.
     eapply (sat_forall _ σ_s) in Hsat.
     eapply sat_wand in Hsat; [| by iPureIntro].
@@ -340,7 +340,7 @@ Section adequacy_statement.
       iIntros "(Hloc & SI & Hprogs & Hunit & $)". iFrame.
       iSplit; first by iPureIntro; intros ??; set_solver.
       simpl. iSplit; last done.
-      iApply (local_to_global_call with "Hloc Hprogs Hunit"); eauto. }
+      iApply (local_to_global_call with "Hloc Hprogs Hunit"); eauto.  }
     split; last split.
     - intros Hfair. eapply (msim_fair_divergence (sat:=sat_frame _)); eauto.
     - intros v_t T_t σ_t' J Hsteps.
diff --git a/theories/simulation/global_sim.v b/theories/simulation/global_sim.v
index 579714ad61319c1cf8732cb6b8c2f541f7ee7aaa..7819680b80801e51210bbf9b6aa5dac99175d67e 100644
--- a/theories/simulation/global_sim.v
+++ b/theories/simulation/global_sim.v
@@ -21,7 +21,10 @@ Section fix_lang.
     (σ_s σ_t σ : state Λ).
 
   Definition prog_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 (ext_rel π))%I.
+    (□ ∀ f x_s e_s, ⌜P_s !! f = Some (x_s, e_s)⌝ →
+       ∃ x_t e_t, ⌜P_t !! f = Some (x_t, e_t)⌝ ∗
+         ∀ v_t v_s π, ext_rel π v_t v_s -∗
+           (subst_map {[x_t:=v_t]} e_t) ⪯{π} (subst_map {[x_s:=v_s]} e_s) {{ ext_rel π }})%I.
   Typeclasses Opaque prog_rel.
 
   Global Instance prog_rel_persistent P_s P_t : Persistent (prog_rel P_s P_t).
@@ -660,18 +663,18 @@ Section fix_lang.
     iDestruct "Hsim" as (f K_t v_t K_s' v_s σ_s') "(% & %Hnfs & Hval & Hstate & Hcont)".
     subst e_t. iRight.
     (* the function is in the source table *)
-    edestruct (@safe_call_in_prg Λ) as [K_f_s Hdef_s]; [ |done|].
+    edestruct (@safe_call_in_prg Λ) as (x_f_s & e_f_s & Hdef_s); [ |done|].
     { eapply fill_safe. by eapply pool_safe_threads_safe. }
 
     (* we prove reducibility and the step case *)
     iSplit.
-    - iAssert (∃ K_f_t, ⌜P_t !! f = Some K_f_t⌝)%I as (K_f_t) "%".
-      { iDestruct ("Hloc" $! _ _ π Hdef_s) as (K_f_t) "[% _]"; by eauto. }
+    - iAssert (∃ x_f_t e_f_t, ⌜P_t !! f = Some (x_f_t, e_f_t)⌝)%I as (x_f_t e_f_t) "%".
+      { iDestruct ("Hloc" $! _ _ _ Hdef_s) as (x_f_t e_f_t) "[% _]"; by eauto. }
       iPureIntro. eexists _, _, _.
       by apply fill_prim_step, head_prim_step, call_head_step_intro.
     - iIntros (e_t' efs_t σ_t' Hstep).
-      apply prim_step_call_inv in Hstep as (K_f_t & Hdef & -> & -> & ->).
-      iModIntro. iRight. iExists (fill K_s' (of_call f v_s)), (fill K_s' (fill K_f_s (of_val v_s))), σ_s', σ_s', [].
+      apply prim_step_call_inv in Hstep as (x_f_t & e_f_t & Hdef & -> & -> & ->).
+      iModIntro. iRight. iExists (fill K_s' (of_call f v_s)), (fill K_s' (subst_map {[x_f_s:=v_s]} e_f_s)), σ_s', σ_s', [].
       iFrame. iSplit; first done. iSplit.
       { iPureIntro. by apply fill_prim_step, head_prim_step, call_head_step_intro. }
       iSplit; first done.
@@ -682,8 +685,10 @@ Section fix_lang.
         intros σ_s''. eapply fill_prim_step, fill_prim_step. by eapply head_prim_step, call_head_step_intro.
       }
       simpl; iSplit; last done.
-      iApply sim_expr_bind. iDestruct ("Hloc" $! _ _ _ Hdef_s) as (K_f_t') "[% Hectx]".
-      replace K_f_t' with K_f_t by naive_solver. rewrite /sim_ectx.
+      iApply sim_expr_bind. iDestruct ("Hloc" $! _ _ _ Hdef_s) as (x_f_t' e_f_t') "[% Hectx]".
+      replace x_f_t' with x_f_t by naive_solver.
+      replace e_f_t' with e_f_t by naive_solver.
+      rewrite /sim_ectx.
       iApply (sim_expr_mono with "[-Hval] [Hval]"); last by iApply "Hectx".
       iIntros (e_t' e_s'). iDestruct 1 as (v_t' v_s' -> ->) "Hval".
       rewrite sim_expr_eq. by iApply "Hcont".
@@ -696,11 +701,14 @@ Section fix_lang.
     ext_rel π v_t v_s -∗
     gsim_expr (lift_post (ext_rel π)) π (of_call f v_t) (of_call f v_s).
   Proof.
-    iIntros ([K_s Hlook]) "#Hloc #Hprogs Hval".
+    iIntros ([[x_s e_s] Hlook]) "#Hloc #Hprogs Hval".
     iApply (local_to_global with "Hloc Hprogs").
     rewrite /prog_rel.
     iDestruct "Hloc" as "#Hloc".
-    iDestruct ("Hloc" $! _ _ _ Hlook) as (K_t) "[% Hsim]".
-    iApply sim_call_inline; last (iFrame; iSplit; first done); eauto.
+    iDestruct ("Hloc" $! _ _ _ Hlook) as (x_t e_t) "[% Hsim]".
+    iApply (sim_call_inline with "[$] Hval"); eauto.
+    iIntros (??) "Hrel". iApply "Hsim". done.
   Qed.
 End fix_lang.
+
+Typeclasses Opaque prog_rel.
diff --git a/theories/simulation/language.v b/theories/simulation/language.v
index 89028c7720277ef20b1ee36b308a14976b40d536..2876244bb433b2899fee099bb68aaa97873a413f 100644
--- a/theories/simulation/language.v
+++ b/theories/simulation/language.v
@@ -20,22 +20,35 @@ Section language_mixin.
   Context (comp_ectx : ectx → ectx → ectx).
   Context (fill : ectx → expr → expr).
 
-  (** A program is a map from function names to function bodies. *)
-  Local Notation mixin_prog := (gmap string ectx).
+  Context (subst_map : gmap string val → expr → expr).
+  Context (free_vars : expr → gset string).
+
+  (** A program is a map from function names to function bodies.
+      A function body is a string (the argument name) and the function code. *)
+  Local Notation mixin_prog := (gmap string (string * expr)).
 
   Context (head_step : mixin_prog → expr → state → expr → state → list expr → Prop).
 
   Record LanguageMixin := {
+    (** Expression classification *)
     mixin_to_of_class c : to_class (of_class c) = Some c;
     mixin_of_to_class e c : to_class e = Some c → of_class c = e;
 
+    (** Reduction behavior of the special classes of expressions *)
     (** mixin_val_head_step is not an iff because the backward direction is trivial *)
     mixin_val_head_step p v σ1 e2 σ2 efs :
       head_step p (of_class (ExprVal v)) σ1 e2 σ2 efs → False;
     mixin_call_head_step p f v σ1 e2 σ2 efs :
       head_step p (of_class (ExprCall f v)) σ1 e2 σ2 efs ↔
-      ∃ K, p !! f = Some K ∧ e2 = fill K (of_class (ExprVal v)) ∧ σ2 = σ1 ∧ efs = [];
+      ∃ (x : string) (e : expr),
+        p !! f = Some (x, e) ∧ e2 = subst_map {[x:=v]} e ∧ σ2 = σ1 ∧ efs = [];
+
+    (** Substitution and free variables *)
+    mixin_subst_map_free_vars (xs1 xs2 : gmap string val) (e : expr) :
+      (∀ x, x ∈ free_vars e → xs1 !! x = xs2 !! x) →
+      subst_map xs1 e = subst_map xs2 e;
 
+    (** Evaluation contexts *)
     mixin_fill_empty e : fill empty_ectx e = e;
     mixin_fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
     mixin_fill_inj K : Inj (=) (=) (fill K);
@@ -69,7 +82,7 @@ Section language_mixin.
 End language_mixin.
 
 Arguments mixin_expr_class : clear implicits.
-Local Notation mixin_prog ectx := (gmap string ectx).
+Local Notation mixin_prog expr := (gmap string (string * expr)).
 
 Structure language := Language {
   expr : Type;
@@ -82,10 +95,12 @@ Structure language := Language {
   empty_ectx : ectx;
   comp_ectx : ectx → ectx → ectx;
   fill : ectx → expr → expr;
-  head_step : mixin_prog ectx → expr → state → expr → state → list expr → Prop;
+  subst_map : gmap string val → expr → expr;
+  free_vars : expr → gset string;
+  head_step : mixin_prog expr → expr → state → expr → state → list expr → Prop;
 
   language_mixin :
-    LanguageMixin (val:=val) of_class to_class empty_ectx comp_ectx fill head_step
+    LanguageMixin (val:=val) of_class to_class empty_ectx comp_ectx fill subst_map free_vars head_step
 }.
 
 Declare Scope expr_scope.
@@ -94,16 +109,18 @@ Bind Scope expr_scope with expr.
 Declare Scope val_scope.
 Bind Scope val_scope with val.
 
-Arguments Language {_ _ _ _ _ _ _ _ _ _} _.
+Arguments Language {expr _ _ _ _ _ _ _ _ _ free_vars head_step}.
 Arguments of_class {_} _.
 Arguments to_class {_} _.
 Arguments empty_ectx {_}.
 Arguments comp_ectx {_} _ _.
 Arguments fill {_} _ _.
+Arguments subst_map {_}.
+Arguments free_vars {_}.
 Arguments head_step {_} _ _ _ _ _ _.
 
 Definition expr_class (Λ : language) := mixin_expr_class Λ.(val).
-Definition prog (Λ : language) := (mixin_prog Λ.(ectx)).
+Definition prog (Λ : language) := (mixin_prog Λ.(expr)).
 
 Definition to_val {Λ : language} (e : expr Λ) :=
   match to_class e with
@@ -148,7 +165,7 @@ Section language.
   Proof. apply language_mixin. Qed.
   Lemma call_head_step p f v σ1 e2 σ2 efs :
     head_step p (of_class (ExprCall f v)) σ1 e2 σ2 efs ↔
-    ∃ K, p !! f = Some K ∧ e2 = fill K (of_class (ExprVal v)) ∧ σ2 = σ1 ∧ efs = nil.
+    ∃ x e, p !! f = Some (x, e) ∧ e2 = subst_map {[x:=v]} e ∧ σ2 = σ1 ∧ efs = nil.
   Proof. apply language_mixin. Qed.
 
   Lemma fill_empty e : fill empty_ectx e = e.
@@ -193,11 +210,11 @@ Section language.
   Qed.
   Lemma call_head_step_inv p f v σ1 e2 σ2 efs :
     head_step p (of_class (ExprCall f v)) σ1 e2 σ2 efs →
-    ∃ K, p !! f = Some K ∧ e2 = fill K (of_class (ExprVal v)) ∧ σ2 = σ1 ∧ efs = [].
+    ∃ x e, p !! f = Some (x, e) ∧ e2 = subst_map {[x:=v]} e ∧ σ2 = σ1 ∧ efs = nil.
   Proof. eapply call_head_step. Qed.
-  Lemma call_head_step_intro p f v K σ1 :
-    p !! f = Some K →
-    head_step p (of_call f v) σ1 (fill K (of_val v)) σ1 [].
+  Lemma call_head_step_intro p f v x e σ1 :
+    p !! f = Some (x, e) →
+    head_step p (of_call f v) σ1 (subst_map {[x:=v]} e) σ1 [].
   Proof. intros ?. eapply call_head_step; eexists; eauto. Qed.
 
   Definition head_reducible (p : prog Λ) (e : expr Λ) (σ : state Λ) :=
@@ -400,7 +417,7 @@ Section language.
 
   Lemma prim_step_call_inv p K f v e' σ σ' efs :
     prim_step p (fill K (of_call f v)) σ e' σ' efs →
-    ∃ K_f, p !! f = Some K_f ∧ e' = fill K (fill K_f (of_val v)) ∧ σ' = σ ∧ efs = [].
+    ∃ x_f e_f, p !! f = Some (x_f, e_f) ∧ e' = fill K (subst_map {[x_f:=v]} e_f) ∧ σ' = σ ∧ efs = [].
   Proof.
     intros (K' & e1 & e2 & Hctx & -> & Hstep)%prim_step_inv.
     eapply step_by_val in Hstep as H'; eauto; last apply to_val_of_call.
@@ -409,8 +426,8 @@ Section language.
     destruct (fill_class K'' e1) as [->|Hval].
     - apply is_call_is_class. erewrite of_to_call_flip; eauto.
     - rewrite fill_empty in Hctx. subst e1.
-      apply call_head_step_inv in Hstep as (K_f & ? & -> & -> & ->).
-      exists K_f. rewrite -fill_comp fill_empty. naive_solver.
+      apply call_head_step_inv in Hstep as (x_f & e_f & ? & -> & -> & ->).
+      exists x_f, e_f. rewrite -fill_comp fill_empty. naive_solver.
     - unfold is_Some in Hval. erewrite val_head_stuck in Hval; naive_solver.
   Qed.
 
@@ -785,9 +802,9 @@ Section language.
     pool_safe p T σ →
     pool_steps p T σ I T' σ' →
     T' !! i = Some (fill K (of_call f v)) →
-    ∃ K', p !! f = Some K'.
+    ∃ x' e', p !! f = Some (x', e').
   Proof.
-    destruct (p !! f) eqn: Hloook; eauto.
+    destruct (p !! f) as [[x' e']|] eqn: Hloook; first by eauto.
     intros Hsafe Hsteps Hlook. exfalso; eapply Hsafe.
     exists T', σ', I; split; first done.
     exists (fill K (of_call f v)), i.
@@ -796,7 +813,7 @@ Section language.
     intros  e'' σ'' efs Hstep.
     pose proof (prim_step_call_inv p empty_ectx f v e'' σ' σ'' efs) as Hinv.
     rewrite fill_empty in Hinv.
-    eapply Hinv in Hstep as (K_f & Hprg & _); naive_solver.
+    eapply Hinv in Hstep as (x_f & e_f & Hprg & _); naive_solver.
   Qed.
 
 
@@ -930,7 +947,7 @@ Section language.
   Qed.
 
   Lemma safe_call_in_prg p K e σ σ' f v:
-    safe p e σ → no_forks p e σ (fill K (of_call f v)) σ' → ∃ K, p !! f = Some K.
+    safe p e σ → no_forks p e σ (fill K (of_call f v)) σ' → ∃ x e, p !! f = Some (x, e).
   Proof.
     intros H1 (I & Hsteps)%no_forks_pool_steps_single_thread.
     eapply (pool_safe_call_in_prg _ _ _ _ 0) in Hsteps; eauto.
diff --git a/theories/simulation/slsls.v b/theories/simulation/slsls.v
index 09f50bff5f017e68c34f7c947c67b6601f4c924f..0a6be10fb7c1a0541097c0e60f8fdfda15cf322a 100644
--- a/theories/simulation/slsls.v
+++ b/theories/simulation/slsls.v
@@ -127,7 +127,7 @@ Section fix_lang.
         ⌜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'⌝ ∗
         ext_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, ext_rel π  v_t v_s -∗ greatest_rec Φ π (fill K_t (of_val v_t)) (fill K_s' (of_val v_s)) ))
+        (∀ v_t v_s, ext_rel π v_t v_s -∗ greatest_rec Φ π (fill K_t (of_val v_t)) (fill K_s' (of_val v_s)) ))
     )%I.
 
 
@@ -349,6 +349,7 @@ Section fix_lang.
     rewrite /sim_expr_ectx sim_expr_fixpoint /sim_expr_inner //.
   Qed.
 
+  (* FIXME: should use [pointwise_relation] *)
   Global Instance sim_expr_ne:
     NonExpansive4 (sim_expr: expr_rel → thread_id → expr_rel).
   Proof. rewrite sim_expr_eq. apply _. Qed.
@@ -360,6 +361,20 @@ Section fix_lang.
     rewrite !sim_expr_eq. eapply greatest_def_proper; done.
   Qed.
 
+  (* FIXME: should use [pointwise_relation] *)
+  Global Instance sim_ne:
+    NonExpansive4 (sim: (val Λ -d> val Λ -d> PROP) → thread_id → expr_rel).
+  Proof.
+    intros ? ?? Hpost ??? ??? ???. apply sim_expr_ne; [|done..].
+    rewrite /lift_post => ??. repeat f_equiv. apply Hpost.
+  Qed.
+
+  Global Instance sim_proper:
+    Proper ((pointwise_relation (val Λ) (pointwise_relation (val Λ) (≡))) ==> eq ==> eq ==> eq ==> (≡)) (sim).
+  Proof.
+    intros ?? Hpost ??? ??? ???. apply sim_expr_proper; [|done..].
+    rewrite /lift_post => ??. repeat f_equiv.
+  Qed.
 
   Existing Instances least_def_body_mono greatest_def_body_mono.
   (* any post-fixed point is included in the gfp *)
@@ -758,12 +773,16 @@ Section fix_lang.
   Qed.
 
   (** Corollaries *)
-  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 ∗ ext_rel π v_t v_s ∗ sim_expr_ectx π K_t K_s Φ -∗ (of_call f v_t) ⪯{π} (of_call f v_s) [{ Φ }].
+  Lemma sim_call_inline P_t P_s v_t v_s x_t x_s e_f_t e_f_s f Φ π :
+    P_t !! f = Some (x_t, e_f_t) →
+    P_s !! f = Some (x_s, e_f_s) →
+    ⊢ progs_are P_t P_s -∗
+      ext_rel π v_t v_s -∗
+      (∀ v'_t v'_s, ext_rel π v'_t v'_s -∗
+        (subst_map {[x_t:=v'_t]} e_f_t) ⪯{π} (subst_map {[x_s:=v'_s]} e_f_s) [{ Φ }]) -∗
+      (of_call f v_t) ⪯{π} (of_call f v_s) [{ Φ }].
  Proof.
-    intros Htgt Hsrc. iIntros "(#Prog & Val & Sim)".
+    intros Htgt Hsrc. iIntros "#Prog Val Sim".
     rewrite sim_expr_unfold. iIntros (P_t' σ_t P_s' σ_s T_s K_s') "[SI [% %]]".
     iModIntro. iRight. iLeft.
     rewrite /progs_are; iDestruct ("Prog" with "SI") as "[% %]"; subst P_t' P_s'; iClear "Prog".
@@ -771,7 +790,7 @@ Section fix_lang.
     - iPureIntro. eapply head_prim_reducible. eexists _, _, _.
       by eapply call_head_step_intro.
     - iIntros (e_t' efs σ_t' Hstep). iModIntro.
-      pose proof (prim_step_call_inv P_t empty_ectx f v_t e_t' σ_t σ_t' efs) as (K_t' & Heq & -> & -> & ->);
+      pose proof (prim_step_call_inv P_t empty_ectx f v_t e_t' σ_t σ_t' efs) as (x_t' & e_f_t' & Heq & -> & -> & ->);
         first by rewrite fill_empty.
       rewrite fill_empty in Hstep. iRight.
       iExists _, _, _, _, _. iSplit; last iSplit; last iSplit; last iSplitL "SI".
@@ -780,7 +799,8 @@ Section fix_lang.
       + done.
       + rewrite app_nil_r. iApply (state_interp_pure_prim_step with "SI"); [done|]. intros ?.
         eapply fill_prim_step. eapply head_prim_step, call_head_step_intro, Hsrc.
-      + rewrite fill_empty; assert (K_t' = K_t) as -> by naive_solver.
+      + rewrite fill_empty. assert (x_t' = x_t) as -> by naive_solver.
+        assert (e_f_t' = e_f_t) as -> by naive_solver.
         iSpecialize ("Sim" with "Val"). simpl. iFrame.
   Qed.