diff --git a/prelude/tactics.v b/prelude/tactics.v
index a9c3458e680f0e8fdfff53f6410ebb41e433524e..fabd259de524e37c005cc2359f962ec8f334ff8a 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -251,8 +251,10 @@ Ltac setoid_subst :=
   end.
 
 (** f_equiv works on goals of the form "f _ = f _", for any relation and any
-    number of arguments. It looks for an appropriate "Proper" instance, and
-    applies it. *)
+number of arguments. It looks for an appropriate "Proper" instance, and applies
+it. The tactic is somewhat limited, since it cannot be used to backtrack on
+the Proper instances that has been found. To that end, we try to ensure the
+trivial instance in which the resulting goals have an [eq]. *)
 Ltac f_equiv :=
   match goal with
   | _ => reflexivity
@@ -263,10 +265,16 @@ Ltac f_equiv :=
   | |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
     destruct x
   (* First assume that the arguments need the same relation as the result *)
-  | |- ?R (?f ?x) (?f _) =>
-    apply (_ : Proper (R ==> R) f)
-  | |- ?R (?f ?x ?y) (?f _ _) =>
-    apply (_ : Proper (R ==> R ==> R) f)
+  | |- ?R (?f ?x) (?f _) => apply (_ : Proper (R ==> R) f)
+  (* For the case in which R is polymorphic, or an operational type class,
+  like equiv. *)
+  | |- (?R _) (?f ?x) (?f _) => apply (_ : Proper (R _ ==> _) f)
+  | |- (?R _ _) (?f ?x) (?f _) => apply (_ : Proper (R _ _ ==> _) f)
+  | |- (?R _ _ _) (?f ?x) (?f _) => apply (_ : Proper (R _ _ _ ==> _) f)
+  | |- (?R _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ ==> R _ ==> _) f)
+  | |- (?R _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ ==> R _ _ ==> _) f)
+  | |- (?R _ _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> _) f)
+  | |- (?R _ _ _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ _ _ ==> R _ _ _ _ ==> _) f)
   (* 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? *)
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 8999eda05ec6cc0a5032e562c13180a9cc8ea1f9..b3532b64a92e0770a1298391afc16d1a66e19dab 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -45,7 +45,7 @@ Implicit Types P Q : iProp.
 
 (* FIXME: solve_proper picks the eq ==> instance for Next. *)
 Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
-Proof. intros P P' HP. by rewrite /box_own_prop HP. Qed.
+Proof. solve_proper. Qed.
 Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (box_inv γ).
 Proof. solve_proper. Qed.
 Global Instance box_slice_ne n γ : Proper (dist n ==> dist n) (box_slice N γ).