Proof of grammar-hex-digitp from hex-digitp.
This is proved using hex-digit-tree
as witness for the existential quantification:
if
Theorem:
(defthm grammar-hex-digitp-when-hex-digitp (implies (hex-digitp x) (grammar-hex-digitp (list x))))