\begin{frame}
\small

\begin{block}{Well-Founded Induction}
\smallskip
given
\begin{itemize}
\item
strongly normalizing ARS $\AA = \ARS$
\item<2->
% property \BLUE{P} of ARSs that satisfies \quad
% $\text{\BLUE{P}}(\AA) \quad\iff\quad
% \forall a \colon \text{\BLUE{P}}(a)$
property \BLUE{P} over the elements of $\AA$
\end{itemize}

\medskip

\onslide<3->
to conclude
\begin{itemize}
\item
% $\text{\BLUE{P}}(\AA)$
$\forall a \in A \colon \text{\BLUE{P}}(a)$
\end{itemize}

\medskip
 
\onslide<4->
it is sufficient to prove
\begin{itemize}
\item
if $\underbrace{\BLACK{\text{$\text{\BLUE{P}}(b)$ for every $b$
with $a \to b$}}}_{\text{\small \alert<4>{induction hypothesis}}}$ then
$\text{\BLUE{P}}(a)$
\end{itemize}
for arbitrary element $a$
\onslide<5->
\[
\biggl(\forall a \colon
\Bigl(\forall b \colon a \to b ~\Longrightarrow~
\text{\BLUE{P}}(b)\Bigr) ~\Longrightarrow~ \text{\BLUE{P}}(a)\biggr)
\quad\Longrightarrow\quad
\forall a \colon \text{\BLUE{P}}(a)
\qquad\qquad
\]
\end{block}

\end{frame}