Round-six lemma `uloop_runs`