[audit] Unguarded argument-qualifier emission at the uninterpreted-function `cstr` and coercion `co_cstr` sites

## Summary

Tracking/audit issue for two more sites that emit a qualifier-constrained `forall` over quantified variables **without** premising those variables with their domain qualifiers — the same class as #194, but at the uninterpreted-function codomain (`*_cstr`) and coercion (`*_co_cstr`) sites. Unlike #194 these over-constrain in the "safe" direction (they can only push results toward spurious `Valid`, never toward spurious `Falsified`), and I have **no exploit** for them today. Filing to audit and to keep them consistent with the guarded template once #194 is fixed.

## Affected code (main @ `3a141c8`)

- `Blaster/Smt/Translate/Application.lean:770` — `generateUndeclaredFun`: codomain constraint
`assertTerm (mkForallTerm none co_quantifiers forallBody pattern)` where `forallBody ← createPredQualifierAppAux f_applyTerm retType`. The argument quantifiers `co_quantifiers` (`@x0 … @xn`) carry no `@is @xi =>` premise; it asserts `(@is (s @x0 … @xn))` for *all* carrier values, not just qualified ones.
- `Blaster/Smt/Translate/Application.lean:405` — `getConversionFunction`: coercion codomain constraint
`assertTerm (mkForallTerm none coeQuant coDomain patterns)` with `coDomain ← createPredQualifierAppAux f_coeTerm toType`. Same shape: `@x` in the source sort is unguarded.

## Correct guarded template

`Blaster/Smt/Translate/Application.lean:833` (`translateIndTypeExpr?`, the abstract-type inhabitation constraint) is the intended pattern:

```
let forallBody := impliesSmt predQualifier instPred
assertTerm (mkForallTerm none #[(xsym, st)] forallBody none)
```

i.e. `(forall ((@x st)) (=> (@is @x) …))`. The `:770` and `:405` sites should adopt the same `impliesSmt …` premise for each quantified argument.

## Why "audit" and not "critical"

Asserting a codomain/coercion property for *more* carrier values than necessary only strengthens the background theory in the direction that makes negated goals *easier* to refute (`unsat` → `Valid`). Whether this can be turned into a concrete spurious `Valid` depends on interactions with the qualifier definitions (e.g. `Nat = Int` letting off-domain `@x` participate). I could not construct one; #194 is the demonstrated soundness bug of this class. This issue is a checklist item to (a) fix these two sites together with #194 and (b) sweep for any other `mkForallTerm none ` without an `impliesSmt` guard.

## Environment

- input-output-hk/Lean-blaster `main` @ `3a141c8`; Lean `v4.24.0`; Z3 4.15.2

## Severity

Audit / tracking — same class as #194, not yet exploited.

## Confirmed false Valid on beta, 9 September 2026

The uninterpreted-function codomain constraint has a concrete soundness failure on `beta-lambda-cache-optimization` (`bafdd4f7`) and the review stack through #230. No assumptions about `hiddenId` are axioms: it is an opaque, well-typed definition.

```lean
import Blaster
namespace Issue196Probe
opaque hiddenId {α : Type} (x : α) : α := x
example : ¬ (∀ α : Type, (∀ x : α, hiddenId x = x) → ∃ _ : α, True) := by
intro h
obtain ⟨x, _⟩ := h Empty (fun x => Empty.elim x)
exact Empty.elim x
#blaster (gen-cex: 0) (solve-result: 1) (timeout: 5)
[∀ α : Type, (∀ x : α, hiddenId x = x) → ∃ _ : α, True]
end Issue196Probe
```

Actual: `Unexpected Valid`. Expected: `Falsified`. The kernel counterexample chooses `Empty`. The unconditional codomain assertion for `hiddenId : α → α` forces `α` to have a member even when its domain is empty. Guarding each argument with its domain membership prevents that fabricated inhabitant. The separate coercion-site audit remains open.

Read Blaster/Smt/Translate/Application.lean at lines 405 and 770, then compare the guarded template at line 833. Run the supplied Issue196Probe against the stated beta-lambda-cache-optimization revision and verify that the codomain case no longer reports Unexpected Valid; the coercion site and any matching unguarded forall emissions should also be audited.

Written by the indexing model from the issue text.