Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. L:L(Alph).
Fin(Alph)
Fin(x,y:(Alph List)//(Rl x y)) 
(l:Alph List. Dec(L l))
(
St:. Auto:Automata(Alph;St). Fin(St) L = L(Auto))
Applied Tactic: D 0 THENW Auto
Generated subgoals:1. L:L(Alph)
Fin(Alph)
Fin(x,y:(Alph List)//(Rl x y)) (l:Alph List. Dec(L l))
(St:. Auto:Automata(Alph;St). Fin(St) L = L(Auto))