simplify proof of step_fupd_mask_mono

b0d9c1a2 · Ralf Jung · 65c53d1d · b0d9c1a2
Commit b0d9c1a2 authored Nov 21, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 5 deletions

base_logic/lib/fancy_updates.v base_logic/lib/fancy_updates.v +3 -5

No files found.
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -217,11 +217,9 @@ Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
  F1 ⊆ F2 → E1 ⊆ E2 → (|={E1,F2}▷=> P) ⊢ |={E2,F1}▷=> P.
 Proof.
  iIntros (??) "HP".
-  iAssert (|={E2,E1}▷=> True)%I as "HE".
-  { iApply fupd_mono. apply later_intro. by iApply fupd_intro_mask. }
-  iAssert (|={F2,F1}▷=> True)%I as "HF".
-  { iApply fupd_mono. apply later_intro. by iApply fupd_intro_mask. }
-  iMod "HE". iMod "HP". iMod "HF". iModIntro. iNext. iMod "HF". iMod "HP". by iMod "HE".
+  iMod (fupd_intro_mask') as "HM1"; first fast_done. iMod "HP".
+  iMod (fupd_intro_mask') as "HM2"; first fast_done. iModIntro.
+  iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
 Qed.

 End step_fupd.