Constraints induced by parse-bin-val.
Theorem: constraints-from-parse-bin-val
(defthm constraints-from-parse-bin-val (implies (not (mv-nth 0 (parse-bin-val input))) (member-equal (car input) (chars=>nats '(#\B #\b)))))