Round-six lemma `c32_ok`