\begin{frame}{Jan has \ldots\ bicycles}
  \begin{block}{\sentence{Jan has more than one bicycle}}
    \pause
    $\existsst{x}{\exists{y}{\big(\,
       \unpred{B}{x} \logandinf \unpred{B}{y} 
       \logandinf \binpred{H}{\const{j}}{x} \logandinf \binpred{H}{\const{j}}{y} 
       \logandinf x \neq y
     \,\big)}}$
  \end{block}
  \pause\medskip
  
  \begin{block}{\sentence{Jan has (precisely) two bicycles}}
    \pause
    There are more solutions:
    \begin{itemize}\vspace*{0.5ex}\setlength{\itemsep}{1ex}
      \item $\begin{aligned}[t]
             \existsst{x}{\existsst{y}{\bigl(\,
                &\unpred{B}{x} \logandinf \unpred{B}{y} 
                \logandinf x \neq y 
                \logandinf \binpred{H}{\const{j}}{x} \logandinf \binpred{H}{\const{j}}{y}\\
                &\;\logandinf\;
                \forall{z}{(
                  \unpred{B}{z} \logandinf \binpred{H}{\const{j}}{z} \logimpinf z = x \logorinf z = y)
                }
             \,\bigr)}}
             \end{aligned}$
    \pause
      \item $\begin{aligned}
             \existsst{x}{\existsst{y}{\big(\,
               x \neq y \logandinf 
               \forallst{z}{(\unpred{B}{z} \logandinf \binpred{H}{\const{j}}{z} 
                             \,\alert{\slogbiimp}\, z = x \logorinf z = y)
               }
             \,\big)}}
             \end{aligned}$ 
    \end{itemize}
  \end{block}
  \pause\medskip  
    
  \begin{block}{\sentence{Jan has two bicycles\mpause[1]{, \firebrick{but he only uses one of them}}}}
    $\begin{aligned}
      \existsst{x}{\existsst{y}{\big(\,
         &x \neq y \logandinf 
         \forallst{z}{(\unpred{B}{z} \logandinf \binpred{H}{\const{j}}{z} \logbiimpinf z = x \logorinf z = y)}
      \malt[2]{\,\big)}{}
      \mpause[2]{\\
         &\hspace{5cm}\logandinf \binpred{U}{\const{j}}{x} \logandinf \lognot{\binpred{U}{\const{j}}{y}}                      
      \,\big)}}}
    \end{aligned}$
  \end{block}
\end{frame}