Hybrid Sequence:
The starting point is $\lib{prf-real}$.
We can add a cache $\prftable[\cdot]$ so that each output is computed only once.
We can replace the calls to PRF $F$ with corresponding lookups in a lazy random dictionary $R[\cdot]$. Note: There is a \emph{single} dictionary $R[\cdot]$, which the library will access on both $X_1$ and $Y_1 \oplus X_2$. The standard three-hop maneuver has been omitted.
This hybrid contains an if-statement ``if $R[Y_1 \oplus X_2]$ undefined.'' Consider another hybrid in which the body of this if-statement is performed \emph{unconditionally.} The two hybrids behave identically unless/until $R[Y_1 \oplus X_2]$ is already defined. So, to show that the hybrids are indistinguishable, we can trigger a bad event in that case and later show that the bad event has negligible probability.
We can swap the assignment order of $\prftable[X_1 \| X_2]$ and $R[Y_1 \oplus X_2]$.
We can move $\prftable[X_1\|X_2] \gets \bits^\secpar$ earlier. After doing so, it is clear that $R[\cdot]$ does not affect the output of $\prfquery$: It is used only to determine whether to trigger the bad event.
Instead of triggering the bad event as $\prfquery$ is called, we can do so at the end of time. This will not change the bad event's probability.
$\lib{prf-real}$
$\key \gets \bits^\secpar$
$\prfquery$($X_1 \| X_2$):
$Y_1 := {}$
$F(\key,X_1)$
$R[X_1]$
$Y_2 := F(\key,Y_1 \oplus X_2)$
return
$Y_2$
$\prftable[X_1\|X_2]$