eqByteString and three BLS12-381 equalities are stubbed to always return true, not left as postulates

`eqByteString`, `eqBls12-381-G1-Element`, `eqBls12-381-G2-Element`, and `eqBls12-381-MlResult` in `plutus-metatheory/src/Utils.lagda.md` are all stubbed to unconditionally return `true`, rather than left as postulates:

```agda
eqByteString : ByteString → ByteString → Bool
eqByteString _ _ = Bool.true
{-# COMPILE GHC eqByteString = (==) #-}
```

Introduced in `1e7a0be3e` (#7059), alongside `eqDATA`'s real recursive implementation (which is fine -- it only bottoms out at `eqByteString` for `B` leaves).

**Why I'm not proposing a plain revert-to-postulate:** the consumer, `builtinEq` (`Untyped/Equality.lagda.md`), only uses the boolean to pick a branch; the branch that matters (`true`) then goes through `primTrustMe`, which only reduces to a usable proof when Agda's own definitional equality independently confirms the two sides match -- for genuinely different values it gets stuck rather than lying. If that's right, `primTrustMe` is the actual gatekeeper, not the boolean. A plain postulate, on the other hand, can't be `with`-split on at all, so reverting would likely break `builtinEq` for every input, not just mismatched ones.

The tension as I see it: this stub is good for keeping certified-compilation proofs computable, but bad if `hsEq`/`eqByteString` are ever used directly for testing or reasoning outside `builtinEq`'s `primTrustMe` gate -- nothing about their name or type stops that.

Live code: `Untyped/Equality.lagda.md` is imported by eight `VerifiedCompilation` certifier modules (`UCaseReduce`, `UInline`, `UCaseOfCase`, and others).

Read plutus-metatheory/src/Utils.lagda.md and Untyped/Equality.lagda.md first, then inspect the eight VerifiedCompilation certifier modules mentioned in the issue. Trace how builtinEq uses the boolean and primTrustMe, and determine a resolution that preserves certified-compilation behavior while addressing unsafe direct use. Done means the equality definitions and their consumer have an agreed, verified behavior.

Written by the indexing model from the issue text.