diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp
index 4f07f9542c..15cc529136 100644
--- a/src/library/congr_lemma_manager.cpp
+++ b/src/library/congr_lemma_manager.cpp
@@ -147,7 +147,7 @@ struct congr_lemma_manager::imp {
 
     optional<result> mk_congr_simp(expr const & fn, buffer<param_info> const & pinfos, buffer<congr_arg_kind> const & kinds) {
         try {
-            expr fn_type = whnf(infer(fn));
+            expr fn_type = relaxed_whnf(infer(fn));
             name e_name("e");
             buffer<expr> lhss;
             buffer<expr> rhss;          // it contains the right-hand-side argument
@@ -183,7 +183,7 @@ struct congr_lemma_manager::imp {
                     eqs.push_back(none_expr());
                     break;
                 }}
-                fn_type  = whnf(instantiate(binding_body(fn_type), lhs));
+                fn_type  = relaxed_whnf(instantiate(binding_body(fn_type), lhs));
             }
             expr lhs = mk_app(fn, lhss);
             expr rhs = mk_app(fn, rhss);
diff --git a/tests/lean/run/blast_fun_info_bug.lean b/tests/lean/run/blast_fun_info_bug.lean
index 40795297e1..1d04e48261 100644
--- a/tests/lean/run/blast_fun_info_bug.lean
+++ b/tests/lean/run/blast_fun_info_bug.lean
@@ -1,4 +1,10 @@
 definition set (A : Type) := A → Prop
+set_option blast.strategy "preprocess"
+
+example {A : Type} (s : set A) (a b : A) : a = b → s a → s b :=
+by blast
+
+set_option blast.strategy "cc"
 
 example {A : Type} (s : set A) (a b : A) : a = b → s a → s b :=
 by blast