Round-six lemma `gs_ok`