Round-six lemma `c3_ok`