diff --git a/theories/tactics.v b/theories/tactics.v
index 0e0adb0e0571f433f1c22549ff06e4b8ab6539f8..43155ebf220fdf1c147c28dee7990c90f3c4d9d0 100644
--- a/theories/tactics.v
+++ b/theories/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? *)