Indexed matcher fallback exposes a loose bound variable during normalization

Blaster throws `optimizeExpr: unexpected bound variable #0` while normalizing a known fallback branch of a well-founded recursive function whose matcher returns an indexed structure. The fallback should return its argument. Lean proves the equation with `simp`.

This arose while integrating a kernel-verified recursive UPLC specialization. No false `Valid` result has been demonstrated; the observed failure is a normalization exception.

Minimal repository-local reproducer (Lean 4.24.0):

```lean
import Tests.Utils
namespace BoundVariableIssue
structure Plan (n : Nat) where
worker : Nat → Nat

def recognize (n : Nat) : Option (Plan n) :=
match n with
| 0 => some { worker := fun x => x+1 }
| _ => none

def run (fuel n x : Nat) : Nat :=
match fuel with
| 0 => x
| fuel+1 =>
match recognize n with
| none => x
| some plan =>
let remaining := plan.worker fuel
if h : remaining < fuel then run remaining n x else x+1
termination_by fuel

example (x : Nat) : run 3 1 x = x := by simp [run, recognize]
attribute [local blaster_specialize 1] run
#testOptimize ["IndexedPlanFallback"] (fun x : Nat => run 3 1 x) ===> (fun x : Nat => x)
end BoundVariableIssue
```

Expected: the kernel example and `#testOptimize` both pass.

Actual: the kernel example passes; `#testOptimize` raises the bound-variable exception.

Removing the phantom `n : Nat` parameter from `Plan` (and using `Option Plan`) makes the normalization test pass. Replacing the record with `Option (Nat → Nat)` also passes. No proof field is needed to trigger the problem.

Confirmed at local review head `3eca6753`, based on PR #244's `47c8364d`, with profiling disabled. An isolated build against `47c8364d` is in progress to confirm the narrower base.

Searches for bound-variable and dependent-matcher issues/PRs did not find an overlapping fix. The fixing PR will include `Issue.lean` with a passing regression, following the review's issue-first workflow.

Start with the repository-local reproducer in the issue, especially the `#testOptimize` entry point and the `Tests.Utils` import. Compare the indexed `Plan` case with the documented phantom-parameter and function alternatives, then add the requested `Issue.lean` regression; done means both the kernel example and `#testOptimize` pass without the bound-variable exception.

Written by the indexing model from the issue text.