From 920241763c9abe33789a9d9f1b990ddb32b53601 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Dec 2016 11:39:57 +0100
Subject: [PATCH] Tweak entails_equiv_and.

---
 theories/base_logic/derived.v | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 11772f13c..a72988e00 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -438,11 +438,7 @@ Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@uPred_sep M).
 Proof. intros P; apply (anti_symm _); auto. Qed.
 
 Lemma entails_equiv_and P Q : (P ⊣⊢ Q ∧ P) ↔ (P ⊢ Q).
-Proof.
-  split; first by intros ->; apply uPred.and_elim_l. intros PQ.
-  apply uPred.equiv_spec; split;
-   [by apply uPred.and_intro|apply uPred.and_elim_r].
-Qed.
+Proof. split. by intros ->; auto. intros; apply (anti_symm _); auto. Qed.
 Lemma sep_and_l P Q R : P ∗ (Q ∧ R) ⊢ (P ∗ Q) ∧ (P ∗ R).
 Proof. auto. Qed.
 Lemma sep_and_r P Q R : (P ∧ Q) ∗ R ⊢ (P ∗ R) ∧ (Q ∗ R).
-- 
GitLab