[Bug]: blaster never terminates translating structural recursion through a `List.foldlM` closure (PlutusCoreBlaster `encodeData` / the `serialiseData` builtin)

## Description

`by blaster` never returns (no error, no timeout, no counterexample) when the goal forces symbolic translation of a function whose recursion goes through a `List.foldlM` closure (a lambda passed to `foldlM` that recursively calls the enclosing function on list elements).

The real-world instance is PlutusCoreBlaster's CBOR encoder [`PlutusCore.Cbor.encodeData`](https://github.com/input-output-hk/PlutusCoreBlaster/blob/a04042c4b7b19c66e7e6fa5bbcc3b1c985894ed0/PlutusCore/Cbor/Basic.lean#L127), the model behind the `serialiseData` builtin. It is a total, structurally recursive definition (explicit `decreasing_by`), and `#eval` on any input is instant, the problem is only in symbolic translation. The consequence is that any imported UPLC validator that calls `serialiseData` on a non-trivial `Data` value cannot be proven at all: we hit this on a production Plutus V3 validator that checks `blake2b_256(serialiseData(config)) == stored_hash`, and a validator-level `blaster` run was left going for hours without producing anything.

The trigger is specifically the recursive/higher-order path: the same goal on an **empty** collection (which takes the encoder's non-recursive branch) proves valid in under a second.

## Steps to Reproduce

Run inside a PlutusCoreBlaster checkout (`main` @ `a04042c4`), or any Lake package depending on it, with `lake env lean `. Put each theorem in its own file, the second one blocks forever.

```lean
import Blaster
import PlutusCore.Cbor.Basic

open PlutusCore.Data (Data)
open PlutusCore.Cbor (encodeData)

-- Control: the empty list takes the encoder's non-recursive branch.
-- Result: ✅ Valid in 0.7 s.
theorem ser_nil : encodeData (Data.List []) = some "\x80" := by blaster

-- One element: forces a single unfolding of the foldlM closure.
-- Result: never returns.
theorem ser_one : encodeData (Data.List [Data.I 1]) ≠ none := by blaster
```

## Expected Behavior

A proof, a counterexample, or a diagnostic in finite time. For a total, structurally recursive function applied to a one-element list, on the order of the empty-list control (0.7 s).

## Actual Behavior

No output at all. The minimized theorem above was killed at 120 s; validator-level instances of the same shape ran for hours before being killed. While it spins, the `lean` process is CPU-bound (~100% of one core) with resident memory climbing past 1.2 GB within the first minute and **no z3 process is ever spawned**, so the divergence is in Blaster's translation/unfolding phase, before the solver is invoked.

## Lean Version

4.24.0

## Z3 Version

4.15.2 (never reached, the process diverges before the solver is invoked)

## Additional Context

- Lean-blaster `main` @ `c576289cb55412b359411d6c89568f95af50730c`; PlutusCoreBlaster `main` @ `a04042c4b7b19c66e7e6fa5bbcc3b1c985894ed0`; Linux x86_64.
- A synthetic function of the same shape (tiny inductive, recursion through a `foldlM` closure, explicit `decreasing_by`) does **not** hang but fails differently, a malformed SMT query, even on the empty-list case, which suggests the `foldlM`-closure translation path is fragile beyond this one hang:

```lean
import Blaster

inductive Tree where
| leaf : Int → Tree
| node : List Tree → Tree

def enc : Tree → Option String
| .leaf _ => .some "i"
| .node xs => List.foldlM (fun s a => do .some (s ++ (← enc a))) "" xs
decreasing_by
have : sizeOf a < sizeOf xs := by apply List.sizeOf_lt_of_mem; assumption
simp; omega

theorem enc_nil : enc (.node []) = some "" := by blaster
-- error: Unexpected smt error:
-- (error "line 112 column 111: unknown constant @List.foldlM._uniq.8298 ...")
```

- Workaround we continue testing with: give the `SerializeData` builtin's encoder the same treatment PlutusCoreBlaster already gives every hash builtin (`opaque blake2b_256` etc. in [`Crypto/Hash/Basic.lean`](https://github.com/input-output-hk/PlutusCoreBlaster/blob/a04042c4b7b19c66e7e6fa5bbcc3b1c985894ed0/PlutusCore/Crypto/Hash/Basic.lean#L41)), an `opaque` alias used only at the builtin dispatch, so symbolic tools see an uninterpreted function while compiled evaluation is unchanged. With that in place, the validator-level theorems that hung forever prove in ~6 s. Offered upstream as [PlutusCoreBlaster PR#27](https://github.com/input-output-hk/PlutusCoreBlaster/pull/27); the proper fix in Blaster itself is this issue (and #153 for the independent BitVec wall behind it).