From 0024ac1fe5e71cd42b72e578975b888369360ba8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Sep 2016 22:52:12 +0200
Subject: [PATCH] Mononicity of own.

---
 program_logic/ghost_ownership.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index f8aa8a7c5..378f3f23a 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -50,8 +50,11 @@ Global Instance own_proper γ :
 
 Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ★ own γ a2.
 Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
-Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (@own Σ A _ γ).
-Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
+Lemma own_mono γ a1 a2 : a2 ≼ a1 → own γ a1 ⊢ own γ a2.
+Proof. move=> [c ->]. rewrite own_op. eauto with I. Qed.
+
+Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (@own Σ A _ γ).
+Proof. intros a1 a2. apply own_mono. Qed.
 
 Lemma own_valid γ a : own γ a ⊢ ✓ a.
 Proof.
-- 
GitLab