Rewrite: (RESET-ARRAY1 name l) = (LIST (HEADER name l)).
This definition of RESET-ARRAY1 is logically equivalent to the actual definition. The actual definition, which includes a COMPRESS1 call, has the run-time side-effect of re-installing the new array. The COMPRESS1 is logically redundant, however.
This lemma is exported DISABLED, however this is the preferred definition to use to reason about RESET-ARRAY1.