some comments on lifetime ending

lifetime/model/creation.v

@@ -129,7 +129,9 @@ Proof.
     - 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Λ. iIntros "!> HΛ".
+  clear I A HΛ HPx HP.
+  (* From here on, we are proving that an atomic lifetime can be ended. *)
+  iIntros "!> HΛ".
   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.
@@ -138,7 +140,7 @@ Proof.
   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.
+  iDestruct "HΛ" as "#HΛ". iModIntro; iNext. (* This is THE step *)
   pose (K := kill_set I Λ).
   pose (K' := filter (lft_alive_in A) (dom I) ∖ K).
   destruct (proj1 (subseteq_disjoint_union_L (K ∪ K') (dom I))) as (K''&HI&HK'').