Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. L : L(Alph)

Conclusion:

Fin(Alph) Fin(x,y:(Alph List)//(Rl x y)) (l:Alph List. Dec(L l)) (St:. Auto:Automata(Alph;St). Fin(St) L = L(Auto))

Applied Tactic: InstLemma `lang_rel_equi` [Alph;L] THENA Auto
Generated subgoals:

1. Fin(Alph) Fin(x,y:(Alph List)//(Rl x y)) (l:Alph List. Dec(L l)) (St:. Auto:Automata(Alph;St). Fin(St) L = L(Auto))