Round-six lemma `stageU_sp`