diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 421f0506715401c67e3c1ca6ab5eec5733f490d4..94bf6a0ea7c6fa8d334b21a65e48fb0dc2d0aa90 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -69,7 +69,7 @@ Lemma own_valid γ a : own i γ a ⊑ ✓ a.
 Proof.
   rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalC_validN.
 Qed.
-Lemma own_valid_r' γ a : own i γ a ⊑ (own i γ a ★ ✓ a).
+Lemma own_valid_r γ a : own i γ a ⊑ (own i γ a ★ ✓ a).
 Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own i γ a).
 Proof. unfold own; apply _. Qed.