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