Round-six lemma `bodyB_runs`