Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. Fin(Alph) Fin(St)

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

Conclusion:

Fin(x,y:(Alph List)//(x Rl y))

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

1. St:. Auto@0:Automata(Alph;St). Fin(St) L(Auto) = L(Auto@0)

2. Fin(x,y:(Alph List)//(x Rl y))