Constraints induced by a terminated tree that matches
Theorem:
(defthm constraints-from-tree-match-equal-/-equal-slash (implies (tree-match-element-p tree (!_ (/_ "=") (/_ "=/")) *grammar*) (equal (car (tree->string tree)) (char-code #\=))) :rule-classes nil)