From bce4912505a8ec79a674ff097835d8fb305df828 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Mar 2020 10:55:39 -0800
Subject: [PATCH] fix: remove bad condition

Recall that `processAssignmentFOApprox` will unfold `v` if possible.
---
 src/Init/Lean/Meta/ExprDefEq.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index 4991c45992..061fde22d8 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -616,7 +616,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
       else
         pure false;
     let useFOApprox : Unit → MetaM Bool := fun _ =>
-      if cfg.foApprox && v.isApp then
+      if cfg.foApprox then
         condM (processAssignmentFOApprox mvar args v)
           (pure true)
           (useConstApprox ())