Use sequent calculus to show if $\Gamma\vdash t_1=t_2$ then $\Gamma\vdash f(t_1)=f(t_2)$

Question

Suppose the sequent $\Gamma\vdash t_1=t_2$ where $t_1,t_2$ are closed terms. Let $f$ be a one-place function symbol.

I am trying to find a sequent calculus derivation of $\Gamma\vdash f(t_1)=f(t_2)$ using these identity rules from this set of notes:

I don't see where functions fit in the picture.

Answer 1

Whenever there is a non-trivial sequent to prove in the sequent calculus, use the cut rule, which is the only "intelligent" rule in that proof system.

The idea is that you can easily derive the sequent $t_1 = t_2 \vdash f(t_1) = f(t_2)$ by the rule $=$, and then you cut this sequent with your assumption $\Gamma \vdash t_1 = t_2$.

The formal solution is below, where the formula $\varphi(x)$ to which I applied the rule $=$ is $f(t_1) = f(x)$.

! $$ \dfrac{ \displaystyle{\atop \Gamma \vdash t_1 = t_2} \qquad \dfrac{ \dfrac{ \dfrac{}{\vdash f(t_1) = f(t_1)}\text{refl} }{ t_1 = t_2 \vdash f(t_1) = f(t_1) }\text{w}_L } { t_1 = t_2 \vdash f(t_1) = f(t_2) }= }{ \Gamma \vdash f(t_1) = f(t_2) }\text{cut} $$