Round-six lemma `jKprog_spec`