is mentioned by

Thm* E:TaggedEventStruct, tr:|E| List, x:|E|, t:Label. (x < tr > _t) (x tr) & tag(E)(x) = t

[member_tag_sublist]

In prior sections: core fun 1 well fnd int 1 bool 1 rel 1 int 2 list 1 mb basic mb nat num thy 1 mb list 1 mb label mb list 2

Try larger context: GenAutomata