Round-six lemma `c4_ok`