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