Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,S1,S2:
. A1:Automata(Alph;S1). A2:Automata(Alph;S2).
L(A1) = L(A2) 
x,y:(Alph List)//(x Rl y) = x,y:(Alph List)//(x Rl y)
Applied Tactic: UnivCD THENA Auto
Generated subgoals:1. x,y:(Alph List)//(x Rl y) = x,y:(Alph List)//(x Rl y)