Substitution in Gentzen sequent calculus

168 Views Asked by At

In an answer to this question a substitution lemma is mentioned, namely

If the sequent $\Gamma \Rightarrow F$ is derivable and a term $t$ is free for a variable $x$ in $\Gamma,F$, then $\Gamma[x \leftarrow t] \Rightarrow F[x \leftarrow t]$ is derivable.

I don't understand whether this lemma is valid in LJ. If it is the case, does it need the cut rule?

If the cut rule isn't necessary to prove the lemma, can you produce an explicit derivation of $$\forall x \forall y R(x,y) \Rightarrow R(y,y)$$ without cuts?