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