Replacing a term in a sequent by a variable

60 Views Asked by At

I'm going through 'Proof Theory' by Gaisi Takeuti (second edition 1987). Theorem 6.9 on page 34 talks about when one can replace all occurrences of a term $t$ in a provable sequent $S$ by a free variable to get another provable sequent $S'$. The sufficient condition stated in the theorem is that there's no sub-semi-term of $t$ is $S$.

My question is: what examples exist where the existence of a sub-semi-term of $t$ in $S$ prevents a proof of $S'$? As far as I can tell, one can still construct a proof $P'$ of $S'$ from the original proof $P$, albeit with possibly partial replacement of $t$ in sequents other than the lowest one.