diff --git a/lifetime/model/creation.v b/lifetime/model/creation.v
index 5eccf4b91c20aa0209be8ec7fa1e5058fe9751ee..3e9a6e0d2c626d2161f9042eab7bec097a662fc2 100644
--- a/lifetime/model/creation.v
+++ b/lifetime/model/creation.v
@@ -107,41 +107,47 @@ Definition kill_set (I : gmap lft lft_names) (Λ : atomic_lft) : gset lft :=
 Lemma elem_of_kill_set I Λ κ : κ ∈ kill_set I Λ ↔ Λ ∈ κ ∧ is_Some (I !! κ).
 Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
 
-Lemma lft_create_strong P E :
-  pred_infinite P → ↑lftN ⊆ E →
-  lft_ctx ={E}=∗
-  ∃ p : positive, let κ := positive_to_lft p in ⌜P p⌝ ∗
-       (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
+Lemma lupd_gmap_mass_insert (Λs : gset atomic_lft) (m : alftUR) (x y : lft_stateR) `{!Exclusive x} : ✓ y →
+  (m, gset_to_gmap x Λs) ~l~> (gset_to_gmap y Λs ∪ m, gset_to_gmap y Λs).
 Proof.
-  assert (userE_lftN_disj:=userE_lftN_disj). iIntros (HP ?) "#LFT".
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  rewrite ->(pred_infinite_set (C:=gset _)) in HP.
-  destruct (HP (dom A)) as [Λ [HPx HΛ%not_elem_of_dom]].
-  iMod (own_update with "HA") as "[HA HΛ]".
-  { apply auth_update_alloc, (alloc_singleton_local_update _ Λ (Cinl 1%Qp))=>//.
-    by rewrite lookup_fmap HΛ. }
-  iMod ("Hclose" with "[HA HI Hinv]") as "_".
-  { iNext. rewrite /lfts_inv /own_alft_auth.
-    iExists (<[Λ:=true]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
-    iApply (@big_sepS_impl with "[$Hinv]").
-    iModIntro. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
-    - iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
-    - iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
-  iModIntro; iExists Λ.
-  rewrite {1}/lft_tok big_sepMS_singleton. iSplit; first done. iFrame "HΛ".
-  clear I A HΛ HPx HP.
-  (* From here on, we are proving that an atomic lifetime can be ended. *)
-  iIntros "!> HΛ".
+  intros ?.
+  apply gmap_local_update.
+  intros Λ; destruct (m !! Λ) as [|] eqn:He1, (decide (Λ ∈ Λs)) as [|].
+  - rewrite lookup_union_l' !lookup_gset_to_gmap !option_guard_True // He1.
+    by apply option_local_update, exclusive_local_update.
+  - rewrite lookup_union_r !lookup_gset_to_gmap !option_guard_False //= He1 //.
+  - rewrite lookup_union_l' !lookup_gset_to_gmap !option_guard_True // He1.
+    by apply alloc_option_local_update.
+  - rewrite lookup_union_r !lookup_gset_to_gmap !option_guard_False //= He1 //.
+Qed.
+
+Lemma lft_kill_atomics :
+  lft_ctx -∗
+  ∀ (Λs : gset atomic_lft),
+    □(([∗ set] Λ∈Λs, 1.[positive_to_lft Λ]) ={↑lftN ∪ userE}[userE]▷=∗
+      ([∗ set] Λ∈Λs, [†positive_to_lft Λ])).
+Proof.
+  assert (userE_lftN_disj:=userE_lftN_disj). iIntros "#LFT" (Λs) "!> HΛs".
+  destruct (decide (Λs = ∅)) as [->|Hne].
+  { rewrite !big_sepS_empty.
+    iApply fupd_mask_intro; [set_solver|iIntros "$"].
+  }
   iApply (step_fupd_mask_mono (↑lftN ∪ userE) _ ((↑lftN ∪ userE)∖↑mgmtN)); [solve_ndisj..|].
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  rewrite /lft_tok big_sepMS_singleton.
-  iDestruct (own_valid_2 with "HA HΛ")
-    as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid_discrete.
-  iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
-  { by eapply auth_update, singleton_local_update,
-      (exclusive_local_update _ (Cinr ())). }
-  iDestruct "HΛ" as "#HΛ". iModIntro; iNext. (* This is THE step *)
-  pose (K := kill_set I Λ).
+  rewrite /lft_tok.
+  iAssert (own alft_name (◯ gset_to_gmap (Cinl 1%Qp) Λs))%I with "[HΛs]" as "HΛs".
+  { setoid_rewrite big_sepMS_singleton.
+    iDestruct (big_opS_own _ _ _ Hne with "HΛs") as "HΛs".
+    rewrite -(big_opS_gset_to_gmap Λs (Cinl 1%Qp)) big_opS_auth_frag //. }
+  iDestruct (own_valid_2 with "HA HΛs")
+    as %[[s Hs] _]%auth_both_valid_discrete.
+  iMod (own_update_2 with "HA HΛs") as "[HA HΛs]".
+  { eapply auth_update.
+    by apply (lupd_gmap_mass_insert Λs _ _ (Cinr ())). }
+  rewrite -[in own alft_name (◯ _)]big_opS_gset_to_gmap big_opS_auth_frag big_opS_own //.
+  iDestruct "HΛs" as "#HΛs".
+  iModIntro; iNext.
+  pose (K := set_bind (λ Λ, kill_set I Λ) Λs).
   pose (K' := filter (lft_alive_in A) (dom I) ∖ K).
   destruct (proj1 (subseteq_disjoint_union_L (K ∪ K') (dom I))) as (K''&HI&HK'').
   { set_solver+. }
@@ -153,36 +159,79 @@ Proof.
     by iApply lft_inv_alive_in. }
   iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [† κ])%I with "[HinvK]" as "HinvK".
   { iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!>".
-    iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
+    iIntros (κ [Λ [HΛ [? _]%elem_of_kill_set]]%elem_of_set_bind) "$".
+    rewrite /lft_dead.
+    by iDestruct (big_sepS_elem_of with "HΛs") as "$". }
   iApply fupd_trans.
   iApply (fupd_mask_mono (userE ∪ ↑borN ∪ ↑inhN)); first solve_ndisj.
   iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
   { done. }
-  { intros κ κ' [??]%elem_of_kill_set ??. apply elem_of_kill_set.
+  { intros κ κ' [Λ [? [??]%elem_of_kill_set]]%elem_of_set_bind ??.
+    apply elem_of_set_bind; exists Λ; split; [assumption|].
+    apply elem_of_kill_set.
     split; last done. by eapply gmultiset_elem_of_subseteq. }
   { intros κ ???. rewrite elem_of_difference elem_of_filter elem_of_dom. auto. }
   iModIntro. iMod ("Hclose" with "[-]") as "_"; last first.
-  { iModIntro. rewrite /lft_dead. iExists Λ.
+  { iModIntro.
+    iApply (big_sepS_impl with "HΛs").
+    iIntros "!>" (Λ) "??".
+    rewrite /lft_dead. iExists Λ.
     rewrite gmultiset_elem_of_singleton. auto. }
-  iNext. iExists (<[Λ:=false]>A), I.
-  rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
+  iNext. iExists ((gset_to_gmap false Λs ∪ A) : gmap atomic_lft bool), I.
+  rewrite /own_alft_auth /to_alftUR map_fmap_union fmap_gset_to_gmap.
+  iFrame "HA HI".
   rewrite HI !big_sepS_union //.
   iSplitL "HinvK HinvD"; first iSplitL "HinvK".
   - iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!>".
-    iIntros (κ [? _]%elem_of_kill_set) "Hdead". rewrite /lft_inv.
-    iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false'.
+    iIntros (κ [Λ [? [? _]%elem_of_kill_set]]%elem_of_set_bind) "Hdead". rewrite /lft_inv.
+    iRight. iFrame. iPureIntro.  by eapply lft_dead_in_union_false'.
   - iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!>".
     iIntros (κ [[Hκ HκI]%elem_of_filter HκK]%elem_of_difference) "Halive".
     rewrite /lft_inv. iLeft. iFrame "Halive". iPureIntro.
-    apply lft_alive_in_insert_false; last done.
-    move: HκK. rewrite elem_of_kill_set -(elem_of_dom (D:=gset lft)). set_solver +HκI.
+    apply lft_alive_in_union_false; [|done].
+    set_solver.
   - iApply (@big_sepS_impl with "[$Hinv]"); iIntros "!>".
     rewrite /lft_inv. iIntros (κ Hκ) "[[? %]|[? %]]".
     + iLeft. iFrame. iPureIntro.
-      apply lft_alive_in_insert_false; last done. intros ?.
-      assert (κ ∈ K) by (rewrite elem_of_kill_set -(elem_of_dom (D:=gset lft)) HI elem_of_union; auto).
-      eapply HK'', Hκ. rewrite elem_of_union. auto.
-    + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
+      apply lft_alive_in_union_false; last done. intros ??.
+      set_solver.
+    + iRight. iFrame. iPureIntro. by apply lft_dead_in_union_false.
+Qed.
+
+Lemma lft_kill_atomic :
+  lft_ctx -∗
+  ∀ (Λ : atomic_lft), □(1.[positive_to_lft Λ] ={↑lftN ∪ userE}[userE]▷=∗ [†positive_to_lft Λ]).
+Proof.
+  iIntros "#LFT" (?).
+  rewrite -(big_sepS_singleton (λ x, 1.[positive_to_lft x])%I)
+          -(big_sepS_singleton (λ x, [†positive_to_lft x])%I).
+  by iApply (lft_kill_atomics with "LFT").
+Qed.
+
+Lemma lft_create_strong P E :
+  pred_infinite P → ↑lftN ⊆ E →
+  lft_ctx ={E}=∗
+  ∃ p : positive, let κ := positive_to_lft p in ⌜P p⌝ ∗
+       (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
+Proof.
+  assert (userE_lftN_disj:=userE_lftN_disj). iIntros (HP ?) "#LFT".
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  rewrite ->(pred_infinite_set (C:=gset _)) in HP.
+  destruct (HP (dom A)) as [Λ [HPx HΛ%not_elem_of_dom]].
+  iMod (own_update with "HA") as "[HA HΛ]".
+  { apply auth_update_alloc, (alloc_singleton_local_update _ Λ (Cinl 1%Qp))=>//.
+    by rewrite lookup_fmap HΛ. }
+  iMod ("Hclose" with "[HA HI Hinv]") as "_".
+  { iNext. rewrite /lfts_inv /own_alft_auth.
+    iExists (<[Λ:=true]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
+    iApply (@big_sepS_impl with "[$Hinv]").
+    iModIntro. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
+    - iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
+    - iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
+  iModIntro; iExists Λ.
+  rewrite {1}/lft_tok big_sepMS_singleton. iSplit; first done. iFrame "HΛ".
+  clear I A HΛ.
+  iApply (lft_kill_atomic with "LFT").
 Qed.
 
 Lemma lft_fresh κ κ' :
diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v
index 15d1cd5e9703a8f4aaa0daaed8f51edda4c76780..3fd9472c74ec87e79e86d38b8b0386a63be1ef1e 100644
--- a/lifetime/model/primitive.v
+++ b/lifetime/model/primitive.v
@@ -221,6 +221,14 @@ Proof.
   intros HΛ Halive Λ' HΛ'.
   rewrite lookup_insert_ne; last (by intros ->); auto.
 Qed.
+Lemma lft_alive_in_union_false A κ Λs b :
+  (∀ Λ, Λ ∈ Λs → Λ ∉ κ) → lft_alive_in A κ → lft_alive_in (gset_to_gmap b Λs ∪ A) κ.
+Proof.
+  intros HΛ Halive Λ' HΛ'.
+  rewrite lookup_union_r; [by apply Halive|].
+  apply lookup_gset_to_gmap_None.
+  by intros ?%HΛ.
+Qed.
 
 Lemma lft_dead_in_insert A κ Λ b :
   A !! Λ = None → lft_dead_in A κ → lft_dead_in (<[Λ:=b]> A) κ.
@@ -236,8 +244,28 @@ Proof.
   - exists Λ. by rewrite lookup_insert.
   - exists Λ'. by rewrite lookup_insert_ne.
 Qed.
+Lemma lft_dead_in_union_false A κ Λs :
+  lft_dead_in A κ → lft_dead_in (gset_to_gmap false Λs ∪ A) κ.
+Proof.
+  intros (Λ&?&HΛ). destruct (decide (Λ ∈ Λs)) as [|].
+  - exists Λ. rewrite lookup_union_l'.
+    + by rewrite lookup_gset_to_gmap_Some.
+    + exists false; by rewrite lookup_gset_to_gmap_Some.
+  - exists Λ. rewrite lookup_union_r.
+    + done.
+    + by rewrite lookup_gset_to_gmap_None.
+Qed.
 Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
 Proof. exists Λ. by rewrite lookup_insert. Qed.
+Lemma lft_dead_in_union_false' A κ Λs Λ :
+  Λ ∈ κ → Λ ∈ Λs → lft_dead_in (gset_to_gmap false Λs ∪ A) κ.
+Proof.
+  intros HΛκ HΛ.
+  exists Λ; split; [done|].
+  rewrite lookup_union_l'.
+  - by apply lookup_gset_to_gmap_Some.
+  - exists false; by apply lookup_gset_to_gmap_Some.
+Qed.
 Lemma lft_dead_in_alive_in_union A κ κ' :
   lft_dead_in A (κ ⊓ κ') → lft_alive_in A κ → lft_dead_in A κ'.
 Proof.