Hybrid Sequence:
The starting point is $\lib{cpa-real}$.
We can apply the security of the PRF in a standard three-hop maneuver:
\FORMATTINGHACK{\needspace{2\baselineskip}\noindent}Sampling $R$ uniformly is indistinguishable from sampling without replacement. The standard three-hop maneuver involving \lemmaref{comp.lem.birthday-lib} is not shown.\FORMATTINGHACK{\pagebreak}
In this hybrid, the $R$ values can never repeat, so the if-statement is always taken. Thus, we can make its body unconditional.
Each value of $\prftable[R]$ is sampled uniformly and used only in a single \xor expression. As a result, $S$ is a OTP encryption of $\ptxt$, with $\prftable[R]$ playing the role of the key. In other words, $S$ is distributed uniformly. The three-hop maneuver involving \claimref{provsec.clm.otp} is not shown.
Finally, we can revert a previous change, so that $R$ is again sampled uniformly with replacement. The result is $\lib{cpa-rand}$, which completes the proof.
$\lib{cpa-real}$
$\key \gets \bits^\secpar$
$\cpaenc$($\ptxt$):
// $R\|S \gets \Enc(\key,\ptxt)$
$R \gets \bits^\secpar$
$$
${} \setminus \mathcal{R}$
$$
$Y := {}$
$F(\key,R)$
$\prfquery(R)$
$S $
${}:= {}$
$Y \oplus \ptxt$
$\prftable[R] \oplus \ptxt$
${}\gets \bits^n$
return $R\|S$
$\link$
$\lib{prf-real}$
$\key \gets \bits^\secpar$
$\prfquery$($X$):
return $F(\key,X)$
$\lib{prf-rand}$
$\prfquery$($X$):
if $\prftable[X]$ undefined:
$\prftable[X] \gets \bits^n$
return $\prftable[X]$