PrintForm Definitions mb structures Sections GenAutomata Doc

At: tag sublist member trivial

E:TaggedEventStruct, tr:|E| List, i:||tr||. (tr[i] < tr > _tag(E)(tr[i]))
By:
Auto
THEN
Unfold `tag_sublist` 0
THEN
RWO "member_filter" 0
THEN
Reduce 0
THEN
Easy
Generated subgoals:

None

About:
listnatural_numberapplyall

PrintForm Definitions mb structures Sections GenAutomata Doc