\begin{frame}{Change of Bound Variables}
  \begin{proposition}
  For all variables $\formula{\avarsynvar}$ and formulas $\aform$ it holds:  
  \begin{enumerate}[(i)]\setlength{\itemsep}{0.4ex}
    \item
      $\;$
      $\formula{\existsst{\avarsynvar}{\:\aform}}
         \logequiv
       \formula{\existsst{\cvarsynvar}{\:\substforin{\cvarsynvar}{\avarsynvar}{\aform}}}$
      \hspace*{1ex} if $\cvarsynvar$ not free in $\aform$
    \item
      $\;$
      $\formula{\forallst{\avarsynvar}{\:\aform}}
         \logequiv
       \formula{\forallst{\cvarsynvar}{\:\substforin{\cvarsynvar}{\avarsynvar}{\aform}}}$
      \hspace*{1ex} 
      if $\cvarsynvar$ not free in $\aform$  
  \end{enumerate}  
  \end{proposition}  
  \pause\medskip
  
  Recall that
  \begin{goal}{}
    \begin{talign}
      \substforin{\term{\ater}}{\avarsynvar}{\aform}
    \end{talign}
    is the result of replacing all free occurrences of $\avarsynvar$ in~$\aform$ by $\term{\ater}$\\
    if \alert{no capture of free variables happens}, otherwise \textit{undefined}.
  \end{goal}
  \pause
  
  \begin{alertblock}{}
    \begin{talign}
      \formula{\myex{y}{R(\freevar{x},y)} \;  [y/x]} \hspace*{1ex} \text{\alert{is undefined}}
    \end{talign}
    since in the replacement result $\formula{\myex{y}{R(y,y)}}$
    \alert{capture of} the inserted variable $\term{y}$ has happened. 
  \end{alertblock}
\end{frame}