diff --git a/theories/simplang/heap_bij.v b/theories/simplang/heap_bij.v
index 892b4c097f60e06976b9864dafa79b1b3f253e1f..94a70911d31f74b0cfee0448add19725bfd7f347 100644
--- a/theories/simplang/heap_bij.v
+++ b/theories/simplang/heap_bij.v
@@ -43,10 +43,9 @@ Section fix_heap.
       iIntros (e_t' efs σ_t') "%"; inv_head_step.
       assert (head_step P_s (Load #l_s) σ_s (Val v_s) σ_s []) as Hs.
       { eauto with head_step. }
-      iModIntro. iExists (Val v_s), σ_s. iFrame.
+      iModIntro. iExists (Val v_s), [], σ_s. iFrame.
       iSplitR. { by iPureIntro. }
-      iSplitR. { by iPureIntro. }
-      iSplitR "Hsim"; first last. { by iApply "Hsim". }
+      iSplitR "Hsim"; first last. { rewrite /= right_id. by iApply "Hsim". }
       iApply ("Hclose" with "Hl_t Hl_s []"). iLeft; eauto.
     - exfalso; contradict Hnstuck.
       apply stuck_reach_stuck. split; first done.
@@ -73,8 +72,8 @@ Section fix_heap.
 
       iMod (gen_heap_update with "Hσ_t Hl_t") as "[$ Hl_t]".
       iMod (gen_heap_update with "Hσ_s Hl_s") as "[Ha Hl_s]".
-      iModIntro. iExists #(),(state_upd_heap <[l_s:=Some v_s]> σ_s).
-      iFrame. iSplitR; first by iPureIntro. iSplitR; first by iPureIntro.
+      iModIntro. iExists #(), [],(state_upd_heap <[l_s:=Some v_s]> σ_s).
+      iFrame. iSplitR; first by iPureIntro. rewrite /= right_id.
       iApply ("Hclose" with "Hl_t Hl_s [Hval]"). iLeft; eauto.
     - exfalso; contradict Hnstuck.
       apply stuck_reach_stuck. split; first done.
@@ -100,8 +99,8 @@ Section fix_heap.
 
       iMod (gen_heap_update with "Hσ_t Hl_t") as "[$ Hl_t]".
       iMod (gen_heap_update with "Hσ_s Hl_s") as "[Ha Hl_s]".
-      iModIntro. iExists #(),(state_upd_heap <[l_s:=None]> σ_s).
-      iFrame. iSplitR; first by iPureIntro. iSplitR; first by iPureIntro.
+      iModIntro. iExists #(), [],(state_upd_heap <[l_s:=None]> σ_s).
+      iFrame. iSplitR; first by iPureIntro. rewrite /= right_id.
       iApply ("Hclose" with "Hl_t Hl_s"). iRight; eauto.
     - exfalso; contradict Hnstuck.
       apply stuck_reach_stuck. split; first done.
diff --git a/theories/simplang/heapbij_refl.v b/theories/simplang/heapbij_refl.v
index bca8076cea7b334e05889d8e0c432bfcad5b6321..65c283cb7e59ff8f8f3397129dc07d401fd45712 100644
--- a/theories/simplang/heapbij_refl.v
+++ b/theories/simplang/heapbij_refl.v
@@ -55,7 +55,7 @@ Section refl.
     | InjL e => expr_wf e
     | InjR e => expr_wf e
     | Match e x1 e1 x2 e2 => expr_wf e ∧ expr_wf e1 ∧ expr_wf e2
-    | Fork e => False             (* currently not supported *)
+    | Fork e => expr_wf e
     | AllocN e1 e2 => expr_wf e1 ∧ expr_wf e2
     | Free e => expr_wf e
     | Load e => expr_wf e
@@ -107,27 +107,27 @@ Section refl.
   Qed.
 
   Lemma val_rel_val_is_unboxed v_t v_s : val_rel v_t v_s -∗ ⌜val_is_unboxed v_t ↔ val_is_unboxed v_s⌝.
-  Proof. 
-    iIntros "Hv". 
-    destruct v_s as [[] | | | ]; val_discr_source "Hv"; [ done .. | |done | | |]. 
-    - by iPoseProof (val_rel_loc_source with "Hv") as (?) "(-> & _)". 
+  Proof.
+    iIntros "Hv".
+    destruct v_s as [[] | | | ]; val_discr_source "Hv"; [ done .. | |done | | |].
+    - by iPoseProof (val_rel_loc_source with "Hv") as (?) "(-> & _)".
     - by iPoseProof (val_rel_pair_source with "Hv") as (??) "(-> & Hv1 & Hv2)".
     - iPoseProof (val_rel_injl_source with "Hv") as (?) "(-> & Hv)".
       destruct v_s as [[] | | | ]; val_discr_source "Hv"; [done.. | | done | | |].
       + by iPoseProof (val_rel_loc_source with "Hv") as (?) "(-> & _)".
       + by iPoseProof (val_rel_pair_source with "Hv") as (??) "(-> & Hv1 & Hv2)".
-      + by iPoseProof (val_rel_injl_source with "Hv") as (?) "(-> & Hv)". 
-      + by iPoseProof (val_rel_injr_source with "Hv") as (?) "(-> & Hv)". 
+      + by iPoseProof (val_rel_injl_source with "Hv") as (?) "(-> & Hv)".
+      + by iPoseProof (val_rel_injr_source with "Hv") as (?) "(-> & Hv)".
     - iPoseProof (val_rel_injr_source with "Hv") as (?) "(-> & Hv)".
       destruct v_s as [[] | | | ]; val_discr_source "Hv"; [done.. | | done | | |].
       + by iPoseProof (val_rel_loc_source with "Hv") as (?) "(-> & _)".
       + by iPoseProof (val_rel_pair_source with "Hv") as (??) "(-> & Hv1 & Hv2)".
-      + by iPoseProof (val_rel_injl_source with "Hv") as (?) "(-> & Hv)". 
-      + by iPoseProof (val_rel_injr_source with "Hv") as (?) "(-> & Hv)". 
+      + by iPoseProof (val_rel_injl_source with "Hv") as (?) "(-> & Hv)".
+      + by iPoseProof (val_rel_injr_source with "Hv") as (?) "(-> & Hv)".
   Qed.
 
   (** TODO: we need to fix the handling of AllocN in the bijection for this:
-        one option is that we make "blocks of allocation" explicit in the semantics of 
+        one option is that we make "blocks of allocation" explicit in the semantics of
           SimpLang and enforce that all locations in one block are added together.
         pointer arithmetic beyond the last location in the block would then be UB in the source.
 
@@ -177,11 +177,11 @@ Section refl.
       iIntros (v_t1 v_s1) "Hv1".
       destruct op; sim_pures; discr_source; val_discr_source "Hv1"; val_discr_source "Hv2"; sim_pures; [done .. | | ].
       + iAssert (⌜vals_compare_safe v_t1 v_t2⌝)%I as "%".
-        { iPoseProof (val_rel_val_is_unboxed with "Hv1") as "%". 
-          iPoseProof (val_rel_val_is_unboxed with "Hv2") as "%". 
+        { iPoseProof (val_rel_val_is_unboxed with "Hv1") as "%".
+          iPoseProof (val_rel_val_is_unboxed with "Hv2") as "%".
           iPureIntro. by rewrite /vals_compare_safe H1 H2.
         }
-        case_bool_decide; subst. 
+        case_bool_decide; subst.
         * iPoseProof (val_rel_inj with "Hv1 Hv2") as "->".
           sim_pures. case_bool_decide; done.
         * sim_pures. case_bool_decide; subst; last done.
@@ -249,7 +249,11 @@ Section refl.
         rewrite -(binder_insert_fmap fst (v_t', x)).
         rewrite -(binder_insert_fmap snd (v_t', x)).
         iApply ("IH2" with "Hwf3"). by iApply subst_map_rel_insert.
-    - done.
+    - (* Fork *)
+      iApply sim_fork; first by sim_pures.
+      iSpecialize ("IH" with "Hwf Hs").
+      iApply (sim_wand with "IH").
+      by iIntros (v_t v_s) "Hv".
     - (* AllocN *)
       (** TODO: fix this: see notes above about adding allocations of length > 1 into the bijection *)
       iDestruct "Hwf" as "(Hwf1 & Hwf2)".
@@ -288,10 +292,10 @@ Section refl.
 
 
   Theorem heap_bij_refl e : expr_wf e -∗ e ⪯ e {{ val_rel }}.
-  Proof. 
+  Proof.
     iIntros "Hwf". iPoseProof (expr_wf_sound with "Hwf") as "Hwf".
     iSpecialize ("Hwf" $! ∅). setoid_rewrite fmap_empty.
-    rewrite !subst_map_empty. iApply "Hwf". rewrite /subst_map_rel. 
+    rewrite !subst_map_empty. iApply "Hwf". rewrite /subst_map_rel.
     by rewrite -map_ForallI_empty.
   Qed.
 End refl.
diff --git a/theories/simplang/primitive_laws.v b/theories/simplang/primitive_laws.v
index 18598a9bafa33b800fa328a84d790c14523432d5..be80962bba844806f30ff061443c6d65314eb7c8 100644
--- a/theories/simplang/primitive_laws.v
+++ b/theories/simplang/primitive_laws.v
@@ -140,6 +140,20 @@ Proof. apply hasfun_agree. Qed.
 Lemma hasfun_source_agree f K_s1 K_s2 : f @s K_s1 -∗ f @s K_s2 -∗ ⌜K_s1 = K_s2⌝.
 Proof. apply hasfun_agree. Qed.
 
+(** fork *)
+Lemma sim_fork e_t e_s Ψ :
+  #() ⪯ #() [{ Ψ }] -∗
+  e_t ⪯ e_s [{ lift_post Ω }] -∗
+  Fork e_t ⪯ Fork e_s [{ Ψ }].
+Proof.
+  iIntros "Hval Hsim". iApply sim_lift_head_step_both.
+  iIntros (????) "[(HP_t & HP_s & Hσ_t & Hσ_s & Hinv) %Hnstuck] !>".
+  iSplitR. { eauto with head_step. }
+  iIntros (e_t' efs_t σ_t') "%"; inv_head_step.
+  iModIntro. iExists _, _, _. iSplitR. { eauto with head_step. }
+  simpl. iFrame.
+Qed.
+
 (** operational heap lemmas *)
 Lemma heap_array_to_seq_mapsto l v (n : nat) γh γm (hG : gen_heapPreNameG loc (option val) Σ γh γm) :
   ([∗ map] l' ↦ ov ∈ heap_array l (replicate n v), gen_sim_heap.mapsto (hG:=hG) l' (DfracOwn 1) ov) -∗
diff --git a/theories/simulation/lifting.v b/theories/simulation/lifting.v
index 7ea086034f2758071fa5e95524431535d40765c3..da665b3ed25a0f1c65bba8256b2fe0fc29fd7552 100644
--- a/theories/simulation/lifting.v
+++ b/theories/simulation/lifting.v
@@ -135,6 +135,25 @@ Section fix_sim.
   Qed.
 
   (** Primitive reduction *)
+  Lemma sim_lift_prim_step_both e_t e_s Φ:
+    (∀ P_t P_s σ_t σ_s, state_interp P_t σ_t P_s σ_s ∗ ⌜¬ reach_stuck P_s e_s σ_s⌝ ==∗
+      ⌜reducible P_t e_t σ_t⌝ ∗
+      ∀ e_t' efs_t σ_t',
+        ⌜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' ∗ e_t' ⪯{Ω} e_s' [{ Φ }] ∗
+            ([∗ list] e_t0;e_s0 ∈ efs_t;efs_s, e_t0 ⪯ e_s0 [{lift_post Ω}])) -∗
+    e_t ⪯{Ω} e_s [{ Φ }].
+  Proof.
+    iIntros "Hsim".
+    rewrite sim_expr_unfold. iIntros (????) "[Hstate %]".
+    iMod ("Hsim" with "[$Hstate ]") as "[Hred Hsim]"; first done. iModIntro. iRight; iLeft.
+    iFrame. iIntros (e_t' efs_t σ_t') "Hstep".
+    iMod ("Hsim" with "Hstep") as (e_s' efs_s σ_s') "(Hs & ? & ? & Hefs)".
+    iRight. iModIntro. iExists _, _, _, _, _.
+    iDestruct (big_sepL2_length with "Hefs") as "#$". iFrame. iPureIntro. constructor.
+  Qed.
+
   Lemma sim_lift_prim_step_target e_t e_s Φ :
     (∀ P_t P_s σ_t σ_s, state_interp P_t σ_t P_s σ_s ∗ ⌜¬ reach_stuck P_s e_s σ_s⌝ ==∗
       ⌜reducible P_t e_t σ_t⌝ ∗
@@ -199,24 +218,22 @@ Section fix_sim.
     iModIntro. iExists e_s', σ_s'. iFrame. iPureIntro. by apply head_prim_step.
   Qed.
 
-  (* this lemma is useful because it only requires to re-establish the SI after
-    stepping both in the target and the source *)
   Lemma sim_lift_head_step_both e_t e_s Φ:
     (∀ P_t P_s σ_t σ_s, state_interp P_t σ_t P_s σ_s ∗ ⌜¬ reach_stuck P_s e_s σ_s⌝ ==∗
       ⌜head_reducible P_t e_t σ_t⌝ ∗
       ∀ e_t' efs_t σ_t',
         ⌜head_step P_t e_t σ_t e_t' σ_t' efs_t⌝ ==∗
-          ∃ e_s' σ_s', ⌜efs_t = []⌝ ∗ ⌜head_step P_s e_s σ_s e_s' σ_s' []⌝ ∗
-            state_interp P_t σ_t' P_s σ_s' ∗ e_t' ⪯{Ω} e_s' [{ Φ }]) -∗
+          ∃ 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' ∗ e_t' ⪯{Ω} e_s' [{ Φ }] ∗
+          ([∗ list] e_t0;e_s0 ∈ efs_t;efs_s, e_t0 ⪯ e_s0 [{lift_post Ω}])) -∗
     e_t ⪯{Ω} e_s [{ Φ }].
   Proof.
-    iIntros "Hsim". iApply sim_step_target.
-    iIntros (????) "[Hstate %Hnreach]". iMod ("Hsim" with "[$Hstate//]") as "(% & Hstep)".
+    iIntros "Hsim". iApply sim_lift_prim_step_both. iIntros (????) "[Hstate %Hnreach]".
+    iMod ("Hsim" with "[$Hstate//]") as "(% & Hstep)".
     iModIntro. iSplitR. { iPureIntro. by eapply head_prim_reducible. }
-    iIntros (e_t' efs_t σ_t') "%". iMod ("Hstep" with "[]") as (e_s' σ_s') "(% & % & Hstate & Hsim)".
+    iIntros (e_t' efs_t σ_t') "%". iMod ("Hstep" with "[]") as (e_s' efs_s σ_s') "(% & Hstate & Hsim)".
     { iPureIntro. by eapply head_reducible_prim_step. }
-    iModIntro. iExists e_s', σ_s'. iFrame. iPureIntro. split; [done|].
-    econstructor; first by eapply head_prim_step. constructor.
+    iModIntro. iExists e_s', efs_s, σ_s'. iFrame. iPureIntro. by eapply head_prim_step.
   Qed.
 
   (** Stuckness *)
diff --git a/theories/simulation/slsls.v b/theories/simulation/slsls.v
index af5499195d56a1d1e7cb7e7d27456c1e018f914a..14da830cd2b64aa2335bd441ade8820fea3acbd7 100644
--- a/theories/simulation/slsls.v
+++ b/theories/simulation/slsls.v
@@ -318,6 +318,7 @@ Section fix_lang.
         (∃ e_s' e_s'' σ_s' σ_s'' efs_s,
           ⌜no_forks P_s e_s σ_s e_s' σ_s'⌝ ∗
           ⌜prim_step P_s e_s' σ_s' e_s'' σ_s'' efs_s⌝ ∗
+          (* TODO: This length constraint is unnecessary as it is implied by the big_sepL2. *)
           ⌜length efs_t = length efs_s⌝ ∗
           state_interp P_t σ_t' P_s σ_s'' ∗ sim_expr Ω Φ e_t' e_s'' ∗ [∗ list] e_t; e_s ∈ efs_t; efs_s, sim_expr Ω (lift_post Ω) e_t e_s))