Round-six lemma `gth_step`