diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 9997c5c4bae25b969a73c9ff488296b0ca942d1e..b51402803548af145d104f6a582edbf799f359f6 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -620,9 +620,9 @@ Definition ccompose {A B C}
   (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g).
 Instance: Params (@ccompose) 3.
 Infix "â—Ž" := ccompose (at level 40, left associativity).
-Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n :
-  f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2.
-Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
+Global Instance ccompose_ne {A B C} :
+  NonExpansive2 (@ccompose A B C).
+Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
 
 (* Function space maps *)
 Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 89f8ef48d678da4b190e2426241efd31c666fde4..b1d1c462a29a1843ff5af67d462f4914c159e15d 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -95,8 +95,7 @@ Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A -n> iProp Σ)
 
 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.
+  solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | f_contractive | f_equiv ]).
 Qed.
 
 Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A -n> iProp Σ) :