Round-six lemma `BAD23L_eq`