Round-six lemma `cov_chk`