Base case of the completeness lemma for parse-conc-rest-comp.
Theorem: parse-conc-rest-comp-when-tree-match-base-case
(defthm parse-conc-rest-comp-when-tree-match-base-case (implies (mv-nth 0 (parse-1*cwsp input)) (pred-conc-rest-comp input)))