Round-six lemma `fineE_runs`