Constraints induced by a non-empty list of terminated trees
that matches
Theorem:
(defthm constraints-from-tree-list-match-*cwsp-when-nonempty (implies (and (tree-list-match-repetition-p trees (*_ *c-wsp*) *grammar*) (tree-list-terminatedp trees) (consp (tree-list->string trees))) (member-equal (car (tree-list->string trees)) (chars=>nats '(#\Tab #\Return #\Space #\;)))) :rule-classes nil)