Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,St:
. Auto:Automata(Alph;St). c:St 
Alph List.
(q:St. Auto(c q) = q) 
Fin(Alph) Fin(St) 
Surj(St;x,y:(Alph List)//(x Rl y);c)
Applied Tactic: UnivCD THENW Auto
Generated subgoals:1. Surj(St;x,y:(Alph List)//(x Rl y);c)