Round-six lemma `g22_ok`