Parsing failure propagation from "-" to ("-" 1*DIGIT).
Theorem: fail-dash-1*digit-when-fail-dash
(defthm fail-dash-1*digit-when-fail-dash (implies (mv-nth 0 (parse-ichar #\- input)) (mv-nth 0 (parse-dash-1*digit input))))