diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index d8b072b053d2c68460aff2bb174ecacd967f1c2a..96c2b8367b1efb5c0bea1dbce1d17a45f5060041 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -16,14 +16,14 @@ Section saved_prop.
   Implicit Types γ : gname.
 
   Lemma saved_prop_alloc_strong N P (G : gset gname) :
-    True ⊑ pvs N N (∃ γ, ■(γ ∉ G) ∧ saved_prop_own SPI γ P).
+    True ⊑ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own SPI γ P).
   Proof. by apply own_alloc_strong. Qed.
 
   Lemma saved_prop_alloc N P :
     True ⊑ pvs N N (∃ γ, saved_prop_own SPI γ P).
   Proof. by apply own_alloc. Qed.
 
-  Lemma saved_prop_twice γ P Q :
+  Lemma saved_prop_agree γ P Q :
     (saved_prop_own SPI γ P ★ saved_prop_own SPI γ Q) ⊑ ▷ (P ↔ Q).
   Proof.
     rewrite /saved_prop_own -own_op own_valid agree_validI.