 and an appeal to (Cut) here, with φ Tonk ψ as cut-formula, amounts to bringing home the bad  news.[30]  But of course this example simply makes vivid the fact that the Tonk rules in play are not Cut-inductive and there is no Cut-free proof of the desired sequent (at least in general: take φ = p, ψ = q). This is hardly surprising since the subformula property which Cut Elimination secures itself guarantees that the rules for one connective conservatively extend the subsystem comprising the rules for the remaining connectives. In the present case, the point of the example was that there was no proof of, for example, p ≻ q which did not detour—in violation of the subformula property—via formulas involving Tonk.