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