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