At: strong safety implies safety 1
1. E: EventStruct
2. P: (|E| List)
Prop
3. 
x,y:|E| List. P(x) 
sublist(|E|;y;x) P(y)
4. x: |E| List
5. y: |E| List
6. P(x)
7. y 
x
sublist(|E|;y;x)
By: BackThru
Thm* L_1,L_2:T List. L_1 L_2 sublist(T;L_1;L_2)
Generated subgoals:None
About:
