Round-six lemma `c40_ok`