Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,St:
. Auto:Automata(Alph;St). S:. A:Automata(Alph;S).
Fin(Alph) 
Fin(St) L(Auto) = L(A) Con(A) |S| 
|x,y:(Alph List)//(x Rl y)|
Applied Tactic: UnivCD THENA Auto
Generated subgoals:1. |S| |x,y:(Alph List)//(x Rl y)|