Round-six lemma `big_ev`