linter.unusedSectionVars: does not detect variable uses in where clauses

The unused section variable linter does not detect when a variable is used inside a where clause.

MWE

variable (n : Nat)
include n

theorem foo : ∃ (_ : Nat), True := by
  exists k
  where
  k := n + 1

This produces a warning:

automatically included section variable(s) unused in theorem 'foo':
  n
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit n in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`

But n is used in the where clause (k := n + 1).

Discussion

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/unused.20section.20variable.20linter.20is.20buggy/near/565224606

Note: the same Zulip thread also reports a related issue where the linter warns about an instance that cannot be omitted because it's referenced in the type of another included variable.

Start by reproducing the MWE and tracing the unusedSectionVars linter entry point. Check why references from where clauses are missed, then verify that the example no longer reports n as unused. The linked Zulip discussion also notes a related instance-omission case that may need separate consideration.