From b508cf813ce2dee4a6058bc96661e6437ba62f9b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Feb 2016 15:36:53 -0800
Subject: [PATCH] perf(library/type_context): small optimization

---
 src/library/type_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 7a438251c..52cf433f5 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -743,8 +743,8 @@ bool type_context::is_def_eq_proof_irrel(expr const & e1, expr const & e2) {
     if (!m_env.prop_proof_irrel())
         return false;
     expr e1_type = infer(e1);
-    expr e2_type = infer(e2);
     if (is_prop(e1_type)) {
+        expr e2_type = infer(e2);
         scope s(*this);
         if (is_def_eq_core(e1_type, e2_type)) {
             s.commit();