fix(grind): handle dot notation on local variables in parameters

When a grind parameter like `n.triv` is given, where `n` is a local
variable and `triv` is a theorem that takes `n` as an argument (so
`n.triv` means `Nat.triv n`), grind was incorrectly rejecting it with
"redundant parameter" because it detected that the identifier resolved
to a local variable via `resolveLocalName`.

The fix checks if `resolveLocalName` returns field projections (non-empty
list), indicating dot notation. In that case, we process the parameter
as a term expression to let elaboration resolve the dot notation properly,
rather than trying to resolve it as a global constant name.

Fixes the issue where `grind [x.exp_pos]` was rejected even though
`x.exp_pos` elaborates to `Real.exp_pos x`, a valid theorem application.

🤖 Prepared with Claude Code
2 files changed