\begin{frame}
  \frametitle{Law of Excluded Middle}

  \begin{goal}{Law of Excluded Middle Rule}
    \vspace{-1ex}
    \begin{align*}
      \infer[\rulename{LEM}]
      {\alpha \vee \neg \alpha}
      {
      }
    \end{align*}
    (The rule does not have premises.)
  \end{goal}
    
  \begin{exampleblock}{}
    Show that \quad$p \to q \;\vdash\; \neg p \vee q$\quad:
    \smallskip
    
    \begin{tikzpicture}
    \naturaldeduction{
      \mpause[1]{
        \proofstep{$p \to q$}{premise};
      }
      \mpause{
        \proofstep{$p \vee \neg p$}{LEM};
      }
      \mpause{
        \proofbox{
          \mpause{
            \proofstep{$p$}{assumption};
          }
          \mpause{
            \proofstep{$q$}{$\to_e$ 3,1};
          }
          \mpause{
            \proofstep{$\neg p \vee q$}{$\vee_{i_2}$ 4};
          }
        }
      }
      \mpause{
        \proofbox{
          \mpause{
            \proofstep{$\neg p$}{assumption};
          }
          \mpause{
            \proofstep{$\neg p \vee q$}{$\vee_{i_1}$ 7};
          }
        }
      }
      \mpause{
        \proofstep{$\neg p \vee q$}{$\vee_e$ 2,\;3--5,\;6--7};
      }
    }
    \end{tikzpicture}
  \end{exampleblock}
\end{frame}