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