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