is mentioned by

Thm* M:MessageStruct. EquivRel(|M|)(_1 =(M) _2)	[msg_eq_equiv]
Thm* M:MessageStruct. uid(M) |M|	[msg_id_wf]
Thm* M:MessageStruct. sender(M) |M|Label	[msg_sender_wf]
Thm* M:MessageStruct. content(M) |M||cEQ(M)|	[msg_content_wf]
Def TaggedEventStruct == E:TypeM:MessageStruct(E|M|)(ELabel)(E)(ELabel)Top	[tagged_event_str]
Def EventStruct == E:TypeM:MessageStruct(E|M|)(ELabel)(E)Top	[event_str]

Try larger context: GenAutomata