diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index d7c76c2a52bb55e5088df1b48e33b48de3a24acd..5ba19e758365e0cf358ccd3ea92471048db9733b 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -32,6 +32,11 @@ Section saved_anything.
     Persistent (saved_anything_own γ x).
   Proof. rewrite /saved_anything_own; apply _. Qed.
 
+  Global Instance saved_anything_ne γ : NonExpansive (saved_anything_own γ).
+  Proof. solve_proper. Qed.
+  Global Instance saved_anything_proper γ : Proper ((≡) ==> (≡)) (saved_anything_own γ).
+  Proof. solve_proper. Qed.
+
   Lemma saved_anything_alloc_strong x (G : gset gname) :
     (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_anything_own γ x)%I.
   Proof. by apply own_alloc_strong. Qed.