(3steps) PrintForm Definitions mb structures Sections GenAutomata Doc

At: member tag sublist 2
1. E: TaggedEventStruct
2. tr: |E| List
3. x: |E|
4. t: Label
5. (x tr)
6. tag(E)(x) = t

tag(E)(x) = t
By:
HypSubstSq -1 0
THEN
EqLblReflexive 0
Generated subgoals:

None

About:
listassertapplyequal

(3steps) PrintForm Definitions mb structures Sections GenAutomata Doc