\begin{frame}{
    But: \, $\formula{\forallst{x}{(\logor{\unpred{LL}{x}}{\unpred{C}{x}})}}
             \;\lognotequiv\;
             \formula{\logor{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$
  }                  
  
  \uncover<2->{%
  \begin{exampleblock}{}
    Define $\model{\amodel}$ as follows: 
    %
    \begin{center}
      $
      \begin{aligned}
        \text{domain } \model{\adomain} & = \{1,2\}
          & & &
        \intin{\sunpred{LL}}{\model{\amodel}} & = \setexp{1}
          & & &
        \intin{\sunpred{C}}{\model{\amodel}} & = \setexp{2}   
      \end{aligned}
      $
    \end{center}    
  \end{exampleblock}
  }
  
  
  \uncover<3->{Then:}
  \begin{itemize}\vspace*{0.3ex}\setlength{\itemsep}{0.3ex}
    \item<3->
      $\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{(\logor{\unpred{LL}{x}}{\unpred{C}{x}})}}$, because:
      \begin{itemize}\vspace*{0.2ex}\setlength{\itemsep}{0.3ex}
        \item<4-> 
          $\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto 1]} \formula{\unpred{LL}{\freevar{x}}}$
          and thus
          $\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto 1]} \formula{\logor{\unpred{LL}{\freevar{x}}}{\unpred{C}{\freevar{x}}}}$
          % $\M \mw_{[x\mapsto 1]} Gx$ en dus $\M \mw_{[x\mapsto 1]} Gx \of Dx$
        \item<5->
          $\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto 2]} \formula{\unpred{C}{\freevar{x}}}$
          and thus
          $\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto 2]} \formula{\logor{\unpred{LL}{\freevar{x}}}{\unpred{C}{\freevar{x}}}}$
          % $\M \mw_{[x\mapsto 2]} Dx$ en dus $\M \mw_{[x\mapsto 2]} Gx \of Dx$
        \item<6-> 
          Hence: $\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{(\logor{\unpred{LL}{x}}{\unpred{C}{x}})}}$
          %Conclusie:   $\M \mw \alle x (Gx \of Dx)$
      \end{itemize}
      \vspace*{0.5ex}
    \item<7-> 
      But $\model{\amodel} \satisfiesnotlookup{\saluf} \formula{\logor{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$, because:
      \begin{itemize}\vspace*{0.2ex}\setlength{\itemsep}{0.3ex}
        \item<8-> 
          $\model{\amodel} \satisfiesnotlookup{\saluf[\freevar{x}\mapsto 2]} \formula{\,\unpred{LL}{\freevar{x}}}$
            % $\M \not\mw_{[x\mapsto 2]} Gx$ en dus
          and thus
          $\model{\amodel} \satisfiesnotlookup{\saluf} \formula{\forallst{x}{\,\unpred{LL}{x}}}$ 
            % $\M \not\mw \alle x Gx$
        \item<9-> 
          $\model{\amodel} \satisfiesnotlookup{\saluf[\freevar{x}\mapsto 1]} \formula{\unpred{C}{\freevar{x}}} $ 
          and thus 
          $\model{\amodel} \satisfiesnotlookup{\saluf} \formula{\forallst{x}{\,\unpred{C}{x}}}$
            % $\M \not\mw_{[x\mapsto 1]} Dx$ en dus
            % $\M \not\mw \alle x Dx$
      \end{itemize}
  \end{itemize}
  
  \smallskip  
  
  \uncover<10->{
  \begin{block}{Follow-up question:}
    What about distribution of $\,\formula{\exists}\,$ over $\,\formula{\slogand}\,$ and $\,\formula{\slogor}\,$?}
    % Hoe zit het met de distributie van $\,\eris\,$ over $\,\en\,$ en $\of\;$?
  \end{block}
\end{frame}