\begin{frame}{Natural Deduction Rules for Equality}
  There are two rules for equality, introduction and elimination.
  \bigskip

  \def\extraVskip{4pt}
  \begin{block}{Equality introduction \;$=_i$}
    \begin{talign}
      \infer[\rulename{=_i}]
      {\quad t=t \quad}
      {}
    \end{talign}
  \end{block}
  \medskip

  \begin{block}{Equality elimination \;$=_e$}
    \begin{talign}
      \infer[\rulename{=_e}]
      {\phi[t_2/x]}
      {t_1 = t_2 && \phi[t_1/x]}
    \end{talign}
  \end{block}
\end{frame}