Round-six lemma `c16_ok`