Equivalence of boolean-literalp and grammar-boolean-literalp.
Theorem: boolean-literalp-is-grammar-boolean-literalp
(defthm boolean-literalp-is-grammar-boolean-literalp (equal (boolean-literalp x) (grammar-boolean-literalp x)))