diff --git a/src/Lean/Elab/DeclNameGen.lean b/src/Lean/Elab/DeclNameGen.lean
index 8d94e64353..2995bf4b22 100644
--- a/src/Lean/Elab/DeclNameGen.lean
+++ b/src/Lean/Elab/DeclNameGen.lean
@@ -51,6 +51,8 @@ Expressions can also be replaced by `.bvar 0` if they shouldn't be mentioned.
 -/
 private partial def winnowExpr (e : Expr) : MetaM Expr := do
   let rec visit (e : Expr) : MonadCacheT Expr Expr MetaM Expr := checkCache e fun _ => do
+    if ← isProof e then
+      return .bvar 0
     match e with
     | .app .. =>
       if let some e' ← getParentProjArg e then