diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index 644a1141b..21d2f7be7 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -441,6 +441,8 @@ struct app_builder::imp {
     }
 
     expr mk_eq_rec(expr const & motive, expr const & H1, expr const & H2) {
+        if (is_constant(get_app_fn(H2), get_eq_refl_name()))
+            return H1;
         expr p       = m_ctx->whnf(m_ctx->infer(H2));
         expr lhs, rhs;
         if (!is_eq(p, lhs, rhs))
@@ -456,6 +458,8 @@ struct app_builder::imp {
     }
 
     expr mk_eq_drec(expr const & motive, expr const & H1, expr const & H2) {
+        if (is_constant(get_app_fn(H2), get_eq_refl_name()))
+            return H1;
         expr p       = m_ctx->whnf(m_ctx->infer(H2));
         expr lhs, rhs;
         if (!is_eq(p, lhs, rhs))
diff --git a/tests/lean/run/blast_cc10.lean b/tests/lean/run/blast_cc10.lean
new file mode 100644
index 000000000..a11b62670
--- /dev/null
+++ b/tests/lean/run/blast_cc10.lean
@@ -0,0 +1,7 @@
+set_option blast.subst false
+set_option blast.simp  false
+
+definition t1 (a b : nat) : (a = b ↔ a = b) :=
+by blast
+
+print t1