\begin{frame}{$\formula{\slogimp}$ versus $\,\formula{\exists}$, $\,\formula{\forall}$}
  \begin{alertblock}{}
    {In general}:
    \begin{itemize}\setlength{\itemsep}{0.4ex}
    \item $\formula{\forallst{\avarsynvar}{(\logimp{\aform}{\bform})}}
           \lognotequiv
           \formula{\logimp{\forallst{\avarsynvar}{\,\aform}}{\forallst{\avarsynvar}{\,\bform}}}$
    \item $\formula{\existsst{\avarsynvar}{(\logimp{\aform}{\bform})}}
           \lognotequiv
           \formula{\logimp{\existsst{\avarsynvar}{\,\aform}}{\existsst{\avarsynvar}{\,\bform}}}$ 
    \end{itemize}  
  \end{alertblock}  
  \pause\medskip

  \alert{Note} again: for specific $\aform$ and $\bform\,$ it is possible:
  \begin{itemize}\setlength{\itemsep}{0.4ex}
  \item $\formula{\forallst{\avarsynvar}{(\logimp{\aform}{\bform})}}
         \logequiv
         \formula{\logimp{\forallst{\avarsynvar}{\,\aform}}{\forallst{\avarsynvar}{\,\bform}}}$
  \item $\formula{\existsst{\avarsynvar}{(\logimp{\aform}{\bform})}}
         \logequiv
         \formula{\logimp{\existsst{\avarsynvar}{\,\aform}}{\existsst{\avarsynvar}{\,\bform}}}$ 
  \end{itemize}
  (e.g.\ if $\aform$ and $\bform$ are the same formula).
  \pause\bigskip

  Yet, we have:
  \begin{proposition}
    For all variables $\formula{\avarsynvar}$ and formulas $\aform$ these formulas are \emph{valid}:
    \begin{enumerate}[(i)]\setlength{\itemsep}{0.4ex}
    \item $\formula{\forallst{\avarsynvar}{(\logimp{\aform}{\bform})}
           \logimpinf
           \logimp{(\forallst{\avarsynvar}{\,\aform}}{\forallst{\avarsynvar}{\,\bform})}}$
    \item $\formula{(\logimp{\existsst{\avarsynvar}{\,\aform}}{\existsst{\avarsynvar}{\,\bform})}
           \logimpinf
           \existsst{\avarsynvar}{(\logimp{\aform}{\bform})}}$ 
    \end{enumerate}  
  \end{proposition}  
\end{frame}