From 81d2754cd244cc97efa686a93d66d5efed7aff5b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 24 Jul 2020 16:05:05 -0700
Subject: [PATCH] chore: add `headBeta` to avoid unnecessary applications
 introduced by metavariable management

---
 src/Lean/MetavarContext.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index b06404c4a8..8516d4126d 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -909,6 +909,7 @@ xs.size.foldRevM
     match lctx.getFVar! x with
     | LocalDecl.cdecl _ _ n type bi =>
       if !usedOnly || e.hasLooseBVar 0 then do
+        let type := type.headBeta;
         type ← abstractRange xs i type;
         if isLambda then
           pure (Lean.mkLambda n bi type e, num + 1)