\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}