Constraints induced by parse-rulename.
Theorem:
(defthm constraints-from-parse-rulename (implies (not (mv-nth 0 (parse-rulename input))) (or (and (<= (char-code #\A) (car input)) (<= (car input) (char-code #\Z))) (and (<= (char-code #\a) (car input)) (<= (car input) (char-code #\z))))) :rule-classes nil)