Move `lft_kill_atomic` to derived laws

This doesn't need to be part of the signature (and in fact, I just
derived it directly from `lft_kill_atomics` when I proved it,) so it's
now explicitly a derived law to keep the signature minimal.

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.[@Λ].

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, [†@Λ]).
 

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}=∗