Hybrid Sequence:
The starting point is $\lib{cpa-real}$.
As discussed above, it is convenient to name the PRP/PRF inputs (as $X_i$).
\FORMATTINGHACK{\needspace{3\baselineskip}\noindent}Compute the \emph{next} $X_i$ value as soon as possible, instead of just before using it as input to $F$. The last iteration of the for-loop has no ``next'' $X_i$ value, so we unroll that iteration from the loop and treat it separately.
Replace the PRF $F$ with a lazy random table. The three-hop maneuver involving $\lib{prf-*}$ is standard and omitted to save space.
We can make the bodies of the if-statements unconditional. This changes the library's behavior only when there is a repeat among the $X_i$ values---an event \FORMATTINGHACK{\pagebreak}that we expect to be rare. We can trigger a bad event in that case, and in a future step of the proof argue that the bad event has negligible probability.
Instead of sampling $\ctxt_i$ uniformly and computing the next $X_{i+1}$, we can sample $X_{i+1}$ uniformly and solve for $\ctxt_i$. There is no effect on the library's behavior. The three-hop maneuver involving \claimref{provsec.clm.generalized-otp} is not shown.
In this hybrid, every $X_i$ is sampled uniformly, and a bad event is triggered only when there is a repeat among these $X_i$'s. Thus, the probability of the bad event is the birthday probability $\Birthday(q,2^\secpar)$, where $q$ is the total number of ciphertext blocks generated during the library's execution. Since $q$ is a polynomial in the security parameter, this bad-event probability is negligible. \FORMATTINGHACK{\pagebreak}Now that we have fulfilled our promise to show that the bad event has negligible probability, the bad event logic is no longer needed and can be removed.
Now the library never reads from $\prftable[\cdot]$, so it can be removed. Also, each $\ctxt_i$ block is generated as a OTP encryption with $X_{i+1}$ acting as the key. Therefore, each $\ctxt_i$ is uniformly distributed. The result of a standard three-hop maneuver involving $\lib{otp-*}$ (not shown) gives us $\lib{cpa-rand}$, completing the proof.
$\lib{cpa-real}$
$\key \gets \bits^\secpar$
$\cpaenc$($\ptxt_1 \| \cdots \| \ptxt_\ell$):
$\ctxt_0 $
${}\gets \bits^\secpar$
${}:= X_1 \oplus \ptxt_1$
${}\gets \bits^\secpar$
for $i = 1$ to
$\ell$:
$\ell-1$:
$\ctxt_i $
${}:= {}$
$F(\key, {}$
$\ctxt_{i-1} \oplus \ptxt_i)$
$X_i)$
$\prftable[X_i]$
$$
$ $
${}\gets \bits^\secpar$
${}:= X_{i+1} \oplus \ptxt_{i+1}$
${}\gets \bits^\secpar$
return $\ctxt_0 \| \ctxt_1 \| \cdots \| \ctxt_\ell$