fix(safe): rebind inner annotations under eta expansion

[oxura]

eta adds a lambda around an argument, but annotations inside that argument can still contain fixed levels from before the new binder. In the report, the inner Nat annotation ends up pointing at the new Bool variable.

Reopen the argument with the existing subst helper before wrapping it, preserving variables from the surrounding scope. The three eta callers now pass their current depth. The emitted annotation refers to x2 again, and the reported program passes --verdict. Neither bend.ts nor the Lean kernel changes.

Added the reported program as a proof regression. Checked it with both --check-only and --verdict, plus five existing eta/dependent-function files with --verdict; all passed with Lean 4.34.0. The kernel matches the base byte for byte (SHA-256 cc78aa9ff3491ff1b788797bdcab4cb98107dcb1730ed99834f6933b11d88335). The repository gate passes without changing caps; the related comments and verdict paragraph are shorter.

Fixes #1665.

[oxura]

I missed #1666, which opened while I was working on the report. We reached the same subst-based fix, so I’m closing this duplicate in favor of that PR.