Flipped Proper for uPred_valid.

e96d5cf8 · Robbert Krebbers · dba0b479 · e96d5cf8
Commit e96d5cf8 authored Dec 02, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

base_logic/primitive.v base_logic/primitive.v +3 -0

No files found.
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -322,6 +322,9 @@ Global Instance uPred_valid_proper : Proper ((⊣⊢) ==> iff) (@uPred_valid M).
 Proof. solve_proper. Qed.
 Global Instance uPred_valid_mono : Proper ((⊢) ==> impl) (@uPred_valid M).
 Proof. solve_proper. Qed.
+Global Instance uPred_valid_flip_mono :
+  Proper (flip (⊢) ==> flip impl) (@uPred_valid M).
+Proof. solve_proper. Qed.

 (** Introduction and elimination rules *)
 Lemma pure_intro φ P : φ → P ⊢ ⌜φ⌝.