Proof of grammar-boolean-literalp from boolean-literalp.
This is proved using boolean-literal-tree
as witness for the existential quantification:
if
Theorem:
(defthm grammar-boolean-literalp-when-boolean-literalp (implies (boolean-literalp x) (grammar-boolean-literalp x)))