diff --git a/library/Init/Lean/LocalContext.lean b/library/Init/Lean/LocalContext.lean
index 8cc88b0307..582eee62eb 100644
--- a/library/Init/Lean/LocalContext.lean
+++ b/library/Init/Lean/LocalContext.lean
@@ -250,9 +250,12 @@ xs.size.foldRev (fun i b =>
     else
       Expr.forallE n bi ty b
   | some (LocalDecl.ldecl _ _ n ty val) =>
-    let ty  := ty.abstractRange i xs;
-    let val := val.abstractRange i xs;
-    Expr.letE n ty val b
+    if b.hasLooseBVar 0 then
+      let ty  := ty.abstractRange i xs;
+      let val := val.abstractRange i xs;
+      Expr.letE n ty val b
+    else
+      b
   | none => panic! "unknown free variable") b
 
 def mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
diff --git a/library/Init/Lean/MetavarContext.lean b/library/Init/Lean/MetavarContext.lean
index e79ea0283c..4f5908df14 100644
--- a/library/Init/Lean/MetavarContext.lean
+++ b/library/Init/Lean/MetavarContext.lean
@@ -567,9 +567,12 @@ do e ← abstractRange elimMVarDeps lctx xs xs.size e;
         else
           pure $ Expr.forallE n bi type e
       | some (LocalDecl.ldecl _ _ n type value) => do
-        type  ← abstractRange elimMVarDeps lctx xs i type;
-        value ← abstractRange elimMVarDeps lctx xs i value;
-        pure $ Expr.letE n type value e
+        if e.hasLooseBVar 0 then do
+          type  ← abstractRange elimMVarDeps lctx xs i type;
+          value ← abstractRange elimMVarDeps lctx xs i value;
+          pure $ Expr.letE n type value e
+        else
+          pure e
       | none => panic! "unknown free variable")
    e