Base case of the completeness lemma for parse-option.
Theorem: parse-option-when-tree-match-base-case
(defthm parse-option-when-tree-match-base-case (implies (mv-nth 0 (parse-ichar #\[ input)) (pred-option input)))