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