[soundness] Qualifier-guarded extensionality + unguarded lambda-definition axioms make the SMT theory inconsistent (blaster admits `False`)

## Summary

`blaster` accepts a **false** theorem as `Valid` and lets the Lean kernel close `False`. The generated SMT theory is **inconsistent** because of a guard asymmetry between two families of assertions:

- **Extensionality / congruence** for a function sort quantify over the *qualified* domain: the inner `forall` is guarded by the domain qualifier (`@isNat @x => ...`).
- **Lambda definition constraints** (`*_def_cstr`) that pin a concrete lambda's values are emitted **unguarded**: they constrain `@apply lam x` for *every* element of the underlying carrier sort, including values that fail the domain qualifier (e.g. negative `Int` for `Nat`, since `Nat` is aliased to `Int`).

Extensionality then concludes that two lambdas which agree on the *qualified* domain are equal, while the unguarded `def_cstr`s force them to *disagree* off the qualified domain. That is a contradiction independent of the goal, so any negated goal is `unsat` and `blaster` reports `Valid`.

## Repro (self-contained)

```lean
import Blaster
set_option warn.sorry false
theorem bogus (l : List Nat) :
(l.all (fun y => decide (y < 3)) && l.all (fun y => decide (y = 0 ∨ y = 1 ∨ y = 2))) = true := by
blaster
theorem boom : False := by have h := bogus [5]; simp at h
#print axioms boom
```

Actual on `main` @ `3a141c8`:

```
✅ Valid
'boom' depends on axioms: [propext, Quot.sound, Blaster.Tactic.blasterProven]
```

`bogus` is false (`[5]` and `[3]` both refute it: `5 < 3` and `3 < 3` are false). Expected: `blaster` reports the goal is not valid (or generates a counterexample); the kernel must never accept `boom`.

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

- `Blaster/Smt/Translate/Application.lean:1248` — simple lambda (`V = ∅`) case:
`assertTerm (mkForallTerm none svars forallBody ...)` with `forallBody := eqSmt applyTerm sb`. **Unguarded** — `svars` carry no qualifier premise.
- `Blaster/Smt/Translate/Application.lean:1277` — global lambda (`V ≠ ∅`) case: same, `gvars` unguarded.
- `Blaster/Smt/Translate/Quantifier.lean:757` — extensionality's inner body **is** guarded: `innerForallBody := impliesSmt predAppX innerForallBody` (emitted at `:778`–`:780`).
- Contrast the correct, guarded template at `Blaster/Smt/Translate/Application.lean:833` (`impliesSmt predQualifier instPred`) and the abstract-type inhabitation constraint.

## Decisive SMT evidence

Extensionality as Blaster emits it — inner `forall` **guarded**:

```
(forall ((@x0 Nat)) (=> (@isNat @x0) (= (@apply @f @x0) (@apply @g @x0)))) ... => (= @f @g)
```

`def_cstr` as Blaster emits it — **unguarded** (no `@isNat` premise on `$8`):

```
(assert (forall (($8 Nat)) (= (@apply @lambda_uniq.783 $8) (< $8 3)) ...))
```

Reduced query with only these two assertion families and **no goal** is already `unsat` (the background theory is inconsistent):

```
$ z3 min_bad.smt2
unsat
```

The full Blaster-emitted query for the repro (`l4_orig.smt2`) is `unsat` → `Valid`. Guarding the two `def_cstr`s with `(=> (@isNat $8) ...)` (`l4_fixed.smt2`) flips it to `sat` with the correct countermodel:

```
$ z3 l4_fixed.smt2
sat
(define-fun $0 () (@List Int) (List.cons 3 List.nil)) ; i.e. l = [3]
```

## Exposed class

Any Bool/predicate lambda family over a *qualified* carrier sort: `Nat` (⊂ `Int`), `Fin`, `List`/datatype element invariants, structure invariant fields — wherever a domain qualifier is non-trivial and a concrete lambda's `def_cstr` is asserted. The `List.all (fun y => …)` shape above is the most common trigger.

## Fix direction

Guard the quantifiers of the `def_cstr` assertions at `Application.lean:1248` and `:1277` with the same qualifier premises the extensionality/congruence generation already uses (the `predAppX`/`impliesSmt` discipline in `generateFunInstDeclAux`, cf. `Quantifier.lean:751`–`:757`, and the guarded template at `Application.lean:833`). `l4_fixed.smt2` confirms this restores soundness and produces the real countermodel.

Do **not** "fix" this by *unguarding* extensionality instead: unguarded extensionality (agreement required on the whole carrier, incl. off-domain values) is sound-but-weaker (incomplete), whereas the guarded `def_cstr` version preserves extensionality's strength. There is an unmeasured completeness cost either way; guarding `def_cstr` is the strength-preserving choice.

## Likely origin

Likely introduced by PR #104 ("Properly handling sort universe at smt level", merged 2026-03-30, merge commit `750039d`). That PR **added** the extensionality domain guard — the diff introduces `innerForallBody := impliesSmt predAppX innerForallBody` and the `predApp{X,Y}` premises in `Quantifier.lean` — and **added** the guarded template at `Application.lean` (`impliesSmt predQualifier instPred`), but left the lambda `def_cstr` emission unguarded. Attribution is based on file-overlap and the guard being introduced in that diff, not a full guard-line bisection.

## Environment

- input-output-hk/Lean-blaster `main` @ `3a141c8d06f13e9c2840cfeb24fdb1eaa9b7f8f5`
- Lean `leanprover/lean4:v4.24.0`, Z3 4.15.2

## Severity

Critical — soundness. `blaster` admits provably false theorems and the kernel accepts `False` via `Blaster.Tactic.blasterProven`.