Completeness theorem for parse-any.
Theorem: parse-any-of-cons
(defthm parse-any-of-cons (equal (parse-any (cons nat nats)) (mv nil (nfix nat) (nat-list-fix nats))))