diff --git a/theories/tactics.v b/theories/tactics.v
index 6a8d64ada235abb1befda8045271daeec6f653e7..6c2d5ecd910ad9c916364aac837aa6412e23c5ea 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -233,7 +233,7 @@ Ltac setoid_subst :=
     If it cannot solve an equality, it will leave that to the user. *)
 Ltac f_equiv :=
   (* Deal with "pointwise_relation" *)
-  try lazymatch goal with
+  repeat lazymatch goal with
     | |- pointwise_relation _ _ _ _ => intros ?
     end;
   (* Normalize away equalities. *)
@@ -249,13 +249,9 @@ Ltac f_equiv :=
             destruct x; f_equiv
           (* First assume that the arguments need the same relation as the result *)
           | |- ?R (?f ?x) (?f _) =>
-            let H := fresh "Proper" in
-            assert (Proper (R ==> R) f) as H by (eapply _);
-            apply H; clear H; f_equiv
+            apply (_ : Proper (R ==> R) f); f_equiv
           | |- ?R (?f ?x ?y) (?f _ _) =>
-            let H := fresh "Proper" in
-            assert (Proper (R ==> R ==> R) f) as H by (eapply _);
-            apply H; clear H; f_equiv
+            apply (_ : Proper (R ==> R ==> R) f); f_equiv
           (* 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? *)
@@ -263,17 +259,9 @@ 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. *)
           | |- ?R (?f ?x) (?f _) =>
-            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
+            apply (_ : Proper (_ ==> R) f); f_equiv
           | |- ?R (?f ?x ?y) (?f _ _) =>
-            let R1 := fresh "R" in let R2 := fresh "R" 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
+            apply (_ : Proper (_ ==> _ ==> R) f); 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) =>