Level: Lib Thy Top: 1
Hypotheses:- Alph :
Conclusion:
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. 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))