Round-six lemma `c36_ok`