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