From 2dc55133f551e7215beb04c9b8d5a070c29b1b14 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 7 Aug 2017 18:13:00 +0200
Subject: [PATCH] pure_flip_mono

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

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 464cb35e6..ca50081f0 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -236,6 +236,8 @@ Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ⌜φ1⌝ ⊢ ⌜φ2⌝.
 Proof. intros; apply pure_elim with φ1; eauto. Qed.
 Global Instance pure_mono' : Proper (impl ==> (⊢)) (@uPred_pure M).
 Proof. intros φ1 φ2; apply pure_mono. Qed.
+Global Instance pure_flip_mono : Proper (flip impl ==> flip (⊢)) (@uPred_pure M).
+Proof. intros φ1 φ2; apply pure_mono. Qed.
 Lemma pure_iff φ1 φ2 : (φ1 ↔ φ2) → ⌜φ1⌝ ⊣⊢ ⌜φ2⌝.
 Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
 Lemma pure_intro_l φ Q R : φ → (⌜φ⌝ ∧ Q ⊢ R) → Q ⊢ R.
-- 
GitLab