Some tau rules about arrays.
Theorem:
(defthm not-errorp-when-arrayp (implies (or (schar-arrayp x) (uchar-arrayp x) (sshort-arrayp x) (ushort-arrayp x) (sint-arrayp x) (uint-arrayp x) (slong-arrayp x) (ulong-arrayp x) (sllong-arrayp x) (ullong-arrayp x)) (not (errorp x))) :rule-classes :tau-system)