diff --git a/prelude/tactics.v b/prelude/tactics.v
index 2a3a94cace9329d4675436ecea90b7dcbfd20186..f770fa9e87e0256ef8b733ff41e5937044d13b86 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -256,22 +256,28 @@ Ltac f_equiv :=
             let H := fresh "Proper" in
             assert (Proper (R ==> R ==> R) f) as H by (eapply _);
             apply H; clear H; f_equiv
-          (* Next, try to infer the relation *)
+          (* Next, try to infer the relation. Unfortunately, there is an instance
+             of Proper for (eq ==> _), which will always be matched. *)
+          (* TODO: Can we exclude that instance? *)
           (* TODO: If some of the arguments are the same, we could also
              query for "pointwise_relation"'s. But that leads to a combinatorial
              explosion about which arguments are and which are not the same. *)
           | |- ?R (?f ?x) (?f _) =>
-            let R1 := fresh "R" in let H := fresh "Proper" in
+            let R1 := fresh "R" in let H := fresh "HProp" in
             let T := type of x in evar (R1: relation T);
             assert (Proper (R1 ==> R) f) as H by (subst R1; eapply _);
             subst R1; apply H; clear H; f_equiv
           | |- ?R (?f ?x ?y) (?f _ _) =>
             let R1 := fresh "R" in let R2 := fresh "R" in
-            let H := fresh "Proper" in
+            let H := fresh "HProp" in
             let T1 := type of x in evar (R1: relation T1);
             let T2 := type of y in evar (R2: relation T2);
             assert (Proper (R1 ==> R2 ==> R) f) as H by (subst R1 R2; eapply _);
             subst R1 R2; apply H; clear H; f_equiv
+           (* In case the function symbol differs, but the arguments are the same,
+              maybe we have a pointwise_relation in our context. *)
+           | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) =>
+             apply H; f_equiv
          end | idtac (* Let the user solve this goal *)
         ].
 
@@ -288,6 +294,10 @@ Ltac solve_proper :=
          end;
   (* Unfold the head symbol, which is the one we are proving a new property about *)
   lazymatch goal with
+  | |- ?R (?f _ _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _ _) => unfold f
+  | |- ?R (?f _ _ _ _ _ _ _) (?f _ _ _ _ _ _ _) => unfold f
+  | |- ?R (?f _ _ _ _ _ _) (?f _ _ _ _ _ _) => unfold f
+  | |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => unfold f
   | |- ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f
   | |- ?R (?f _ _ _) (?f _ _ _) => unfold f
   | |- ?R (?f _ _) (?f _ _) => unfold f
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 15f435ff598bfb45902563395ca84190867f6e7e..3cb74b8085775e010663d62c0b884982bec3b65f 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -40,7 +40,7 @@ Section auth.
   Implicit Types γ : gname.
 
   Global Instance auth_own_ne n γ : Proper (dist n ==> dist n) (auth_own γ).
-  Proof. by rewrite auth_own_eq /auth_own_def=> a b ->. Qed.
+  Proof. rewrite auth_own_eq; solve_proper. Qed.
   Global Instance auth_own_proper γ : Proper ((≡) ==> (≡)) (auth_own γ).
   Proof. by rewrite auth_own_eq /auth_own_def=> a b ->. Qed.
   Global Instance auth_own_timeless γ a : TimelessP (auth_own γ a).
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index f2b597942774fdfa33346f2d12f6affe3bafbd2f..d6dee8b2fdb009984a89cc684c467037b723f083 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -9,6 +9,7 @@ Local Hint Extern 10 (✓{_} _) =>
   | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
   end; solve_validN.
 
+(* TODO: Consider sealing this, like all the definitions in upred.v. *)
 Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
   {| uPred_holds n r1 := ∀ rf k Ef σ,
        0 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ →
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 2d369c1b2dfef7a20e43a5185e4740abbafc848f..f48b69809f533e38f0fec7504869b35fc3e672f7 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -52,22 +52,20 @@ Section sts.
   (** Setoids *)
   Global Instance sts_inv_ne n γ :
     Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv γ).
-  Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
+  Proof. solve_proper. Qed.
   Global Instance sts_inv_proper γ :
     Proper (pointwise_relation _ (≡) ==> (≡)) (sts_inv γ).
-  Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
+  Proof. solve_proper. Qed.
   Global Instance sts_ownS_proper γ : Proper ((≡) ==> (≡) ==> (≡)) (sts_ownS γ).
-  Proof.
-    intros S1 S2 HS T1 T2 HT. by rewrite !sts_ownS_eq /sts_ownS_def HS HT.
-  Qed.
+  Proof. rewrite sts_ownS_eq. solve_proper. Qed.
   Global Instance sts_own_proper γ s : Proper ((≡) ==> (≡)) (sts_own γ s).
-  Proof. intros T1 T2 HT. by rewrite !sts_own_eq /sts_own_def HT. Qed.
+  Proof. rewrite sts_own_eq. solve_proper. Qed.
   Global Instance sts_ctx_ne n γ N :
     Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N).
-  Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
+  Proof. solve_proper. Qed.
   Global Instance sts_ctx_proper γ N :
     Proper (pointwise_relation _ (≡) ==> (≡)) (sts_ctx γ N).
-  Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
+  Proof. solve_proper. Qed.
 
   (* The same rule as implication does *not* hold, as could be shown using
      sts_frag_included. *)
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 213bbcbb4b41592d8d6195d42380db9e829a9089..0c452428a5aaf8e907a5fe931d42c14ea039c40f 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -30,6 +30,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset)
        wp_go (E ∪ Ef) (wp_pre E Φ)
                       (wp_pre ⊤ (λ _, True%I)) k rf e1 σ1) →
      wp_pre E Φ e1 n r1.
+(* TODO: Consider sealing this, like all the definitions in upred.v. *)
 Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
   (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}.
 Next Obligation.