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