Round-six lemma `umt2_eq`