This sequent is not provable. $\mathcal{M} : p = T, q = T$ \\ $\mathcal{M} \nmodels (p \imp q) \land \neg q$