Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Digital systems, linear algebra, introduction to formal proof / 8 / b / ii / Solution

Use reflexivity to obtain $T_1=T_1$. In equality elimination rule, take $\varphi (z)$ to be $z=T_1$, and replace the designated first occurrence of $T_1$ using the premise $T_1=T_2$:

ThereforeThe second occurrence of $T_1$ in $T_1=T_1$ is part of the fixed parameter in $\varphi (z)$ and is not replaced.