A theory of all functions specific to 1-dimensional arrays.
This theory must be DISABLEd in order for the lemmas exported by the "array1" book to be applicable.
