From 8258cfe2a1111aa1d3304fadce6068950fe9e444 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 21 Jan 2026 06:05:43 -0800
Subject: [PATCH] fix: preprocessLCtx (#12081)

This PR fixes a bug in the `Sym.preprocessLCtx` function.
---
 src/Lean/Meta/Sym/Util.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Meta/Sym/Util.lean b/src/Lean/Meta/Sym/Util.lean
index 5ed5889c75..509ba81d8e 100644
--- a/src/Lean/Meta/Sym/Util.lean
+++ b/src/Lean/Meta/Sym/Util.lean
@@ -74,6 +74,7 @@ def preprocessLCtx (lctx : LocalContext) : SymM LocalContext := do
         let type ← preprocessExpr type
         let value ← preprocessExpr value
         pure <| LocalDecl.ldecl index fvarId userName type value nondep kind
+    index := index + 1
     decls := decls.push (some decl)
     fvarIdToDecl := fvarIdToDecl.insert decl.fvarId decl
   return { fvarIdToDecl, decls, auxDeclToFullName }