Round-six lemma `c39_ok`