Round-six lemma `c14_ok`