From 97b304a05e9ca99bca8ccfc29ce5613761aa8360 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Oct 2018 19:39:09 +0200
Subject: [PATCH] Tweak a proof.

---
 theories/base_logic/lib/fancy_updates.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 2c4a5818f..37535edcd 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -63,11 +63,10 @@ Lemma step_fupdN_soundness `{invPreG Σ} φ n :
   (∀ `{Hinv: invG Σ}, (|={⊤, ∅}▷=>^n |={⊤, ∅}=> ⌜ φ ⌝ : iProp Σ)%I) →
   φ.
 Proof.
-  iIntros (Hiter).
-  eapply (soundness (M:=iResUR Σ) _  (S (S n))).
-  eapply (fupd_plain_soundness ⊤); first by apply _.
-  intros Hinv. rewrite -/sbi_laterN.
-  iPoseProof (Hiter Hinv) as "H".
+  intros Hiter.
+  apply (soundness (M:=iResUR Σ) _  (S (S n))); simpl.
+  apply (fupd_plain_soundness ⊤ _).
+  intros Hinv. iPoseProof (Hiter Hinv) as "H".
   destruct n as [|n].
   - rewrite //=. iPoseProof (fupd_plain_strong with "H") as "H'".
     do 2 iMod "H'"; iModIntro; auto.
-- 
GitLab