Dumb technical lemma showing that we always get a good plaintoken as long as we're using a valid keyword table.
Theorem:
(defthm vl-plaintokentype-p-of-vl-keyword-lookup (implies (vl-keyword-table-p table) (equal (vl-plaintokentype-p (vl-keyword-lookup str table)) (if (vl-keyword-lookup str table) t nil))))