From bdb566a4039fe9ae15ef9fc750510565cb91fe47 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 7 May 2018 23:58:44 +0200
Subject: [PATCH] Shorten proof.
---
theories/bi/derived_laws_bi.v | 6 +-----
1 file changed, 1 insertion(+), 5 deletions(-)
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 7b8a79d49..f3e5d9502 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -123,11 +123,7 @@ Proof.
+ rewrite -EQ impl_elim_r. done.
Qed.
Lemma entails_impl_True P Q : (P ⊢ Q) ↔ (True ⊢ (P → Q)).
-Proof.
- rewrite entails_eq_True. split.
- - by intros <-.
- - intros. apply (anti_symm (⊢)); last done. apply True_intro.
-Qed.
+Proof. rewrite entails_eq_True equiv_spec; naive_solver. Qed.
Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
Proof. auto. Qed.
--
GitLab