diff --git a/coq/ra/_CoqProject b/coq/ra/_CoqProject
index f19b0f4f854ad8649a0d9115dbd35fdeb5260251..81b789448602ba0b8f059ebd7af9ff4e76db099a 100644
--- a/coq/ra/_CoqProject
+++ b/coq/ra/_CoqProject
@@ -9,7 +9,6 @@
 ./tactics.v
 ./props.v
 ./derived.v
-./wp_tactics.v
 ./notation.v
 ./foundational_ghosts.v
 ./foundational_helpers.v
diff --git a/coq/ra/alloc.v b/coq/ra/alloc.v
index 688efa4293b4c4e13a257b958918db3d18b24464..003203e5a102ae48133a8d3558f59097ba438636 100644
--- a/coq/ra/alloc.v
+++ b/coq/ra/alloc.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import ghost_ownership coq_tactics.
 From iris.algebra Require Import gmap upred_big_op.
 
-From ra Require Export notation foundational wp_tactics.
+From ra Require Export notation foundational.
 
 Import uPred.
 
diff --git a/coq/ra/foundational.v b/coq/ra/foundational.v
index e6466cc2e438338e9a9680d743c854de27126d3e..fcbdf96bb242c9907649c3eac6871319642e9c8f 100644
--- a/coq/ra/foundational.v
+++ b/coq/ra/foundational.v
@@ -13,7 +13,6 @@ From ra Require Export foundational_accessors foundational_helpers.
 
 Set Bullet Behavior "Strict Subproofs".
 
-
 Section Triples.
   Context `{fG : !foundationG Σ} (N : namespace).
   Local Notation iProp := (iProp Σ).
@@ -95,7 +94,7 @@ Section Triples.
       invariants.inv N PSInv
       ★ ▷ Seen π V ★ ▷ P
       ★ ▷ (True -★ Φ (LitV LitUnit, π))
-      ★ ▷ (∀ ρ, invariants.inv N PSInv ★ Seen π V ★ P
+      ★ ▷ (∀ ρ, invariants.inv N PSInv ★ Seen ρ V ★ P
               -★ WP (e, ρ) {{ _, True }})
     ⊢ WP (Fork e, π) @ N {{ Φ }}.
   Proof.
@@ -109,19 +108,27 @@ Section Triples.
     assert (Some V ⊑ VIEW !! π). { by apply Views_frag_valid_le. }
 
     iDestruct "HV" as "[HV _]".
+
     iApply wp_fork_pst => //.
     - destruct (VIEW !! π) as [V0|] eqn: EqV => //.
       rewrite -H0 in EqV. by eexists.
     - iNext. iFrame "HoP".
-      iIntros (ρ ς') "[% [% [% Oς']]]". iSplitR "HP HFork";
-        last by (iApply "HFork"; repeat iSplit).
+      iIntros (ρ ς') "[% [% [% Oς']]]".
+
       inversion H7.
 
       iAssert (|=r=> own VN (● (<[ρ := V0]> VIEW) ⋅ ◯ {[ρ := V0]}))%I
-        with "[HV]" as "==>[AV' FV']".
+        with "[HV]" as "==>[AV' #FV']".
       { iApply Views_alloc => //. by rewrite -H0. }
 
-      iVsIntro.
+      iAssert (Seen ρ V) as "#?".
+        { iApply ((Seen_Mono _ _ V0)). iSplit => //.
+          iPureIntro. change (Some V ⊑ Some V0).
+          by rewrite -ViewOf H0. }
+
+      iSplitR "HP HFork"; last by (iApply "HFork"; iFrame; iSplit).
+
+      do 2 iVsIntro.
       iVs ("HClose" with "[-Post]").
         { iNext. iExists ς', (<[ρ:=V0]> VIEW), HIST, INFO. iFrame.
           repeat iSplit; iPureIntro => //.
diff --git a/coq/ra/lifting.v b/coq/ra/lifting.v
index 709786abaf56e46fe1f25bb4a6df58688c3f2e01..f62776f72b8fa054cc4c8b5aef08d4c63d5f0164 100644
--- a/coq/ra/lifting.v
+++ b/coq/ra/lifting.v
@@ -29,6 +29,39 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types ef : option (expr).
 
+(** Hot fix for fork *)
+Lemma wp_lift_atomic_step2 {E Φ} e1 σ1 :
+  atomic e1 →
+  reducible e1 σ1 →
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs,
+    ■ prim_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★ |=r=> (|={E}=> Φ v2) ★ wp_fork efs)
+  ⊢ WP e1 @ E {{ Φ }}.
+Proof.
+  iIntros (Hatomic ?) "[Hσ H]".
+  iApply (wp_lift_step E _ e1); eauto using reducible_not_val.
+  iApply pvs_intro'; [set_solver|iIntros "Hclose"].
+  iExists σ1. iFrame "Hσ"; iSplit; eauto.
+  iNext; iIntros (e2 σ2 efs) "[% Hσ]".
+  edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
+  iDestruct ("H" $! v2 σ2 efs with "[Hσ]") as "==>[HΦ $]"; first by eauto.
+  iVs "Hclose". iVs "HΦ". iApply wp_value; auto using to_of_val.
+Qed.
+
+Lemma wp_lift_atomic_head_step2 {E Φ} e1 σ1 :
+  atomic e1 →
+  head_reducible e1 σ1 →
+  ▷ ownP σ1 ★ ▷ (∀ v2 σ2 efs,
+  ■ ectx_language.head_step e1 σ1 (of_val v2) σ2 efs ∧ ownP σ2 -★ |=r=> (|={E}=> Φ v2) ★ wp_fork efs)
+  ⊢ WP e1 @ E {{ Φ }}.
+Proof.
+  iIntros (??) "[? H]". iApply wp_lift_atomic_step2; eauto.
+  - by eapply head_prim_reducible.
+  - iFrame. iNext.
+    iIntros (???) "[% ?]". iApply "H". iFrame. eauto.
+    iPureIntro. by apply head_reducible_prim_step.
+Qed.
+
+
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :
   WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
@@ -123,12 +156,12 @@ Lemma wp_fork_pst E π (σ: state) e Φ :
     ★ ▷(∀ ρ (σ': state),
           ■ inv σ' ∧ ■ rel_inv σ σ'
         ∧ ■ Fork_post σ σ' π ρ
-        ∧ ownP σ' -★ ((|={E}=> Φ (LitV $ LitUnit, π)) ★ WP (e, ρ) {{ _, True }}))
+        ∧ ownP σ' -★ |=r=> ((|={E}=> Φ (LitV $ LitUnit, π)) ★ WP (e, ρ) {{ _, True }}))
   ⊢ WP (Fork e, π) @ E {{ Φ }}.
 Proof.
   intros [V ViewOf] Inv.
   iIntros "[HP HΦ]".
-  iApply (wp_lift_atomic_head_step (Fork _, π) σ).
+  iApply (wp_lift_atomic_head_step2 (Fork _, π) σ).
   - by solve_atomic.
   - assert (HNew: ∃ ρ, ρ ∉ dom (gset thread) (threads σ)).
       { eexists (fresh (dom _ (threads σ))). eapply is_fresh. }