is mentioned by

Thm* E:DecidableEquiv. EquivRel(|E|)(_1 =(E) _2)	[eq_dequiv_equiv]
Def =(M)(m_1,m_2) == ((content(M)(m_1)) =(cEQ(M)) (content(M)(m_2)))sender(M)(m_1) = sender(M)(m_2) (uid(M)(m_1)=uid(M)(m_2))	[msg_eq]

Try larger context: GenAutomata