Add lft_create_atomic

This lemma exposes the fact that `lft_create` can be used to actually
produce an atomic lifetime. This version of the lemma doesn't need to
include the killing update thanks to the existence of `lft_kill_atomic`
which is always applicable for these atomic lifetimes.

This *could* replace `lft_create`, but we keep that lemma for backwards
compatibility in the API.

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.