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)