Round-six lemma `upF_runs`