At: maction wf 2 2
1. Alph: Type
2. S: ActionSet(Alph)
3. L: Alph*
4. s: S.car
5. u: Alph
6. v: Alph*
7. (S:v
s) 
S.car
8. 
u.v = nil
S.act(u,(S:vs)) S.car
By: Inst
Thm* 
T:Type, a:ActionSet(T). a.act T
a.cara.car
[Alph;S]
Generated subgoals:None
About:
