diff --git a/theories/tactics.v b/theories/tactics.v
index 4b42a8f6f6fab451dabf069cf32632bdbe75e1b1..eb0b3969e41e71fa25961b09be691e24fa2bbbb5 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -316,6 +316,7 @@ Ltac f_equiv :=
      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
   end;
   try simple apply reflexivity.
 Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.