From f326e731a03b0d7129a7053cc156088d43c01178 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 22 Nov 2015 15:37:32 -0800
Subject: [PATCH] fix(library/blast/subst_action): do not apply subst to (H : a
 = a), let the discard_action to get rid of it

---
 src/library/blast/subst_action.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/library/blast/subst_action.cpp b/src/library/blast/subst_action.cpp
index f82bc5c17..7976612a1 100644
--- a/src/library/blast/subst_action.cpp
+++ b/src/library/blast/subst_action.cpp
@@ -51,6 +51,8 @@ bool subst_core(hypothesis_idx hidx) {
     expr type = h.get_type();
     expr lhs, rhs;
     lean_verify(is_eq(type, lhs, rhs));
+    if (is_def_eq(lhs, rhs))
+        return false;
     lean_assert(is_href(rhs));
     try {
         hypothesis_idx_buffer_set to_revert;