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) 1-1-Corresp(St;x,y:(Alph List)//(x Rl y))
Inj(St;x,y:(Alph List)//(x Rl y);c)
Applied Tactic: D 0 THENA Auto THEN D 0 THENA Auto THEN D 0 THENA Auto
Generated subgoals:1. c:St Alph List
(q:St. Auto(c q) = q) Fin(Alph) Fin(St) 1-1-Corresp(St;x,y:(Alph List)//(x Rl y))
Inj(St;x,y:(Alph List)//(x Rl y);c)