Constraints induced by parse-wsp.
Theorem: constraints-from-parse-wsp
(defthm constraints-from-parse-wsp (implies (not (mv-nth 0 (parse-wsp input))) (member-equal (car input) (chars=>nats '(#\Tab #\Space)))) :rule-classes nil)