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