Proof of grammar-jkeywordp from jkeywordp.
This is proved using jkeyword-tree as witness for the existential quantification: if x is a (non-restricted) keyword, then we can use its tree as witness, since its leaves are the keyword x as well.
Theorem: grammar-jkeywordp-when-jkeywordp
(defthm grammar-jkeywordp-when-jkeywordp (implies (jkeywordp x) (grammar-jkeywordp x)))
