diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index f8aa8a7c59fa896e3cf438dcd58764411a107ccd..378f3f23a5a23de13a10c4fcc05df72ea57f7738 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.