NEAT test suite: missing builtins + investigation

The type used to represent builtin types in the NEAT generator code is missing support for `Array` and `Value`. The type is defined in https://github.com/IntersectMBO/plutus/blob/321c5e5a435ffbf5f9fd20c764d637560d6e9460/plutus-core/testlib/PlutusCore/Generators/NEAT/Type.agda#L48, and its [corresponding Haskell file](https://github.com/IntersectMBO/plutus/blob/321c5e5a435ffbf5f9fd20c764d637560d6e9460/plutus-core/testlib/PlutusCore/Generators/NEAT/Type.hs) must be generated with `agda-to-hs` and checked into the codebase.

One question which should be investigated as part of this issue is why are we using `agda-to-hs`, if this Agda module (or others, if there are any others) are also used the metatheory in some way.

The https://github.com/IntersectMBO/plutus/pull/7883 PR makes some improvements to the NEAT tests, but we need to understand what other limitations/issues there are and come up with a strategy. Related issue https://github.com/IntersectMBO/plutus/issues/6075.

Inspect plutus-core/testlib/PlutusCore/Generators/NEAT/Type.agda and its generated Type.hs, then review how agda-to-hs is used for the NEAT tests and any metatheory references. The concrete result should support Array and Value, regenerate and check in Type.hs, and document why agda-to-hs is used plus a strategy for the remaining limitations, including PR 7883 and issue 6075.

Written by the indexing model from the issue text.