remove True

theories/base_logic/lib/invariants.v

@@ -78,7 +78,7 @@ Section inv.
 
   (** Invariants API *)
   Definition inv_def (N: namespace) (P: iProp Σ) : iProp Σ :=
-    (□ (∀ E, ⌜↑N ⊆ E⌝ → True ={E,E ∖ ↑N}=∗ ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True)))%I.
+    (□ (∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True)))%I.
   Definition inv_aux : seal (@inv_def). by eexists. Qed.
   Definition inv := inv_aux.(unseal).
   Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
@@ -101,9 +101,8 @@ Section inv.
     inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
   Proof.
     iIntros "#I #Acc". rewrite inv_eq.
-    iModIntro. iIntros (E H) "T".
-    iSpecialize ("I" $! E H with "T").
-    iApply fupd_wand_r. iFrame.
+    iModIntro. iIntros (E H). iDestruct ("I" $! E H) as "#I'".
+    iApply fupd_wand_r. iFrame "I'".
     iIntros "(P & Hclose)". iSpecialize ("Acc" with "P").
     iDestruct "Acc" as "[Q CB]". iFrame.
     iIntros "Q". iApply "Hclose". now iApply "CB".