Round-six lemma `opK_CH`