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

For transitivity of first-order equality, take the substitution formula $\varphi (u)\equiv (T_1=u)$:For symmetry, use reflexivity and $\psi (u)\equiv (u=T_1)$:Thus both transitivity and symmetry follow from the two equality rules. In the symmetry proof, only the designated first occurrence in $T_1=T_1$ is replaced; the second remains fixed.