Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

Conclusion:

g:x,y:(Alph List)//(x Rl y) . c:St Alph List. (q:St. Auto(c q) = q) (q:St. a:Alph. c (Auto q a) = A(g) (c q) a)

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

1. g:x,y:(Alph List)//(x Rl y) . c:St Alph List. (q:St. Auto(c q) = q) (q:St. a:Alph. c (Auto q a) = A(g) (c q) a)