From fc6c8e0348618c4215f33ddb14755366aec7aaca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Nov 2020 14:46:28 -0800
Subject: [PATCH] fix: beta reduce value at `processAssignmentFOApprox`

---
 src/Lean/Meta/ExprDefEq.lean   | 1 +
 tests/lean/run/concatElim.lean | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 98894e0036..55c7dbff38 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -675,6 +675,7 @@ private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr)
       pure false
     else
       trace[Meta.isDefEq.foApprox]! "{mvar} {args} := {v}"
+      let v := v.headBeta
       if (← commitWhen $ processAssignmentFOApproxAux mvar args v) then
         pure true
       else
diff --git a/tests/lean/run/concatElim.lean b/tests/lean/run/concatElim.lean
index f0d9e6488e..0879a6bf6f 100644
--- a/tests/lean/run/concatElim.lean
+++ b/tests/lean/run/concatElim.lean
@@ -88,7 +88,7 @@ def concatElim {α}
 def test (xs : List Nat) : IO Unit :=
   concatElim (motive := fun _ => IO Unit)
     (fun _ => pure ())
-    (fun xs x (r : IO Unit) => do IO.println s!"step xs: {xs} x: {x}"; r) -- TODO: check why we need (r : IO Unit)
+    (fun xs x r => do IO.println s!"step xs: {xs} x: {x}"; r)
     xs
 
 #eval test [1, 2, 3, 4]