Add new array type and builtins to Agda metatheory

[kwxm]

See #6727. We need to add the new array builtin functions (and type) to the metatheory. Previously we were able to get away with doing this in a separate PR after adding the builtins to plutus-core, but now that other things depend on the metatheory it may be necessary to do it in the same PR to avoid build errors in CI.