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