Round-six lemma `pops_end`