diff --git a/lifetime/lifetime.v b/lifetime/lifetime.v
index 3e50e5e2b50b5d3b1c48842c9c730785f2f9d613..08ee880b401ea8345024f9e2cf4c68b463707107 100644
--- a/lifetime/lifetime.v
+++ b/lifetime/lifetime.v
@@ -29,6 +29,15 @@ Section derived.
 Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
+Lemma lft_kill_atomic (Λ : atomic_lft) :
+  lft_ctx -∗ □(1.[@Λ] ={↑lftN ∪ userE}[userE]▷=∗ [†@Λ]).
+Proof.
+  iIntros "#LFT".
+  rewrite -(big_sepS_singleton (λ x, 1.[@x])%I)
+          -(big_sepS_singleton (λ x, [†@x])%I).
+  by iApply (lft_kill_atomics with "LFT").
+Qed.
+
 Lemma lft_create_atomic E :
   ↑lftN ⊆ E →
   lft_ctx ={E}=∗ ∃ Λ, 1.[@Λ].
diff --git a/lifetime/lifetime_sig.v b/lifetime/lifetime_sig.v
index 6771f88d13efd2dcd862572ccad54b5875b1e0bb..06af32be7f4594d08bccf4cbd334b1dc3bc0e209 100644
--- a/lifetime/lifetime_sig.v
+++ b/lifetime/lifetime_sig.v
@@ -134,7 +134,6 @@ Module Type lifetime_sig.
      fresh lifetimes when using lifetimes as keys to index into a map. *)
   Parameter lft_fresh : ∀ κ κ', ∃ i : positive,
     ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
-  Parameter lft_kill_atomic : ∀ Λ, lft_ctx -∗ □ ((1).[@Λ] ={↑lftN ∪ userE}[userE]▷=∗ [†@Λ]).
   Parameter lft_kill_atomics : ∀ Λs,
     lft_ctx -∗ □ (([∗ set] Λ ∈ Λs, (1).[@Λ]) ={↑lftN ∪ userE}[userE]▷=∗ [∗ set] Λ∈Λs, [†@Λ]).
 
diff --git a/lifetime/model/creation.v b/lifetime/model/creation.v
index 43ed4f91f4f7fcf278a6268881c391a3acf226d1..57cc589a07a507b17a79775e25abfd538be4635a 100644
--- a/lifetime/model/creation.v
+++ b/lifetime/model/creation.v
@@ -197,15 +197,6 @@ Proof.
     + iRight. iFrame. iPureIntro. by apply lft_dead_in_union_false.
 Qed.
 
-Lemma lft_kill_atomic (Λ : atomic_lft) :
-  lft_ctx -∗ □(1.[@Λ] ={↑lftN ∪ userE}[userE]▷=∗ [†@Λ]).
-Proof.
-  iIntros "#LFT".
-  rewrite -(big_sepS_singleton (λ x, 1.[@x])%I)
-          -(big_sepS_singleton (λ x, [†@x])%I).
-  by iApply (lft_kill_atomics with "LFT").
-Qed.
-
 Lemma lft_create_strong P E :
   pred_infinite P → ↑lftN ⊆ E →
   lft_ctx ={E}=∗