diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 7baa97fdb2..b06404c4a8 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -769,9 +769,11 @@ xs.size.foldRevM
     let x := xs.get! i;
     match lctx.getFVar! x with
     | LocalDecl.cdecl _ _ n type bi => do
+      let type := type.headBeta;
       type ← abstractRangeAux elimMVarDeps xs i type;
       pure $ Lean.mkForall n bi type e
     | LocalDecl.ldecl _ _ n type value => do
+      let type := type.headBeta;
       type  ← abstractRangeAux elimMVarDeps xs i type;
       value ← abstractRangeAux elimMVarDeps xs i value;
       let e := mkLet n type value e;