Fix false Valid results from empty types and type classes

[RSoulatIOHK]

Blaster reports Valid for ∀ α : Type, (∀ _ : α, False) → False, although α := Empty refutes it. The same problem affects function spaces and classes such as Inhabited α: both unused-quantifier elimination and SMT class-binder erasure assumed nonemptiness without evidence.

Require an inhabitant before dropping a domain. Search global Nonempty instances and bounded constructor/function witnesses, excluding retained local instances that may belong to a closed binder. This also supports inhabited classes and constructor fields without treating every class as inhabited. Preserve SMT membership constraints for classes whose nonemptiness is unknown.

The tests include four kernel-checked counterexample proofs, five solver regressions requiring Falsified, a closed-local-instance regression, and positive coverage for LT, BEq, constructor fields and function codomains. Seventeen existing optimizer expectations were corrected to preserve vacuity or recognize newly supported inhabited domains.

Validation: the full optimizer suite and all new/old fixed-issue tests pass. A full lake test run with a uniform 30-second Z3 process cap passed every module except the existing nonlinear arithmetic case at Tests/Smt/SmtNat/SmtNatMod.lean:37, which timed out. The pristine beta suite also stalled in that module for six minutes without a cap; its bounded rerun passed. This solver-sensitive performance case is being addressed in a following optimization PR rather than weakening its expected verdict.

Stacked on #223; base branch fix/beta-proof-irrelevance.

Fixes #226. Regression: Tests/FixedIssues/Issue226.lean.

Follow-up: the complete stack through #230 passes lake test with the same 30-second Z3 process cap. #230 removes the nonlinear modulo bottleneck through a kernel-justified optimizer rule.