Hybrid Sequence:
The starting point is $\lib{dict-real}$.
Similar to the proof of \claimref{crhf.clm.hash-then-prf}, we can implement the dictionary $\prftable[\cdot]$ inefficiently using a list of records and explicit equality comparisons between strings. For this proof it is convenient to store records of the form $(X, H, Y)$ where $H = U(\key,X)$. When accessing the dictionary, we check the $H$-values and ignore the $X$-values; they will be used later.
Modify the library to recognize the correct record in the list according to its $X$-value instead of $H$-value. This will change the library's behavior \emph{only} in the event that $X \ne X'$ but $H == H'$. So record a bad event in that case; later we will show that the bad event has negligible probability.\FORMATTINGHACK{\pagebreak}
Now the UHF outputs are used only to trigger the bad event, and nothing else. So we can move all of the logic involving the UHF and bad event to the end of time. This involves two changes: storing only $(X,Y)$, not $H$, in the dictionary records, and storing a list of $(X,X')$ pairs that could possibly trigger the bad event.
$\lib{dict-real}$
$\key \gets \bits^\secpar$
dict.set($X, Y$):
$\prftable[U(\key,X)] := Y$
dict.get($X$):
return
$\prftable[U(\key,X)]$
$Y$