\[\begin{array}{rll} \mathfrak{A} \models \phi \left[ s \right] & \text{if and only if} \: \mathfrak{A} \models \neg \alpha \left[ s \right] & \\ & \text{if and only if} \: \mathfrak{A} \not\models \alpha \left[ s \right] & \\ & \text{if and only if} \: \mathfrak{B} \not\models \alpha \left[ s \right] & \text{inductive hypothesis \\ & \text{if and only if} \: \mathfrak{B} \models \neg \alpha \left[ s \right] & \\ & \text{if and only if} \: \mathfrak{B} \models \phi \left[ s \right]. \end{array}\]