(5steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: tag sublist preserved

E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), m:Label, tr1,tr2:A List. (tr1 R(tg) tr2) < tr1 > _m = < tr2 > _m A List
By:
Auto
THEN
Assert R(tg) preserves L. < tr1 > _m = < L > _m
Generated subgoals:

11. E: EventStruct
2. A: Type
3. evt: A|E|
4. tg: ALabel
5. m: Label
6. tr1: A List
7. tr2: A List
8. tr1 R(tg) tr2
R(tg) preserves L. < tr1 > _m = < L > _m A List
21. E: EventStruct
2. A: Type
3. evt: A|E|
4. tg: ALabel
5. m: Label
6. tr1: A List
7. tr2: A List
8. tr1 R(tg) tr2
9. R(tg) preserves L. < tr1 > _m = < L > _m A List
< tr1 > _m = < tr2 > _m A List

About:
listlambdafunctionuniverseequalimpliesall

(5steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc