Constraints induced by parse-wsp/vchar.
Theorem:
(defthm constraints-from-parse-wsp/vchar (implies (not (mv-nth 0 (parse-wsp/vchar input))) (or (equal (car input) (char-code #\Tab)) (and (<= (char-code #\Space) (car input)) (<= (car input) (char-code #\~))))))