diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index e589e65182da0d2b077eea8dd75841cf6987ad27..6d9b3e3cf3c49fba5186f41f225a21e2a272f270 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -265,3 +265,49 @@ Tactic Notation "rel_load_r" :=
   |reflexivity
   |rel_finish  (** new goal *)].
 
+(** Fork *)
+Lemma tac_rel_fork_l `{relocG Σ} K ℶ E e' eres Γ e t A :
+  e = fill K (Fork e') →
+  is_closed_expr [] e' →
+  eres = fill K #() →
+  envs_entails ℶ (|={⊤,E}=> ▷ (WP e' {{ _ , True%I }} ∗ refines E Γ eres t A))%I →
+  envs_entails ℶ (refines ⊤ Γ e t A).
+Proof.
+  intros ????. subst e eres.
+  rewrite -refines_fork_l //.
+Qed.
+
+Tactic Notation "rel_fork_l" :=
+  iStartProof;
+  first
+    [rel_reshape_cont_l ltac:(fun K e' =>
+       eapply (tac_rel_fork_l K); first reflexivity)
+    |fail 1 "rel_fork_l: cannot find 'Fork'"];
+  (* the remaining goals are from tac_rel_load_r (except for the first one, which has already been solved by this point) *)
+  [try fast_done    (** is_closed_expr [] e' *)
+  |reflexivity    || fail "rel_fork_l: this should not happen O-:"
+  |rel_finish  (** new goal *)].
+
+Lemma tac_rel_fork_r `{relocG Σ} K ℶ E e' Γ e t eres A :
+  e = fill K (Fork e') →
+  nclose specN ⊆ E →
+  is_closed_expr [] e' →
+  eres = fill K #() →
+  envs_entails ℶ (∀ i, i ⤇ e' -∗ refines E Γ t eres A) →
+  envs_entails ℶ (refines E Γ t e A).
+Proof.
+  intros ?????. subst e eres.
+  rewrite -refines_fork_r //.
+Qed.
+
+Tactic Notation "rel_fork_r" "as" ident(i) constr(H) :=
+  iStartProof;
+  first
+    [rel_reshape_cont_r ltac:(fun K e' =>
+       eapply (tac_rel_fork_r K); first reflexivity)
+    |fail 1 "rel_fork_r: cannot find 'Fork'"];
+  (* the remaining goals are from tac_rel_load_r (except for the first one, which has already been solved by this point) *)
+  [solve_ndisj || fail "rel_fork_r: cannot prove 'nclose specN ⊆ ?'"
+  |try fast_done    (** is_closed_expr [] e' *)
+  |reflexivity    || fail "rel_fork_r: this should not happen O-:"
+  |iIntros (i) H; rel_finish  (** new goal *)].
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 988bf4f4c41636f427d0c19944a5ed89c23d0090..198cc4df27f228cfa858d66dab727307f9cc1ee1 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -379,8 +379,8 @@ Section rules.
 
   Lemma refines_fork_l K Γ E e t A :
     is_closed_expr [] e →
-   (|={⊤,E}=> ▷ (WP e {{ _, True }}) ∗
-    ({E;Γ} ⊨ fill K (of_val #()) << t : A)) -∗
+   (|={⊤,E}=> ▷ (WP e {{ _, True }} ∗
+    ({E;Γ} ⊨ fill K (of_val #()) << t : A))) -∗
    Γ ⊨ fill K (Fork e) << t : A.
   Proof.
     iIntros (?) "Hlog".
diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index d6b5ac6f3bf9a9745caa5f8077c662d07204bc5e..b3689499b17a174c38e9586df34496f9f6a3bb9f 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -70,4 +70,27 @@ Proof.
   rel_values.
 Qed.
 
+(* testing fork *)
+Lemma test5 l r Γ N :
+  inv N (l ↦ #3) -∗
+  r ↦ₛ #4 -∗
+  Γ ⊨ (let: "x" := #1 + (Fork !#l;; !#l) in "x")
+  << (Fork (#r <- #0);; !#r) : EqI.
+Proof.
+  iIntros "#IN Hr".
+  rel_fork_l. iModIntro. iSplitR.
+  { iNext. iInv N as "Hl" "Hcl".
+    iApply (wp_load with "Hl"). iNext. iIntros "Hl".
+    by iApply "Hcl". }
+  iNext. rel_pure_l. rel_pure_l.
+  rel_load_l. iInv N as "?" "Hcl". iModIntro. iExists _; iFrame.
+  iNext. iIntros "Hl". iMod ("Hcl" with "Hl") as "_".
+  repeat rel_pure_l.
+  rel_fork_r as i "Hi".
+  repeat rel_pure_r.
+  rel_load_r.
+  rel_values.
+Qed.
+
 End test.
+