is mentioned by

Thm* E:TaggedEventStruct, tr:|E| List, i:||tr||. (tr[i] < tr > _tag(E)(tr[i]))	[tag_sublist_member_trivial]
Thm* E:TaggedEventStruct, tr:|E| List, x:|E|, t:Label. (x < tr > _t) (x tr) & tag(E)(x) = t	[member_tag_sublist]
Thm* E:TaggedEventStruct. tag(E) |E|Label	[event_tag_wf]

Try larger context: GenAutomata