At: total back listify 1 1 1 1 1
1. Alph: Type
2. S: ActionSet(Alph)
3. sL: S.car*
4. Fin(Alph)
5. Fin(S.car)
6. s: S.car
7. mem_f(S.car;s;sL)
w:Alph*. mem_f(S.car;(S:w
s);sL)
By:
InstConcl [nil]
THEN
RecUnfold `maction` 0
THEN
Reduce 0
Generated subgoals:None
About:
