Round-six lemma `R1L_eq`