At: maction lemma 1 2 1 1
1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. L1: Alph*
5. L2: Alph*
6. L: Alph*
7. (S:L1
s) = (S:L2s)
8. u: Alph
9. v: Alph*
10. (S:v @ L1s) = (S:v @ L2s)
11. u.(v @ L1) = nil
s = (S:u.(v @ L2)s)
By: Inst
Thm* 
h:T, t:T*. 
h.t = nil
[Alph;u;v @ L1]
Generated subgoals:None
About:
