\begin{frame}{$\formula{\slogand}$, $\formula{\slogor}\,$ versus $\,\formula{\exists}$, $\,\formula{\forall}$}
  \begin{proposition}
    For all variables $\formula{\avarsynvar}$ and formulas $\aform$ it holds:  
    \begin{enumerate}[(i)]\setlength{\itemsep}{0.4ex}
      \item $\formula{\forallst{\avarsynvar}{(\logand{\aform}{\bform})}}
             \logequiv
             \formula{\logand{\forallst{\avarsynvar}{\,\aform}}{\forallst{\avarsynvar}{\,\bform}}}$
      \item $\formula{\existsst{\avarsynvar}{(\logor{\aform}{\bform})}}
             \logequiv
             \formula{\logor{\existsst{\avarsynvar}{\,\aform}}{\existsst{\avarsynvar}{\,\bform}}}$ 
    \end{enumerate}  
  \end{proposition}
  \pause\medskip

  \begin{alertblock}{}
    However, \alert{in general}:
    \begin{itemize}\setlength{\itemsep}{0.4ex}
    \item $\formula{\forallst{\avarsynvar}{(\logor{\aform}{\bform})}}
           \lognotequiv
           \formula{\logor{\forallst{\avarsynvar}{\,\aform}}{\forallst{\avarsynvar}{\,\bform}}}$
    \item $\formula{\existsst{\avarsynvar}{(\logand{\aform}{\bform})}}
           \lognotequiv
           \formula{\logand{\existsst{\avarsynvar}{\,\aform}}{\existsst{\avarsynvar}{\,\bform}}}$ 
    \end{itemize}  
  \end{alertblock}
  \pause\medskip
  
  \alt<-3>{
    \alert{But note:} for some specific $\aform$ and $\bform\,$:
    \begin{itemize}\setlength{\itemsep}{0.4ex}
    \item
      $\formula{\forallst{\avarsynvar}{(\logor{\aform}{\bform})}}
         \logequiv
       \formula{\logor{\forallst{\avarsynvar}{\,\aform}}{\forallst{\avarsynvar}{\,\bform}}}$
    \item 
      $\formula{\existsst{\avarsynvar}{(\logand{\aform}{\bform})}}
         \logequiv
       \formula{\logand{\existsst{\avarsynvar}{\,\aform}}{\existsst{\avarsynvar}{\,\bform}}}$ 
    \end{itemize}  
    can hold (e.g.\ if $\aform$ and $\bform$ are the same formula).
  }{
    \pause
    Yet:
    
    \begin{proposition}
      For all variables $\formula{\avarsynvar}$ and formulas $\aform$ these formulas are \emph{valid}:
      \begin{enumerate}[(i)]\setlength{\itemsep}{0.4ex}
      \item $\formula{\logor{(\forallst{\avarsynvar}{\,\aform}}{\forallst{\avarsynvar}{\,\bform})}
             \logimpinf
             \forallst{\avarsynvar}{(\logor{\aform}{\bform})}}$
      \item $\formula{\existsst{\avarsynvar}{(\logand{\aform}{\bform})}
             \logimpinf
             \logand{\existsst{\avarsynvar}{\,\aform}}{\existsst{\avarsynvar}{\,\bform}}}$ 
      \end{enumerate}  
    \end{proposition}  
  }
  \onslide<4>{}
  \vspace{10cm}
\end{frame}