diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 89f8ef48d678da4b190e2426241efd31c666fde4..c3da8e276685a9203269b81aed29c4bf377a6aaa 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -94,10 +94,7 @@ Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -n> iProp Σ)
   saved_anything_own (F := A -n> ▶ ∙) γ (CofeMor Next ◎ Φ).
 
 Instance saved_pred_own_contractive `{savedPredG Σ A} γ : Contractive (saved_pred_own γ).
-Proof.
-  intros n Φ Φ' HΦ. rewrite /saved_pred_own /saved_anything_own /=.
-  do 3 f_equiv. intros x. rewrite /=. by f_contractive.
-Qed.
+Proof. rewrite /saved_pred_own=> n Φ Φ' ?. f_equiv=> x /=. by f_contractive. Qed.
 
 Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -n> iProp Σ) :
   (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I.