Level: Lib Thy Top: 1 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. l : x,y:(Alph List)//(Auto(x) = Auto(y))

Conclusion:

F(Auto) Auto(l)


Applied Tactic: MemCD
Generated subgoals:

1. F(Auto) St

2. Auto(l) St