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 }