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

  \begin{exampleblock}{}
    The LEM rule \quad$\vdash\; \alpha \vee \neg \alpha$\quad is derivable:
    \medskip
    
    \begin{tikzpicture}
    \naturaldeduction{
      \mpause[1]{
        \proofbox{
          \mpause{
            \proofstep{$\neg (\alpha \vee \neg \alpha) $}{assumption};
          }
          \mpause{
            \proofbox{
              \mpause{
                \proofstep{$\alpha$}{assumption};
              }
              \mpause{
                \proofstep{$\alpha \vee \neg \alpha$}{$\vee_{i_1}$ 2};
              }
              \mpause{
                \proofstep{$\bot$}{$\neg_e$ 3,1};
              }
            }
          }
          \mpause{
            \proofstep{$\neg \alpha$}{$\neg_i$ 2--4};
          }
          \mpause{
            \proofstep{$\alpha \vee \neg \alpha$}{$\vee_{i_2}$ 5};
          }
          \mpause{
            \proofstep{$\bot$}{$\neg_e$ 6,1};
          }
        }
      }
      \mpause{
        \proofstep{$\alpha \vee \neg \alpha$}{PBC 1--7};
      }
    }
    \end{tikzpicture}
  \end{exampleblock}
\end{frame}