[Bug]: "Inductive datatype with instance parameters not supported: `BitVec" on UInt8-level byte encoding (PlutusCoreBlaster `encodeBytestring` / the `serialiseData` builtin)

## Description

Goals that force symbolic translation of PlutusCoreBlaster's byte-level CBOR encoding fail with:

```
error: Inductive datatype with instance parameters not supported: `BitVec
```

`UInt8` is not unsupported wholesale, a plain arithmetic goal on `UInt8` literals proves fine (see Additional Context) — but the encoder's bytestring path ([`encodeBytestring`](https://github.com/input-output-hk/PlutusCoreBlaster/blob/a04042c4b7b19c66e7e6fa5bbcc3b1c985894ed0/PlutusCore/Cbor/Basic.lean), reached from [`encodeData`](https://github.com/input-output-hk/PlutusCoreBlaster/blob/a04042c4b7b19c66e7e6fa5bbcc3b1c985894ed0/PlutusCore/Cbor/Basic.lean#L127) on any `B` leaf, and the header/tag encoding reached from `Constr`) hits a `BitVec`-backed construct the translator rejects.

Practical impact: this is the second, independent wall in front of the `serialiseData` builtin (the first is the non-termination reported in #152 . Bytestring leaves are ubiquitous in real on-chain `Data` (script hashes, policy IDs, asset names), so even validator shapes that avoid #152 's recursive path cannot be proven, this one at least fails loudly instead of hanging.

## Steps to Reproduce

Run inside a PlutusCoreBlaster checkout (`main` @ `a04042c4`), or any Lake package depending on it, with `lake env lean `.

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

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

-- Bytestring leaf: no Data-level recursion involved.
theorem ser_b : encodeData (Data.B { data := "abc" }) ≠ none := by blaster
-- error: Inductive datatype with instance parameters not supported: `BitVec

-- Same error on an empty constructor (tag/header encoding, no fields):
theorem ser_constr : encodeData (Data.Constr 0 []) ≠ none := by blaster
```

## Expected Behavior

Either a translation to SMT bitvector theory (z3 supports it natively), or, failing that, a diagnostic that points at the offending definition/subterm so the user can tell which part of their goal is untranslatable. Given how common byte-level manipulation is in UPLC-adjacent code, actual `BitVec` support would be the valuable outcome.

## Actual Behavior

Immediate error at the theorem, before the solver is invoked:

```
error: Inductive datatype with instance parameters not supported: `BitVec
```

## Lean Version

4.24.0

## Z3 Version

4.15.2 (not reached, the error occurs during translation)

## Additional Context

- Lean-blaster `main` @ `c576289cb55412b359411d6c89568f95af50730c`; PlutusCoreBlaster `main` @ `a04042c4b7b19c66e7e6fa5bbcc3b1c985894ed0`; Linux x86_64.
- Plain `UInt8` arithmetic on literals is fine, so the rejection is narrower than "any UInt8":

```lean
import Blaster
def bump (x : UInt8) : UInt8 := x + 1
theorem bump_one : bump 1 = 2 := by blaster -- ✅ Valid
```

- Workaround we to continue testing (same as in #152 : an `opaque` alias for the `SerializeData` builtin's encoder, mirroring PlutusCoreBlaster's existing `opaque` hash builtins, symbolic tools then see an uninterpreted function and never reach the byte-level code. Offered upstream as [PlutusCoreBlaster PR#27](https://github.com/input-output-hk/PlutusCoreBlaster/pull/27).

Reproduce the failure with the encodeData examples in PlutusCore/Cbor/Basic.lean, especially encodeBytestring and the Constr header/tag path, using the supplied Lean and Z3 versions. Trace the translator's BitVec rejection and determine whether the work should provide SMT bitvector translation or a diagnostic that identifies the offending definition or subterm.

Written by the indexing model from the issue text.