\begin{frame}{Symmetry of Equality}
  We show that
  \begin{talign}
    t_1 = t_2  \;\vdash\; t_2 = t_1
  \end{talign}
  
  \begin{exampleblock}{}
    \begin{tikzpicture}
      \naturaldeduction{
          \proofstep{$t_1=t_2$}{premise};
        \proofstep{$t_1=t_1$}{$=_i$};
        \proofstep{$t_2=t_1$}{$=_e\;$ 1,2};
      }
    \end{tikzpicture}
  \end{exampleblock}
  \medskip
  
  The rule $=_e$ in step 3 is applied with the formula \alert{$\phi = \alert{x=t_1}$}.
  \medskip
  
  Then \alert{$\phi[t_1/x] \;=\; t_1=t_1$} and \alert{$\phi[t_2/x] \;=\; t_2=t_1$}.
  \medskip

  \begin{goal}{}
  Recall the $=_e$-rule and the instance with $\phi = \alert{x=t_1}$:
  \begin{talign}
    \infer[\rulename{=_e}]
    {\phi[t_2/x]}
    {t_1 = t_2 && \phi[t_1/x]}
    &&
    \infer[\rulename{=_e}]
    {t_2 = t_1}
    {t_1 = t_2 && t_1 = t_1}
  \end{talign}
  \end{goal}  
\end{frame}