Round-six lemma `allL_spec`