diff --git a/src/Rewriter/Rewriter/ProofsCommonTactics.v b/src/Rewriter/Rewriter/ProofsCommonTactics.v
index 162add0ab..01cd01529 100644
--- a/src/Rewriter/Rewriter/ProofsCommonTactics.v
+++ b/src/Rewriter/Rewriter/ProofsCommonTactics.v
@@ -490,8 +490,10 @@ Module Compilers.
              [ now
                  let H := fresh in
                  cbv [Proper respectful] in *;
-                 intro H; eapply H; intros; subst; eauto
+                 intro H; eapply H; intros; subst; eauto;
+                 prove_eq_by_Proper
              | first [ now typeclasses eauto
+                     | now cbv [Proper respectful] in *; typeclasses eauto with core
                      | idtac "WARNING: Could not find Proper instance";
                        clear;
                        print_context_and_goal ();