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