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