Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. c : St Alph List

  5. (q:St. Auto(c q) = q) Fin(Alph) Fin(St)

  6. EquivRel(Alph List;x,y.x Rl y)

Conclusion:

Surj(St;x,y:(Alph List)//(x Rl y);c)

Applied Tactic: InstLemma `fin_alph_list_quo` [Alph;x,y.x = y] THENA Auto
Generated subgoals:

1. EquivRel(Alph List;x,y.x (x,y.x = y) y)

2. Dec(x (x,y.x = y) y)

3. Surj(St;x,y:(Alph List)//(x Rl y);c)