Solution (source code)

= Solution

The whole <logical formula> $\neg\psi$ is a <subformula> of itself, and any <subformula> of $\psi$ remains a contiguous substring after placing a <negation> symbol in front of $\psi$.

Conversely, a <subformula occurrence> starting at the first symbol of $\neg\psi$ is an initial <subformula>, so equals the whole <logical formula> by <prefix-freeness of fully parenthesized formulas>. An occurrence starting later lies wholly inside the following string $\psi$, and is therefore a <subformula> of $\psi$. Consequently
$$
\boxed{\operatorname{Sub}(\neg\psi)=\{\neg\psi\}\cup\operatorname{Sub}(\psi).}
$$
Here $\operatorname{Sub}$ records distinct <logical formulas>; multiple occurrences of the same <logical formula> do not create different elements of this <set>.