Round-six lemma `GREC_len`