Constraints induced by a tree
that matches
Theorem:
(defthm constraints-from-tree-match-?-%i-when-nonempty (implies (and (tree-match-element-p tree (?_ (/_ "%i")) *grammar*) (consp (tree->string tree))) (and (equal (car (tree->string tree)) (char-code #\%)) (member-equal (cadr (tree->string tree)) (chars=>nats '(#\I #\i))))) :rule-classes nil)