75/77
\begin{frame}
  \frametitle{Examples}
  
  \vspace{-1ex}
  \begin{exampleblock}{$\myall{x}{(P(x) \vee Q(x))} \;\vdash\; \myall{x}{P(x)} \vee \myex{x}{Q(x)}$}
  \pause
  {\small
  \renewcommand{\lineheight}{.5cm}% regelafstand
  \begin{tikzpicture}
    \naturaldeduction{
      \proofstep{$\myall{x}{(P(x) \vee Q(x))}$}{premise};
      \proofbox{
        \proofstep{$\neg (\myall{x}{P(x)} \vee \myex{x}{Q(x)})$}{assumption};
        \namedproofbox{$y$}{
          \proofstep{$P(y) \vee Q(y)$}{$\forall_e\;$ 1};
          \proofbox{
            \proofstep{$P(y)$}{assumption};  
          }  
          \proofbox{
            \proofstep{$Q(y)$}{assumption};  
            \proofstep{$\myex{x}{Q(x)}$}{$\exists_i\;$ 5};
            \proofstep{$\myall{x}{P(x)} \vee \myex{x}{Q(x)}$}{$\vee_{i2}\;$ 7};
            \proofstep{$\bot$}{$\neg e\;$ 2,7};
            \proofstep{$P(y)$}{$\bot_e\;$ 8}; 
          }  
          \proofstep{$P(y)$}{$\vee_e\;$ 3, 4--4, 5--9}; 
        }
        \proofstep{$\myall{x}{P(x)}$}{$\forall_i\;$ 3--10};
        \proofstep{$\myall{x}{P(x)} \vee \myex{x}{Q(x)}$}{$\vee_{i1}\;$ 11};
        \proofstep{$\bot$}{$\neg_e\;$ 2,12};
      }
     \proofstep{$\myall{x}{P(x)} \vee \myex{x}{Q(x)}$}{PBC\; 2--13};
    }
  \end{tikzpicture}}
  \end{exampleblock}
\end{frame}