Round-six lemma `g2_ok`