Get rid of lft_inv_alive_twice, which was completely artificial.

Instead, we strengthen a little bit the induction hypothesis.

theories/lifetime/lifetime.v

@@ -110,7 +110,6 @@ Proof.
   - iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
 Qed.
 
-
 Lemma bor_later_tok E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].

theories/lifetime/model/creation.v

@@ -57,6 +57,7 @@ Qed.
 
 Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) :
   let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive κ')%I in
+  K ⊥ K' →
   (∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →
   (∀ κ κ', κ ∈ K → lft_alive_in A κ → is_Some (I !! κ') →
     κ' ∉ K → κ' ⊂ κ → κ' ∈ K') →
@@ -64,7 +65,7 @@ Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) :
     ={↑borN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
 Proof.
   intros Iinv. revert K'.
-  induction (collection_wf K) as [K _ IH]=> K' HK HK'.
+  induction (collection_wf K) as [K _ IH]=> K' HKK' HK HK'.
   iIntros "[HI Halive] HK".
   pose (Kalive := filter (lft_alive_in A) K).
   destruct (decide (Kalive = ∅)) as [HKalive|].
@@ -75,11 +76,10 @@ Proof.
     as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
   iDestruct (@big_sepS_delete with "HK") as "[[Hκinv Hκ] HK]"; first done.
   iDestruct (lft_inv_alive_in with "Hκinv") as "Hκalive"; first done.
-  iAssert ⌜κ ∉ K'⌝%I with "[#]" as %HκK'.
-  { iIntros (Hκ). iApply (lft_inv_alive_twice κ with "Hκalive").
-    by iApply (@big_sepS_elem_of with "Halive"). }
+  assert (κ ∉ K') as HκK' by set_solver +HκK HKK'.
   specialize (IH (K ∖ {[ κ ]})). feed specialize IH; [set_solver +HκK|].
   iMod (IH ({[ κ ]} ∪ K') with "[HI Halive Hκalive] HK") as "[[HI Halive] Hdead]".
+  { set_solver +HKK'. }
   { intros κ' κ''.
     rewrite !elem_of_difference !elem_of_singleton=> -[? Hneq] ??.
     split; [by eauto|]; intros ->.
@@ -176,6 +176,7 @@ Proof.
   iApply fupd_trans. iApply (fupd_mask_mono (↑borN ∪ ↑inhN));
                        first by apply union_least; 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.
     split; last done. by eapply gmultiset_elem_of_subseteq. }
   { intros κ κ' ?????. apply elem_of_down_close; eauto 10. }

theories/lifetime/model/primitive.v

@@ -242,14 +242,6 @@ Proof.
   by rewrite HAinsert.
 Qed.
 
-Lemma lft_inv_alive_twice κ : lft_inv_alive κ -∗ lft_inv_alive κ -∗ False.
-Proof.
-  rewrite lft_inv_alive_unfold /lft_inh.
-  iDestruct 1 as (P Q) "(_&_&Hinh)"; iDestruct 1 as (P' Q') "(_&_&Hinh')".
-  iDestruct "Hinh" as (E) "[HE _]"; iDestruct "Hinh'" as (E') "[HE' _]".
-  by iDestruct (own_inh_valid_2 with "HE HE'") as %?.
-Qed.
-
 Lemma lft_inv_alive_in A κ : lft_alive_in A κ → lft_inv A κ -∗ lft_inv_alive κ.
 Proof.
   rewrite /lft_inv. iIntros (?) "[[$ _]|[_ %]]".