Constraints induced by parse-in-range.
Theorem: constraints-from-parse-in-range
(defthm constraints-from-parse-in-range (implies (not (mv-nth 0 (parse-in-range min max input))) (and (<= (nfix min) (nfix (car input))) (<= (nfix (car input)) (nfix max)))) :rule-classes nil)