Constraints induced by parse-htab.
Theorem: constraints-from-parse-htab
(defthm constraints-from-parse-htab (implies (not (mv-nth 0 (parse-htab input))) (equal (car input) (char-code #\Tab))) :rule-classes nil)