Equivalence of hex-digitp and grammar-hex-digitp.
Theorem: hex-digitp-is-grammar-hex-digitp
(defthm hex-digitp-is-grammar-hex-digitp (equal (hex-digitp x) (grammar-hex-digitp (list x))))