From b58adc74115309eb79c0b5a55f4573122f041671 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Oct 2018 21:27:26 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20`(|=3D=3D>=20=E2=88=80=20x,=20=CE=A6=20?=
 =?UTF-8?q?x)=20=E2=8A=A3=E2=8A=A2=20(=E2=88=80=20x,=20|=3D=3D>=20=CE=A6?=
 =?UTF-8?q?=20x)`=20for=20plain=20`=CE=A6`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/updates.v | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 33824c502..40a3437b4 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -156,8 +156,21 @@ Section bupd_derived_sbi.
     by rewrite -bupd_intro -or_intro_l.
   Qed.
 
-  Lemma bupd_plain P `{BiBUpdPlainly PROP, !Plain P} : (|==> P) ⊢ P.
-  Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
+  Section bupd_plainly.
+    Context `{BiBUpdPlainly PROP}.
+
+    Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
+    Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
+
+    Lemma bupd_forall {A} (Φ : A → PROP) `{∀ x, Plain (Φ x)} :
+      (|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x).
+    Proof.
+      apply (anti_symm _).
+      - apply forall_intro=> x. by rewrite (forall_elim x).
+      - rewrite -bupd_intro. apply forall_intro=> x.
+        by rewrite (forall_elim x) bupd_plain.
+    Qed.
+  End bupd_plainly.
 End bupd_derived_sbi.
 
 Section fupd_derived.
-- 
GitLab