Hybrid Sequence:
The starting point is a block of code that evaluates CBC-MAC on inputs $X$ and $X'$ and tests for a collision.
When $X$ and $X'$ are identical in the first $i$ blocks, then CBC-MAC will compute the same $Y_i$ value for both. The library can notice this and avoid calling $F$ twice in this case. No other calls to $F$ are expected to repeat.
Apply the security of the PRF, replacing $F$ with a lazy random dictionary. The standard three-hop maneuver is omitted.
Assume that each probe to the random dictionary has never been made before and trigger a bad event when that assumption is violated. We will need to argue later that this bad event has negligible probability.
Instead of sampling $\prftable[B_i]$ and then using it to compute $B_{i+1}$, we can sample $B_{i+1}$ and use it to compute $\prftable[B_i]$. The three-hop maneuver involving \claimref{provsec.clm.generalized-otp} is omitted.
The library never reads actual values from $\prftable[\cdot]$; instead, it only checks whether a value is defined in $\prftable[\cdot]$. The same functionality can be achieved with a simple set $\mathcal{B}$, and we can do away with $\prftable[\cdot]$.
Finally, modify the program to ignore everything that came before and simply return $\myfalse.$ The program's output changes only in case of a collision ($X \ne X'$ but $Y_\ell = Y'_{\ell'}$) so we indicate this case as a bad event.
// given: $X_1 \| \cdots \| X_\ell \ne X'_1 \| \cdots \| X'_{\ell'}$
$\key \gets \bits^\secpar$
// $F_{\textsf{cbc}}(\key,X)$:
$B_1 := X_1$
for $i = 1$ to $\ell$:
$Y_i := {}$
$F(\key, B_i)$
$\prftable[B_i]$
$$
$ $
${}\gets \bits^\secpar$
${}:= B_{i+1} \oplus X_{i+1}$
$B_{i+1} \oplus X_{i+1}$
$B_{i+1} := Y_i \oplus X_{i+1}$
// $F_{\textsf{cbc}}(\key,X')$:
$B'_1 := X'_1$
for $i = 1$ to $\ell'$:
$Y'_i := {}$
$F(\key, B'_i)$
$\prftable[B'_i]$
$$
$ $
${}\gets \bits^\secpar$
${}:= B'_{i+1} \oplus X'_{i+1}$
$B'_{i+1} \oplus X'_{i+1}$
$B'_{i+1} := Y'_i \oplus X'_{i+1}$
return
$Y_\ell == Y'_{\ell'}$
$\myfalse$