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