diff --git a/algebra/upred.v b/algebra/upred.v
index 465cfb505535f854cfe88478e4b66f1e1d6857b3..a3ceb502ae4de2d4b07ceb201c05ba46834d9c31 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -846,6 +846,8 @@ Proof. done. Qed.
 (* Own and valid derived *)
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
 Proof. by intros; rewrite ownM_valid valid_elim. Qed.
+Global Instance ownM_mono : Proper (flip (≼) ==> (⊑)) (@uPred_ownM M).
+Proof. move=>a b [c H]. rewrite H ownM_op. eauto. Qed.
 
 (* Timeless *)
 Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 0 x → P n x.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 6d48f129479ae59ea4add81eafb6a3ad45f05ccb..4e94acc1c75c612fcf6271458b63fbde65ba1ab3 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -116,7 +116,7 @@ Section auth.
     (* Getting this wand eliminated is really annoying. *)
     rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
     rewrite wand_elim_r fsa_frame_l.
-    apply (fsa_mono_pvs fsa)=> v.
+    apply (fsa_mono_pvs fsa)=> x.
     rewrite sep_exist_l; apply exist_elim=> L.
     rewrite sep_exist_l; apply exist_elim=> Lv.
     rewrite sep_exist_l; apply exist_elim=> ?.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index c6fd4ff2297626dbc44f23fcd75237222c039588..b5b8cedc691b541861efe62e7884c92027703224 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -66,6 +66,8 @@ Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper
 
 Lemma own_op γ a1 a2 : own i γ (a1 ⋅ a2) ≡ (own i γ a1 ★ own i γ a2)%I.
 Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
+Global Instance own_mono γ : Proper (flip (≼) ==> (⊑)) (own i γ).
+Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
 Lemma always_own_unit γ a : (□ own i γ (unit a))%I ≡ own i γ (unit a).
 Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
 Lemma own_valid γ a : own i γ a ⊑ ✓ a.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 913b0db5b4102ddf081bfad8b4c7d61f83137a4d..7327ff1006cc2e1c6509a3c39fe4776d3972d222 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -50,6 +50,8 @@ Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
 Global Instance ownG_proper : Proper ((≡) ==> (≡)) (@ownG Λ Σ) := ne_proper _.
 Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ≡ (ownG m1 ★ ownG m2)%I.
 Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
+Global Instance ownG_mono : Proper (flip (≼) ==> (⊑)) (@ownG Λ Σ).
+Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
 Lemma always_ownG_unit m : (□ ownG (unit m))%I ≡ ownG (unit m).
 Proof.
   apply uPred.always_ownM.
@@ -64,6 +66,7 @@ Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
 
+
 (* inversion lemmas *)
 Lemma ownI_spec r n i P :
   ✓{n} r →