Solution (source code)

= Solution

Under any <Boolean valuation> there are two possibilities. If $\neg(\psi\to\chi)$ is false, the outer <logical implication> is true by <vacuous truth>. If it is true, then $\psi\to\chi$ is false, which forces $\psi$ true and $\chi$ false. In that case $\neg\chi$ is true, so the outer <logical implication> is again true. These possibilities exhaust the <truth values> of its antecedent; therefore
$$
\boxed{\models\neg(\psi\to\chi)\to\neg\chi.}
$$