diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index af69eaed4e0503b63a0d2553d041b8b8602979e3..4ac1bd858402b4ed8313f0573cc710157c03da5a 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -155,5 +155,5 @@ Module Type lifetime_sig.
   Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
 
   Parameter lft_init : ∀ `{invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
-    True ={E}=∗ ∃ _ : lftG Σ, lft_ctx.
+    (|={E}=> ∃ _ : lftG Σ, lft_ctx)%I.
 End lifetime_sig.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 4da62c201f87203fac7ece7397944f3b397733c9..b716b63ccbdfe555b291809b37d75deba3cd886e 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -36,7 +36,7 @@ Section type_soundness.
     { split. by eapply adequate_nonracing.
       intros. by eapply (adequate_safe (main [exit_cont]%E)). }
     apply: lrust_adequacy=>?. iIntros "_".
-    iMod (lft_init with "[//]") as (?) "#LFT". done.
+    iMod lft_init as (?) "#LFT". done.
     iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
     wp_bind (of_val main). iApply (wp_wand with "[Htl]").
     iApply (Hmain _ [] [] $! tid with "LFT [] Htl [] []").