Hybrid Sequence:
The starting point is $\lib{prf-real}^H$:
We first separate $\key_1$ from $\key_2$, since they will be treated separately during the proof. We can also add a dictionary $\prftable^*[\cdot]$ to cache past answers of $\prfquery_H(\cdot)$ so that they are not recomputed twice.
We can apply the PRF security of $F$ in a three-hop maneuver, replacing $F(\key_1,\cdot)$ with a lazy random dictionary, which we name $\prftable_1[\cdot]$.
\FORMATTINGHACK{\needspace{3\baselineskip}\noindent}We can again apply the PRF security of $F$, this time replacing all calls to $F(\key_2,\cdot)$ with a lazy random dictionary. This is a new dictionary, which we call $\prftable_2$. The repetitive three-hop maneuver is not shown.
The ``if $\prftable_1[X]$ undefined'' condition is always true, because $\prftable_1[X]$ and $\prftable^*[X]$ are always assigned during the same call to $\prfquery_H(X)$, and we only reach this if-statement if $\prftable^*[X]$ is undefined. Thus, this if-statement's body can be made unconditional.
Now $\prftable_1[\cdot]$ is not needed, so it can be eliminated.
Uniformly sampled $Y$-values are indistinguishable from values sampled without replacement. The three-hop maneuver involving \lemmaref{comp.lem.birthday-lib} is omitted.
In this hybrid, the $Y$-values are guaranteed to not repeat. Thus, the inner if-statement is \emph{always} taken, and its body can be made unconditional.
Now the overall effect of the if-statement's body is to assign a uniformly sampled value to $\prftable^*[X]$. The same logic can be written more directly, without $Y$, $\mathcal{Y}$, or $\prftable_2[\cdot]$. The result of these simplification is $\lib{prf-rand}^H$, which completes the proof.
$\lib{prf-real}^H$
$\key_1 $
$\| \key_2 \gets \bits^{2\secpar}$
${}\gets \bits^\secpar$
$\prfquery_H$($X$):
$Y $
${}:= {}$
$F(\key_1, X)$
$\prfquery_F(X)$
$\prftable_1[X]$
${}\gets \bits^\secpar$
$$
${} \setminus \mathcal{Y}$
return
$F(\key_2, Y)$
$\prftable^*[X]$
$\link$
$\lib{prf-real}^F$
$\key \gets \bits^\secpar$
$\prfquery_F$($X$):
return $F(\key, X)$
$\lib{prf-rand}^F$
if $\prftable[X]$ undefined:
$\prftable[X] \gets \bits^\secpar$
return $\prftable[X]$