Round-six lemma `g1_ok`