Theorems about results of std/strings functions that return lists of hexadecimal digit characters.
Those std/strings are accompanied by theorems that they return hex-digit-char-list*p, but they in fact return true lists, so here we add theorems that they return hex-digit-char-listp.
Theorem:
(defthm hex-digit-char-listp-of-basic-nat-to-hex-chars (hex-digit-char-listp (basic-nat-to-hex-chars nat)))
Theorem:
(defthm hex-digit-char-listp-of-nat-to-hex-chars-aux (implies (hex-digit-char-listp acc) (hex-digit-char-listp (nat-to-hex-chars-aux nat acc))))
Theorem:
(defthm hex-digit-char-listp-of-nat-to-hex-chars (hex-digit-char-listp (nat-to-hex-chars nat)))