Constraints induced by parse-ichar.
Theorem: constraints-from-parse-ichar
(defthm constraints-from-parse-ichar (implies (not (mv-nth 0 (parse-ichar char input))) (nat-match-insensitive-char-p (car input) char)) :rule-classes nil)