From fbde58f6f41a13a11d5c58b5fd439382f0c76c56 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 24 Feb 2018 11:58:12 +0100
Subject: [PATCH] Show yet another relation between plainly and equality.

---
 theories/bi/derived_laws.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 9229c6a02..8e99ebd7d 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1934,6 +1934,16 @@ Proof.
     by rewrite plainly_pure True_impl.
 Qed.
 
+Lemma plainly_True_alt P : bi_plainly (True -∗ P) ⊣⊢ P ≡ True.
+Proof.
+  apply (anti_symm (⊢)).
+  - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto.
+    by rewrite wand_elim_r.
+  - rewrite internal_eq_sym (internal_eq_rewrite _ _
+      (λ Q, bi_plainly (True -∗ Q)) ltac:(solve_proper)).
+    by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
+Qed.
+
 Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
   Absorbing (x ≡ y : PROP)%I.
 Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
-- 
GitLab