Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,St:
. Auto:Automata(Alph;St). l:x,y:(Alph List)//(x Rl y). Auto(l)
Applied Tactic: D 0 THENA Auto THEN D 0 THENA Auto THEN D 0 THENA Auto THEN InstLemma `lang_rel_equi` [
Alph
;
L(Auto)] THENA Auto
Generated subgoals:1. l:x,y:(Alph List)//(x Rl y). Auto(l)