diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 75175fe82e3fbda945f08ce00ef0a5594e4807e6..acd4f0a8c6c7acc9caa29466a21f6163c867c057 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -53,11 +53,11 @@ Proof.
   iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
   { iNext. iExists NONEV. iFrame; eauto. }
-  wp_apply wp_fork; simpl. iSplitR "Hf".
-  - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
-  - wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
+  wp_apply (wp_fork with "[Hf]").
+  - iNext. wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
     iInv N as (v') "[Hl _]".
     wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
+  - wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
 Qed.
 
 Lemma join_spec (Ψ : val → iProp Σ) l :
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index b6734455cd0c135483a48cd801de2f90891136ef..959d6fc5d72d892042542034340c9a38e51e3fdd 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -104,18 +104,18 @@ Implicit Types Φ : val → iProp Σ.
 Implicit Types efs : list expr.
 Implicit Types σ : state.
 
-(** Base axioms for core primitives of the language: Stateless reductions *)
+(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
 Lemma wp_fork s E e Φ :
-  ▷ (Φ (LitV LitUnit) ∗ WP e @ s; ⊤ {{ _, True }}) ⊢ WP Fork e @ s; E {{ Φ }}.
+  ▷ WP e @ s; ⊤ {{ _, True }} -∗ ▷ Φ (LitV LitUnit) -∗ WP Fork e @ s; E {{ Φ }}.
 Proof.
-  iIntros "[HΦ He]".
+  iIntros "He HΦ".
   iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
   iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
 Qed.
 Lemma twp_fork s E e Φ :
-  Φ (LitV LitUnit) ∗ WP e @ s; ⊤ [{ _, True }] ⊢ WP Fork e @ s; E [{ Φ }].
+  WP e @ s; ⊤ [{ _, True }] -∗ Φ (LitV LitUnit) -∗ WP Fork e @ s; E [{ Φ }].
 Proof.
-  iIntros "[HΦ He]".
+  iIntros "He HΦ".
   iApply twp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
   iIntros "!> /= {$He}". by iApply twp_value.
 Qed.