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