 After all, the TONK-E rule is supposed to conclude \(B\) from \((A\) TONK \(B)\), but given that the TONK-I rule introduced the \((A\) TONK \(B)\) formula merely from the previous formula \(A\), clearly—if we are to honour the view that the elimination operation only has the effect of “undoing” the introduction rule—we need it to be the case that \(A\) already entailed \(B\).