[Metatheory] Fix eqDATA, array equality and remove builtinEq

[ana-pantilie]

Fixes https://github.com/IntersectMBO/plutus-private/issues/2418

---

As part of fixing the issue above, I tried out what @basetunnel and I discussed last week: moving primTrustMe from builtinEq to a dedicated function for each postulated type.

I think this new design is much safer. It's also cleaner because we now have one decision procedure for each builtin type, and one boolean checker derived from the decision procedure.

EDIT

Turns out the approach above doesn't work, and I've remembered why: the compiled decision procedures will not behave correctly, they'll just return yes. eqBuiltin was defined specifically for this purpose, to bypass this issue, since it would call Haskell's (==) on the Haskell ByteString/etc. first and return the right result based on that. At the typechecking level, the equality check would default to true and use Agda's unification algorithm to decide the result (yes or typechecking would get stuck).

---

This PR also fixes the problems with eqDATA described in the issue, and it also removes its TERMINATING pragma.

I also uncovered another bug, namely that Array equality would compile to constant true. This should also be fixed now.