From 1a4f9850e836bcdc8aca68dcb9a02054fc2dfdd2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Nov 2017 11:48:19 +0100
Subject: [PATCH] Shorten proof.

---
 theories/base_logic/derived.v | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index f8b24ad03..55f213448 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -981,13 +981,9 @@ Proof. rewrite -(plainly_plainly P); apply plainly_intro'. Qed.
 Lemma plainly_alt P : ■ P ⊣⊢ P ≡ True.
 Proof.
   apply (anti_symm (⊢)).
-  - rewrite -prop_ext. apply plainly_intro'. rewrite plainly_elim.
-    apply and_intro; apply impl_intro_r.
-    + apply True_intro.
-    + apply and_elim_l.
+  - rewrite -prop_ext. apply plainly_mono, and_intro; apply impl_intro_r; auto.
   - rewrite internal_eq_sym (internal_eq_rewrite _ _ (λ P, ■ P)%I).
-    eapply impl_elim; first reflexivity.
-    rewrite plainly_pure. apply True_intro.
+    by rewrite plainly_pure True_impl.
 Qed.
 
 Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
-- 
GitLab