Solution (source code)

= Solution

A <subformula> beginning at the first opening parenthesis equals the whole <logical formula> by <prefix-freeness of fully parenthesized formulas>. Every other <subformula> is the <logical formula> of a proper syntax subtree, by the <parsing> argument in part (iii). The two children of the root are precisely $\psi$ and $\chi$, so such a subtree lies entirely inside one of those children. In particular no <logical formula> substring can begin in $\psi$ and cross the principal <logical implication> symbol into $\chi$.

Conversely, each <subformula> of either child is visibly a substring of the whole expression, as is the whole expression itself. Thus
$$
\boxed{\operatorname{Sub}((\psi\to\chi))=\{(\psi\to\chi)\}\cup\operatorname{Sub}(\psi)\cup\operatorname{Sub}(\chi).}
$$
Together these cases identify the substring definition of a <subformula> with its usual syntax-tree definition.