57/179
\begin{frame}
  \frametitle{Copy Rule}

  \begin{goal}{Copy rule}
    \vspace{-1.5ex}
    \begin{align*}
      \infer[\rulename{copy}]
      {\alpha}
      {\alpha}
    \end{align*}
  \end{goal}  
  
  \begin{exampleblock}{}
  Lets try to prove \quad$\vdash p \to (q \to p)$\quad!
  \bigskip
  
  \begin{tikzpicture}
  \naturaldeduction{
    \mpause[1]{
    \proofbox{
      \mpause{
        \proofstep{$p$}{assumption};
      }
      \mpause{
        \proofbox{
          \mpause{
            \proofstep{$q$}{assumption};
          }
          \mpause{
            \proofstep{$p$}{copy 1};
          }
        }
      }
      \mpause{
       \proofstep{$q \to p$}{$\to_i$ 2--3};
      }
    }
    }
    \mpause{
      \proofstep{$p \to (q \to p)$}{$\to_i$ 1--4};
    }
  }
  \end{tikzpicture}
  \pause\pause\pause\pause\pause\pause\pause\pause
  \bigskip
  
  This concludes the derivation.
  \end{exampleblock}
\end{frame}