Constraints induced by a tree that matches a case-insensitive character value notation.
Theorem:
(defthm constraints-from-tree-match-ichars (implies (tree-match-element-p tree (element-char-val (char-val-insensitive iprefix charstring)) *grammar*) (nats-match-insensitive-chars-p (tree->string tree) (explode charstring))) :rule-classes nil)