diff --git a/lifetime/lifetime.v b/lifetime/lifetime.v
index 3ed2db60f5afb297a36bc1df8df8ec4c304e2f7b..3e50e5e2b50b5d3b1c48842c9c730785f2f9d613 100644
--- a/lifetime/lifetime.v
+++ b/lifetime/lifetime.v
@@ -29,13 +29,21 @@ Section derived.
 Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
+Lemma lft_create_atomic E :
+  ↑lftN ⊆ E →
+  lft_ctx ={E}=∗ ∃ Λ, 1.[@Λ].
+Proof.
+  iIntros (?) "#LFT".
+  iMod (lft_create_strong (λ _, True) with "LFT") as (κ _) "$"=>//.
+  by apply pred_infinite_True.
+Qed.
+
 Lemma lft_create E :
   ↑lftN ⊆ E →
   lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
 Proof.
   iIntros (?) "#LFT".
-  iMod (lft_create_strong (λ _, True) with "LFT") as (κ _) "$"=>//;
-    [by apply pred_infinite_True|].
+  iMod (lft_create_atomic with "LFT") as "[% $]"=>//.
   by iApply lft_kill_atomic.
 Qed.