Wrong ghosts declaration checking for `include=` specs

[danilych]

When specs are composed via include=, ghost variables "leak" up through the spec chain even when the spec that sets the ghost (the "setter spec") is not included in the current verification trace.

This means a spec is forced to declare_global a ghost variable that no spec in its entire trace ever sets — which is meaningless and blocks verification with error E0011.

fresh_object_address_spec (native_specs.move)
├── declares SpecFreshObjectAddress ghost
├── SETS ghost via ensures()
│
enter_market_inner_spec (include = fresh_object_address_spec)
├── declares SpecFreshObjectAddress ghost
├── uses global<SpecFreshObjectAddress>() in ensures()
├── ghost setter IS in scope ✅
│
enter_market_return_spec (include = enter_market_inner_spec)
├── does NOT include fresh_object_address_spec
├── ghost setter NOT in scope
├── system spec used for fresh_object_address (no ghost)
├── ❌ BUG: still required to declare SpecFreshObjectAddress
└── ERROR: "Ghost variable ... must be declared" (E0011)