diff --git a/theories/tactics.v b/theories/tactics.v
index bc3a43b24cd592d77870835b5428103a6815e05b..4d19c7d5960b9169497ab4d17f48d2e27f4f83fe 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -325,30 +325,37 @@ Ltac setoid_subst :=
   | H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x
   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. 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 avoid the
-trivial instance in which the resulting goals have an [eq]. More generally,
-we try to "maintain" the relation of the current goal. For example,
-when having [Proper (equiv ==> dist) f] and [Proper (dist ==> dist) f], it will
-favor the second because the relation (dist) stays the same. *)
+(** The tactic [f_equiv] works on goals of the form [R (f _) (f _)], for any
+relation [R] and function [f]. The tactic looks for an appropriate [Proper]
+instance, and applies it.
+
+The tactic is somewhat limited:
+
+- Due to limitations of Ltac, this tactic is restricted to functions [f] up to
+  arity of 4.
+- The tactic cannot be used to backtrack on the [Proper] instances that has been
+  found. To that end, it tries to avoid using the trivial instance in which the
+  resulting goals have an [eq]. More generally, we try to "maintain" the
+  relation of the current goal. For example, given a goal [dist (f x) (f y)],
+  and instances [Proper (equiv ==> dist) f] and [Proper (dist ==> dist) f], the
+  tactic will favor the second [Proper] instance because the relation [dist]
+  stays the same. *)
 Ltac f_equiv :=
   match goal with
-  | |- pointwise_relation _ _ _ _ => intros ?
   (* We support matches on both sides, *if* they concern the same variable, or
      variables in some relation. *)
   | |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
     destruct x
   | H : ?R ?x ?y |- ?R2 (match ?x with _ => _ end) (match ?y with _ => _ end) =>
-     destruct H
-  (* First assume that the arguments need the same relation as the result *)
+    destruct H
+  (* First assume that the arguments need exactly the same relation as the result *)
   | |- ?R (?f _) _ => simple apply (_ : Proper (R ==> R) f)
   | |- ?R (?f _ _) _ => simple apply (_ : Proper (R ==> R ==> R) f)
   | |- ?R (?f _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R) f)
   | |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R) f)
-  (* For the case in which R is polymorphic, or an operational type class,
-  like equiv. *)
+  (* For the case in which [R] is polymorphic (like [eq]), or an operational
+  type class (like [equiv]), we try to find [Proper]s where the relation is the
+  same modulo some arguments. *)
   | |- (?R _) (?f _) _ => simple apply (_ : Proper (R _ ==> _) f)
   | |- (?R _ _) (?f _) _ => simple apply (_ : Proper (R _ _ ==> _) f)
   | |- (?R _ _ _) (?f _) _ => simple apply (_ : Proper (R _ _ _ ==> _) f)
@@ -361,20 +368,28 @@ Ltac f_equiv :=
   | |- (?R _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> _) f)
   | |- (?R _ _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> _) f)
   | |- (?R _ _ _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ R _ _ _ ==> R _ _ _ ==> _) f)
-  (* Next, try to infer the relation. Unfortunately, very often, it will turn
-     the goal into a Leibniz equality so we get stuck. *)
+  (* If we cannot find a [Proper] instance that involves the relation [R],
+  check if [R] is convertable to a [pointwise_relation], i.e., [R] is a
+  point-wise relation on functions. In this case, we introduce the function
+  argument, and [simpl]ify the resulting goal. *)
+  | |- ?R _ _ => eunify R (pointwise_relation _ _); intros ?; csimpl
+  (* Next, try to infer the relation by searching for an arbitrary [Proper]
+  instance. Unfortunately, very often, it will turn the goal into a Leibniz
+  equality so we get stuck. *)
   (* TODO: Can we exclude that instance? *)
   | |- ?R (?f _) _ => simple apply (_ : Proper (_ ==> R) f)
   | |- ?R (?f _ _) _ => simple apply (_ : Proper (_ ==> _ ==> R) f)
   | |- ?R (?f _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> R) f)
   | |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> R) f)
   (* In case the function symbol differs, but the arguments are the same,
-     maybe we have a pointwise_relation in our context. *)
+  maybe we have a [pointwise_relation] in our context. *)
   (* TODO: If only 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. *)
-  | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => simple apply H
-  | H : pointwise_relation _ (pointwise_relation _ ?R) ?f ?g |- ?R (?f ?x ?y) (?g ?x ?y) => simple apply H
+  | H : ?R' ?f ?g |- ?R (?f _) (?g _) => eunify R' (pointwise_relation _ _); simple apply H
+  | H : ?R' ?f ?g |- ?R (?f _ _) (?g _ _) => eunify R' (pointwise_relation _ _); simple apply H
+  | H : ?R' ?f ?g |- ?R (?f _ _ _) (?g _ _ _) => eunify R' (pointwise_relation _ _); simple apply H
+  | H : ?R' ?f ?g |- ?R (?f _ _ _ _) (?g _ _ _ _) => eunify R' (pointwise_relation _ _); simple apply H
   end;
   try simple apply reflexivity.
 Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.